| 1330 |
2020/01/09 20:04:32
|
forall f: bool -> bool, f^3(x) = f(x)
|
nekodesu |
Failure |
|
|
| 1329 |
2020/01/09 20:03:43
|
infinite bool sequence is uncountable
|
blue_jam |
Failure |
|
|
| 1328 |
2020/01/09 19:59:54
|
n * S m = n + n * m
|
nuip |
Failure |
|
|
| 1327 |
2020/01/09 19:53:06
|
forall f: bool -> bool, f^3(x) = f(x)
|
nuip |
Failure |
|
|
| 1326 |
2020/01/09 19:39:15
|
infinite bool sequence is uncountable
|
nuip |
Failure |
|
|
| 1325 |
2020/01/09 18:54:16
|
1 + 1 = 2
|
nekodesu |
Failure |
|
|
| 1324 |
2020/01/09 18:51:16
|
plus_comm
|
nekodesu |
Failure |
|
|
| 1323 |
2020/01/09 18:49:04
|
plus_assoc
|
nekodesu |
Failure |
|
|
| 1322 |
2020/01/04 20:34:47
|
plus_comm
|
Eldora |
Success |
|
|
| 1321 |
2020/01/04 05:39:42
|
1 + 1 = 2
|
Eldora |
Success |
|
|
| 1320 |
2020/01/04 05:39:23
|
1 + 1 = 2
|
Eldora |
Failure |
|
|
| 1319 |
2019/12/26 23:13:56
|
Relative prime squares
|
fetburner |
Success |
|
|
| 1318 |
2019/12/24 17:34:20
|
Multiplication of non-zero value in F_p is injective
|
fetburner |
Success |
|
|
| 1317 |
2019/12/22 21:20:17
|
n < m \/ n = m \/ n > m
|
nmjr31 |
Success |
|
|
| 1316 |
2019/12/22 11:51:52
|
l1 <> l2 if l2 is an odd permutation of l1
|
fetburner |
Success |
|
|
| 1315 |
2019/12/22 09:05:44
|
Equivalent two quicksorts
|
fetburner |
Success |
|
|
| 1314 |
2019/12/22 08:58:19
|
Equivalent two quicksorts
|
fetburner |
Failure |
|
|
| 1313 |
2019/12/21 23:12:41
|
n * S m = n + n * m
|
nmjr31 |
Success |
|
|
| 1312 |
2019/12/21 22:48:32
|
forall f: bool -> bool, f^3(x) = f(x)
|
nmjr31 |
Success |
|
|
| 1311 |
2019/12/21 22:23:29
|
1 + 1 = 2
|
nmjr31 |
Success |
|
|
| 1310 |
2019/12/21 22:21:41
|
plus_comm
|
nmjr31 |
Success |
|
|
| 1309 |
2019/12/21 22:02:40
|
plus_assoc
|
nmjr31 |
Success |
|
|
| 1308 |
2019/12/21 22:00:49
|
plus_assoc
|
nmjr31 |
Failure |
|
|
| 1307 |
2019/12/21 16:31:58
|
n * S m = n + n * m
|
ry3s |
Success |
|
|
| 1306 |
2019/12/21 16:10:00
|
forall f: bool -> bool, f^3(x) = f(x)
|
ry3s |
Success |
|
|
| 1305 |
2019/12/21 15:58:36
|
1 + 1 = 2
|
ry3s |
Success |
|
|
| 1304 |
2019/12/21 15:55:31
|
plus_comm
|
ry3s |
Success |
|
|
| 1303 |
2019/12/21 15:33:37
|
plus_assoc
|
ry3s |
Success |
|
|
| 1302 |
2019/12/20 16:13:13
|
Uniqueness of inequality proofs
|
fetburner |
Success |
|
|
| 1301 |
2019/12/20 15:08:28
|
Binary search
|
fetburner |
Success |
|
|
| 1300 |
2019/12/20 14:02:28
|
Iterated iteration
|
fetburner |
Success |
|
|
| 1299 |
2019/12/20 12:01:04
|
Grand Garden
|
fetburner |
Success |
|
|
| 1298 |
2019/12/20 10:13:28
|
Sum of binomial coefficients
|
fetburner |
Success |
|
|
| 1297 |
2019/12/20 09:30:37
|
Tree addressing is injective
|
fetburner |
Success |
|
|
| 1296 |
2019/12/20 09:19:16
|
infinite bool sequence is uncountable
|
fetburner |
Success |
|
|
| 1295 |
2019/12/20 09:07:02
|
Double
|
fetburner |
Success |
|
|
| 1294 |
2019/12/19 20:19:06
|
Zero test
|
nekodesu |
Failure |
|
|
| 1293 |
2019/12/19 20:09:31
|
Boolean-hole principle revisited
|
nuip |
Failure |
|
|
| 1292 |
2019/12/19 20:03:05
|
Boolean-hole principle revisited
|
nekodesu |
Failure |
|
|
| 1291 |
2019/12/18 23:58:47
|
Boolean-hole principle revisited
|
fetburner |
Success |
|
|
| 1290 |
2019/12/18 23:54:11
|
Midpoint
|
fetburner |
Success |
|
|
| 1289 |
2019/12/18 23:23:05
|
Zero test
|
fetburner |
Success |
|
|
| 1288 |
2019/12/18 23:20:57
|
Constructor is injective
|
fetburner |
Success |
|
|
| 1287 |
2019/12/18 23:19:55
|
Yoneda embedding for preorder
|
fetburner |
Success |
|
|
| 1286 |
2019/12/18 23:06:13
|
Two is not Three
|
fetburner |
Success |
|
|
| 1285 |
2019/12/18 22:52:38
|
Three is prime
|
fetburner |
Success |
|
|
| 1284 |
2019/12/18 22:38:47
|
Boolean-hole principle
|
fetburner |
Success |
|
|
| 1283 |
2019/12/18 22:36:49
|
De Morgan's laws in Coq
|
fetburner |
Success |
|
|
| 1282 |
2019/12/18 22:32:35
|
Any natural number is expressible in binary notation
|
fetburner |
Success |
|
|
| 1281 |
2019/12/18 22:21:03
|
De Morgan's laws in Coq
|
fetburner |
Rejected |
|
|