Skip to content

Commit 521b93f

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(proofs): expand corpus for 10+ provers + fix EchidnaBuddy overclaim
proofs/metamath/tiny.mm, broken.mm — smallest valid + deliberate-fail proofs/dimacs/*.cnf — 5 SAT/UNSAT problems for cadical proofs/smt-lib-mined/*.smt2 — 15 synthetic LIA/NIA/BV/UF/AX/NRA problems exercising QF_LIA..QF_NRA across z3 + cvc5 src/julia/EchidnaBuddy.jl docstring fixed: module previously claimed to implement "Simulated Annealing AND Tactic Swarming" — only SA exists. Documented real status + what is NOT implemented (PSO, GA, k9/A2ML integration, tests). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 6f78591 commit 521b93f

40 files changed

Lines changed: 1361 additions & 1 deletion

‎proofs/agda/IdentityLaws.agdai‎

27.6 KB
Binary file not shown.

‎proofs/coq/.basic.aux‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
COQAUX1 6ce7438fa2096eadc5f6feaa2a894e8a /var/mnt/eclipse/repos/echidna/proofs/coq/basic.v
2+
0 0 VernacProof "tac:no using:no"
3+
736 740 proof_build_time "0.001"
4+
0 0 identity "0.001"
5+
695 703 context_used ""
6+
736 740 proof_check_time "0.000"
7+
0 0 VernacProof "tac:no using:no"
8+
856 860 proof_build_time "0.001"
9+
0 0 identity' "0.001"
10+
847 855 context_used ""
11+
856 860 proof_check_time "0.000"
12+
0 0 VernacProof "tac:no using:no"
13+
1483 1487 proof_build_time "0.001"
14+
0 0 modus_ponens "0.001"
15+
1427 1437 context_used ""
16+
1483 1487 proof_check_time "0.000"
17+
0 0 VernacProof "tac:no using:no"
18+
1671 1675 proof_build_time "0.001"
19+
0 0 modus_ponens' "0.001"
20+
1621 1632 context_used ""
21+
1671 1675 proof_check_time "0.000"
22+
0 0 VernacProof "tac:no using:no"
23+
1827 1831 proof_build_time "0.000"
24+
0 0 modus_ponens'' "0.000"
25+
1781 1786 context_used ""
26+
1827 1831 proof_check_time "0.000"
27+
0 0 VernacProof "tac:no using:no"
28+
2420 2424 proof_build_time "0.001"
29+
0 0 transitivity "0.001"
30+
2378 2388 context_used ""
31+
2420 2424 proof_check_time "0.000"
32+
0 0 VernacProof "tac:no using:no"
33+
2659 2663 proof_build_time "0.001"
34+
0 0 transitivity' "0.001"
35+
2647 2658 context_used ""
36+
2659 2663 proof_check_time "0.000"
37+
0 0 VernacProof "tac:no using:no"
38+
2980 2984 proof_build_time "0.001"
39+
0 0 and_intro "0.001"
40+
2950 2960 context_used ""
41+
2980 2984 proof_check_time "0.000"
42+
0 0 VernacProof "tac:no using:no"
43+
3227 3231 proof_build_time "0.001"
44+
0 0 and_elim_left "0.001"
45+
3216 3226 context_used ""
46+
3227 3231 proof_check_time "0.000"
47+
0 0 VernacProof "tac:no using:no"
48+
3444 3448 proof_build_time "0.001"
49+
0 0 and_elim_right "0.001"
50+
3433 3443 context_used ""
51+
3444 3448 proof_check_time "0.000"
52+
0 0 VernacProof "tac:no using:no"
53+
3685 3689 proof_build_time "0.002"
54+
0 0 and_commutative "0.002"
55+
3674 3684 context_used ""
56+
3685 3689 proof_check_time "0.000"
57+
0 0 VernacProof "tac:no using:no"
58+
3931 3935 proof_build_time "0.001"
59+
0 0 or_intro_left "0.001"
60+
3920 3930 context_used ""
61+
3931 3935 proof_check_time "0.000"
62+
0 0 VernacProof "tac:no using:no"
63+
4181 4185 proof_build_time "0.001"
64+
0 0 or_intro_right "0.001"
65+
4170 4180 context_used ""
66+
4181 4185 proof_check_time "0.000"
67+
0 0 VernacProof "tac:no using:no"
68+
4558 4562 proof_build_time "0.002"
69+
0 0 or_elim "0.002"
70+
4547 4557 context_used ""
71+
4558 4562 proof_check_time "0.000"
72+
0 0 VernacProof "tac:no using:no"
73+
4875 4879 proof_build_time "0.002"
74+
0 0 curry "0.002"
75+
4864 4874 context_used ""
76+
4875 4879 proof_check_time "0.000"
77+
0 0 VernacProof "tac:no using:no"
78+
5151 5155 proof_build_time "0.002"
79+
0 0 uncurry "0.002"
80+
5140 5150 context_used ""
81+
5151 5155 proof_check_time "0.000"
82+
0 0 vo_compile_time "0.030"

‎proofs/coq/.list.aux‎

Lines changed: 87 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,87 @@
1+
COQAUX1 0bf9bbab8c3fa9f56c16986ccf79dece /var/mnt/eclipse/repos/echidna/proofs/coq/list.v
2+
0 0 VernacProof "tac:no using:no"
3+
786 790 proof_build_time "0.004"
4+
0 0 app_nil_r "0.004"
5+
773 785 context_used ""
6+
786 790 proof_check_time "0.001"
7+
0 0 VernacProof "tac:no using:no"
8+
1161 1165 proof_build_time "0.004"
9+
0 0 app_assoc "0.004"
10+
1148 1160 context_used ""
11+
1161 1165 proof_check_time "0.001"
12+
0 0 VernacProof "tac:no using:no"
13+
1331 1335 proof_build_time "0.001"
14+
0 0 cons_app "0.001"
15+
1318 1330 context_used ""
16+
1331 1335 proof_check_time "0.000"
17+
0 0 VernacProof "tac:no using:no"
18+
1798 1802 proof_build_time "0.003"
19+
0 0 length_app "0.003"
20+
1785 1797 context_used ""
21+
1798 1802 proof_check_time "0.001"
22+
0 0 VernacProof "tac:no using:no"
23+
1996 2000 proof_build_time "0.001"
24+
0 0 length_cons "0.001"
25+
1983 1995 context_used ""
26+
1996 2000 proof_check_time "0.000"
27+
0 0 VernacProof "tac:no using:no"
28+
2133 2137 proof_build_time "0.001"
29+
0 0 length_nil "0.001"
30+
2120 2132 context_used ""
31+
2133 2137 proof_check_time "0.000"
32+
0 0 VernacProof "tac:no using:no"
33+
2521 2525 proof_build_time "0.006"
34+
0 0 rev_app_distr "0.006"
35+
2508 2520 context_used ""
36+
2521 2525 proof_check_time "0.002"
37+
0 0 VernacProof "tac:no using:no"
38+
2895 2899 proof_build_time "0.005"
39+
0 0 rev_involutive "0.005"
40+
2882 2894 context_used ""
41+
2895 2899 proof_check_time "0.001"
42+
0 0 VernacProof "tac:no using:no"
43+
3222 3226 proof_build_time "0.008"
44+
0 0 length_rev "0.008"
45+
3217 3221 context_used ""
46+
3222 3226 proof_check_time "0.003"
47+
0 0 VernacProof "tac:no using:no"
48+
3574 3578 proof_build_time "0.003"
49+
0 0 map_length "0.003"
50+
3561 3573 context_used ""
51+
3574 3578 proof_check_time "0.001"
52+
0 0 VernacProof "tac:no using:no"
53+
3937 3941 proof_build_time "0.005"
54+
0 0 map_app "0.005"
55+
3924 3936 context_used ""
56+
3937 3941 proof_check_time "0.002"
57+
0 0 VernacProof "tac:no using:no"
58+
4298 4302 proof_build_time "0.004"
59+
0 0 map_map "0.004"
60+
4285 4297 context_used ""
61+
4298 4302 proof_check_time "0.001"
62+
0 0 VernacProof "tac:no using:no"
63+
4578 4582 proof_build_time "0.004"
64+
0 0 map_id "0.004"
65+
4565 4577 context_used ""
66+
4578 4582 proof_check_time "0.001"
67+
0 0 VernacProof "tac:no using:no"
68+
4898 4902 proof_build_time "0.004"
69+
0 0 map_rev "0.004"
70+
4885 4897 context_used ""
71+
4898 4902 proof_check_time "0.002"
72+
0 0 VernacProof "tac:no using:no"
73+
5112 5116 proof_build_time "0.001"
74+
0 0 fold_right_nil "0.001"
75+
5099 5111 context_used ""
76+
5112 5116 proof_check_time "0.000"
77+
0 0 VernacProof "tac:no using:no"
78+
5346 5350 proof_build_time "0.001"
79+
0 0 fold_right_cons "0.001"
80+
5333 5345 context_used ""
81+
5346 5350 proof_check_time "0.001"
82+
0 0 VernacProof "tac:no using:no"
83+
5716 5720 proof_build_time "0.003"
84+
0 0 fold_right_app "0.003"
85+
5703 5715 context_used ""
86+
5716 5720 proof_check_time "0.002"
87+
0 0 VernacProof "tac:no using:no"

‎proofs/coq/.nat.aux‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
COQAUX1 7b396d99494f97c07a3abd69aa2ead75 /var/mnt/eclipse/repos/echidna/proofs/coq/nat.v
2+
0 0 VernacProof "tac:no using:no"
3+
864 868 proof_build_time "0.005"
4+
0 0 plus_comm "0.005"
5+
851 863 context_used ""
6+
864 868 proof_check_time "0.001"
7+
0 0 VernacProof "tac:no using:no"
8+
1197 1201 proof_build_time "0.004"
9+
0 0 plus_assoc "0.004"
10+
1184 1196 context_used ""
11+
1197 1201 proof_check_time "0.001"
12+
0 0 VernacProof "tac:no using:no"
13+
1493 1497 proof_build_time "0.003"
14+
0 0 plus_0_r "0.003"
15+
1480 1492 context_used ""
16+
1493 1497 proof_check_time "0.000"
17+
0 0 VernacProof "tac:no using:no"
18+
1804 1808 proof_build_time "0.011"
19+
0 0 plus_succ_r "0.011"
20+
1791 1803 context_used ""
21+
1804 1808 proof_check_time "0.001"
22+
0 0 VernacProof "tac:no using:no"
23+
2098 2102 proof_build_time "0.002"
24+
0 0 mult_0_r "0.002"
25+
2088 2097 context_used ""
26+
2098 2102 proof_check_time "0.000"
27+
0 0 VernacProof "tac:no using:no"

‎proofs/coq/.propositional.aux‎

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
COQAUX1 6bcfd32afd3ce0aa23a071992139f39a /var/mnt/eclipse/repos/echidna/proofs/coq/propositional.v
2+
0 0 VernacProof "tac:no using:no"
3+
948 952 proof_build_time "0.004"
4+
0 0 de_morgan_1 "0.004"
5+
937 947 context_used ""
6+
948 952 proof_check_time "0.001"
7+
0 0 VernacProof "tac:no using:no"
8+
1368 1372 proof_build_time "0.003"
9+
0 0 de_morgan_1_rev "0.003"
10+
1357 1367 context_used ""
11+
1368 1372 proof_check_time "0.000"
12+
0 0 VernacProof "tac:no using:no"
13+
1965 1969 proof_build_time "0.003"
14+
0 0 de_morgan_2_constructive "0.003"
15+
1954 1964 context_used ""
16+
1965 1969 proof_check_time "0.000"
17+
0 0 VernacProof "tac:no using:no"
18+
2407 2411 proof_build_time "0.003"
19+
0 0 de_morgan_2_classical "0.003"
20+
2392 2406 context_used ""
21+
2407 2411 proof_check_time "0.001"
22+
0 0 VernacProof "tac:no using:no"
23+
2648 2652 proof_build_time "0.001"
24+
0 0 double_negation_intro "0.001"
25+
2637 2647 context_used ""
26+
2648 2652 proof_check_time "0.000"
27+
0 0 VernacProof "tac:no using:no"
28+
3076 3080 proof_build_time "0.002"
29+
0 0 double_negation_elim "0.002"
30+
3061 3075 context_used ""
31+
3076 3080 proof_check_time "0.000"
32+
0 0 VernacProof "tac:no using:no"
33+
3510 3514 proof_build_time "0.002"
34+
0 0 lem_implies_dne "0.002"
35+
3495 3509 context_used ""
36+
3510 3514 proof_check_time "0.000"
37+
0 0 VernacProof "tac:no using:no"
38+
3871 3875 proof_build_time "0.003"
39+
0 0 peirce_law "0.003"
40+
3860 3870 context_used ""
41+
3871 3875 proof_check_time "0.000"
42+
0 0 VernacProof "tac:no using:no"
43+
4158 4162 proof_build_time "0.001"
44+
0 0 contrapositive "0.001"
45+
4147 4157 context_used ""
46+
4158 4162 proof_check_time "0.000"
47+
0 0 VernacProof "tac:no using:no"
48+
4506 4510 proof_build_time "0.003"
49+
0 0 contrapositive_reverse "0.003"
50+
4495 4505 context_used ""
51+
4506 4510 proof_check_time "0.000"
52+
0 0 VernacProof "tac:no using:no"
53+
4766 4770 proof_build_time "0.002"
54+
0 0 or_commutative "0.002"
55+
4749 4765 context_used ""
56+
4766 4770 proof_check_time "0.000"
57+
0 0 VernacProof "tac:no using:no"
58+
5069 5073 proof_build_time "0.004"
59+
0 0 or_associative "0.004"
60+
5044 5068 context_used ""
61+
5069 5073 proof_check_time "0.001"
62+
0 0 VernacProof "tac:no using:no"
63+
5394 5398 proof_build_time "0.003"
64+
0 0 and_associative "0.003"
65+
5383 5393 context_used ""
66+
5394 5398 proof_check_time "0.000"
67+
0 0 VernacProof "tac:no using:no"
68+
5612 5616 proof_build_time "0.003"
69+
0 0 and_associative_rev "0.003"
70+
5601 5611 context_used ""
71+
5612 5616 proof_check_time "0.000"
72+
0 0 VernacProof "tac:no using:no"
73+
5987 5991 proof_build_time "0.002"
74+
0 0 and_distributes_over_or "0.002"
75+
5961 5986 context_used ""
76+
5987 5991 proof_check_time "0.001"
77+
0 0 VernacProof "tac:no using:no"
78+
6262 6266 proof_build_time "0.003"
79+
0 0 and_distributes_over_or_rev "0.003"
80+
6244 6261 context_used ""
81+
6262 6266 proof_check_time "0.001"
82+
0 0 VernacProof "tac:no using:no"
83+
6640 6644 proof_build_time "0.004"
84+
0 0 or_distributes_over_and "0.004"
85+
6622 6639 context_used ""
86+
6640 6644 proof_check_time "0.000"
87+
0 0 VernacProof "tac:no using:no"
88+
7046 7050 proof_build_time "0.002"
89+
0 0 proof_by_contradiction "0.002"
90+
7031 7045 context_used ""
91+
7046 7050 proof_check_time "0.000"
92+
0 0 VernacProof "tac:no using:no"
93+
7261 7265 proof_build_time "0.001"
94+
0 0 ex_falso "0.001"
95+
7246 7260 context_used ""
96+
7261 7265 proof_check_time "0.000"
97+
0 0 vo_compile_time "0.219"

‎proofs/coq/algebra/.GroupTheory.aux‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
COQAUX1 e5207d7d070e743a29c20c7b6936edd5 /var/mnt/eclipse/repos/echidna/proofs/coq/algebra/GroupTheory.v

‎proofs/coq/algebra/GroupTheory.glob‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
DIGEST e5207d7d070e743a29c20c7b6936edd5
2+
FGroupTheory

0 commit comments

Comments
 (0)