| 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 |
|
|
| 1343 |
2020/01/23 19:42:11
|
n < m \/ n = m \/ n > m
|
blue_jam |
Failure |
|
|
| 1342 |
2020/01/20 15:23:26
|
forall f: bool -> bool, f^3(x) = f(x)
|
Eldora |
Success |
|
|
| 1341 |
2020/01/20 15:08:24
|
forall f: bool -> bool, f^3(x) = f(x)
|
Eldora |
Success |
|
|
| 1340 |
2020/01/20 14:15:29
|
plus_comm
|
Eldora |
Success |
|
|
| 1339 |
2020/01/20 13:29:41
|
plus_assoc
|
Eldora |
Success |
|
|
| 1338 |
2020/01/16 20:41:29
|
Any natural number is expressible in binary notation
|
na4zagin3 |
Failure |
|
|
| 1337 |
2020/01/16 20:37:44
|
Any natural number is expressible in binary notation
|
nuip |
Failure |
|
|
| 1336 |
2020/01/16 20:37:35
|
Multiplication of non-zero value in F_p is injective
|
nuip |
Failure |
|
|
| 1335 |
2020/01/16 20:31:40
|
Any natural number is expressible in binary notation
|
blue_jam |
Failure |
|
|
| 1334 |
2020/01/16 20:06:35
|
Any natural number is expressible in binary notation
|
nekodesu |
Failure |
|
|
| 1333 |
2020/01/13 14:38:15
|
Three is prime
|
kurgm |
Success |
|
|
| 1332 |
2020/01/13 12:52:06
|
Boolean-hole principle
|
kurgm |
Success |
|
|
| 1331 |
2020/01/09 20:04:51
|
n * S m = n + n * m
|
nekodesu |
Failure |
|
|
| 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 |
|
|