| 1393 |
2020/03/12 19:55:51
|
gcd(n, n+1) = 1
|
nekodesu |
Failure |
|
|
| 1392 |
2020/03/10 19:46:44
|
Cycle detection
|
kozima |
Success |
|
|
| 1391 |
2020/03/10 19:46:08
|
Postorder traversal
|
kozima |
Success |
|
|
| 1390 |
2020/03/10 19:45:06
|
Not a sum of squares
|
kozima |
Success |
|
|
| 1389 |
2020/03/10 19:44:14
|
eq_sym?
|
kozima |
Success |
|
|
| 1388 |
2020/03/05 19:00:38
|
and_comm (Lean)
|
ukikagi |
Success |
|
|
| 1387 |
2020/02/26 14:48:34
|
n < m \/ n = m \/ n > m
|
yishibashi |
Success |
|
|
| 1386 |
2020/02/25 17:50:45
|
Zero test
|
proofninja |
Failure |
|
|
| 1385 |
2020/02/24 03:44:57
|
Zero test
|
chir |
Success |
|
|
| 1384 |
2020/02/24 03:01:08
|
n < m \/ n = m \/ n > m
|
chir |
Success |
|
|
| 1383 |
2020/02/24 02:45:21
|
n * S m = n + n * m
|
chir |
Success |
|
|
| 1382 |
2020/02/24 02:21:42
|
forall f: bool -> bool, f^3(x) = f(x)
|
chir |
Success |
|
|
| 1381 |
2020/02/24 02:10:16
|
1 + 1 = 2
|
chir |
Success |
|
|
| 1380 |
2020/02/20 08:11:11
|
n < m \/ n = m \/ n > m
|
emoken |
Success |
|
|
| 1379 |
2020/02/18 12:27:11
|
n * S m = n + n * m
|
emoken |
Success |
|
|
| 1378 |
2020/02/18 12:21:58
|
forall f: bool -> bool, f^3(x) = f(x)
|
emoken |
Success |
|
|
| 1377 |
2020/02/18 12:11:50
|
1 + 1 = 2
|
emoken |
Success |
|
|
| 1376 |
2020/02/18 12:07:53
|
plus_comm
|
emoken |
Success |
|
|
| 1375 |
2020/02/18 12:00:19
|
plus_comm
|
emoken |
Success |
|
|
| 1374 |
2020/02/18 11:53:06
|
plus_assoc
|
emoken |
Success |
|
|
| 1373 |
2020/02/13 19:01:51
|
and_comm (Lean)
|
na4zagin3 |
Success |
|
|
| 1372 |
2020/02/13 18:38:32
|
and_comm (Lean)
|
blue_jam |
Success |
|
|
| 1371 |
2020/02/08 07:20:41
|
and_comm (Lean)
|
tzik |
Success |
|
|
| 1370 |
2020/02/07 14:55:59
|
forall l: list nat, l @ [0] <> []
|
mttm |
Success |
|
|
| 1369 |
2020/02/07 14:42:57
|
Product of n consecutive integers is divisible by n!
|
mttm |
Success |
|
|
| 1368 |
2020/02/06 19:07:17
|
gcd(n, n+1) = 1
|
nekodesu |
Failure |
|
|
| 1367 |
2020/02/05 13:46:12
|
n < m \/ n = m \/ n > m
|
mttm |
Success |
|
|
| 1366 |
2020/02/05 08:19:22
|
and_comm (Lean)
|
nekodesu |
Success |
|
|
| 1365 |
2020/02/05 04:09:02
|
and_comm (Lean)
|
nuip |
Failure |
|
|
| 1364 |
2020/02/05 04:07:26
|
and_comm (Lean)
|
nuip |
Success |
|
|
| 1363 |
2020/02/05 04:06:47
|
and_comm (Lean)
|
nuip |
Failure |
|
|
| 1362 |
2020/02/05 03:15:54
|
and_comm (Lean)
|
asi1024 |
Success |
|
|
| 1361 |
2020/02/05 00:36:18
|
and_comm (Lean)
|
asi1024 |
Failure |
|
|
| 1360 |
2020/02/01 00:25:23
|
Boolean-hole principle
|
na4zagin3 |
Success |
|
|
| 1359 |
2020/02/01 00:25:22
|
De Morgan's laws in Coq
|
na4zagin3 |
Success |
|
|
| 1358 |
2020/02/01 00:25:20
|
mult_n_O
|
na4zagin3 |
Success |
|
|
| 1357 |
2020/02/01 00:25:19
|
gcd(n, n+1) = 1
|
na4zagin3 |
Success |
|
|
| 1356 |
2020/02/01 00:25:18
|
Summand of one
|
na4zagin3 |
Success |
|
|
| 1355 |
2020/02/01 00:25:16
|
forall l: list nat, l @ [0] <> []
|
na4zagin3 |
Success |
|
|
| 1354 |
2020/01/31 23:54:12
|
n * S m = n + n * m
|
na4zagin3 |
Success |
|
|
| 1353 |
2020/01/31 23:54:10
|
forall f: bool -> bool, f^3(x) = f(x)
|
na4zagin3 |
Success |
|
|
| 1352 |
2020/01/31 23:54:08
|
1 + 1 = 2
|
na4zagin3 |
Success |
|
|
| 1351 |
2020/01/31 23:54:05
|
plus_comm
|
na4zagin3 |
Success |
|
|
| 1350 |
2020/01/31 23:27:47
|
plus_assoc
|
na4zagin3 |
Success |
|
|
| 1349 |
2020/01/30 20:15:04
|
Summand of one
|
nekodesu |
Failure |
|
|
| 1348 |
2020/01/30 19:54:36
|
n < m \/ n = m \/ n > m
|
nekodesu |
Failure |
|
|
| 1347 |
2020/01/24 14:17:34
|
mult_n_O
|
Eldora |
Success |
|
|
| 1346 |
2020/01/24 14:11:34
|
Boolean-hole principle
|
Eldora |
Success |
|
|
| 1345 |
2020/01/23 20:14:48
|
n < m \/ n = m \/ n > m
|
nuip |
Failure |
|
|
| 1344 |
2020/01/23 20:12:40
|
n < m \/ n = m \/ n > m
|
nuip |
Failure |
|
|