Projects · Feasibility study
Thirteen Verified Results
Wave 1 was a feasibility study of the operating procedure: freeze a conjecture exactly as stated in its source, attack that statement, verify any result through independent exact checkers or the Lean kernel, and release the supporting record. It was intended to test the pipeline before work moved to harder targets, not to establish a general success rate.
The resulting portfolio contains thirteen results: eleven refutations of conjectures as stated, one proof of the Elizalde–Luo {1132, 3312} conjecture in Lean 4, and the lower bound C(13) ≥ 36 for the “no 5 on a sphere” problem. The refutations include qualifications that matter to their scope: the Graffiti 154 result uses the standard-deviation reading; the Sun result refutes part (ii), not part (i); and the three solubilizer results carry the restrictions recorded in the catalog.
The study established that this workflow could produce a mixed portfolio of kernel-checked theorems and finite certificates with recorded verification gates. It did not establish novelty by mechanical means, replace the human review of statement fidelity, or provide external refereeing. None of these results has been externally refereed.
Individual results
Verification grades are defined in the master catalog.
| Result | Grade |
|---|---|
| A Pattern-Avoidance Conjecture of Elizalde and Luo, Proved in Lean 4 — the {1132, 3312} count is proved for all n and kernel-checked. | kernel |
| A Discrete Borsuk Partition Conjecture, Disproved in Lean 4 — a four-point witness at d = 2 refutes Conjecture 3 as stated. | kernel |
| C(13) ≥ 36 for the “No 5 on a Sphere” Grid Problem — an explicit 36-point certificate improves the inherited lower bound 33. | dual-checker |
| Sun's Conjecture 4.6(ii) on Sine Permanents, Refuted at p = 29 — both sign clauses fail at the first prime beyond Sun's table; part (i) is not refuted. | dual-checker |
| Two Graffiti Conjectures on Graph Eigenvalues, Refuted — 143 fails under both average-distance conventions, and 154 fails under the standard-deviation reading. | dual-checker |
Further refutations
The weight of these results varies. This group includes machine-generated conjectures and conjectures from very fresh papers; the three solubilizer statements are LLM-generated appendix conjectures and are recorded at erratum-note scale.
| Result | Grade | Artifacts |
|---|---|---|
| IRIS Conjecture 6.1 (“NuevaMirada”) is refuted as printed by exactly five 10-face counterexamples, with none smaller; the cleanest has p3 = 4, p5 = 3, p7 = 3, while the integer-rounded weakening survives the census through 16 faces. | dual-checker | RESULTS.md · problem tree |
| TxGraffiti / Davila Conjecture 9 (arXiv:2406.19231v2), that connected cubic diamond-free graphs satisfy Z(G) ≤ γ(G)+2, is refuted as stated by G14 at n = 14, where Z = 7 = γ+3; the proved claw-free sibling is untouched. | dual-checker | RESULTS.md · problem tree |
| Pandey's parity conjecture (arXiv:2601.03293 v1), that I(GP(n,k)) is real-rooted iff k is even, is refuted as stated in both directions outside the author's tested window: GP(9,2) is not real-rooted; GP(7,3) and GP(3,1) are; and GP(7,2) is isomorphic to GP(7,3). | dual-checker | RESULTS.md · problem tree |
| Koch–Narayan Conjecture 1 (arXiv:2511.01719 v1), on maximal bipartite graphs with a unique minimum dominating set, is refuted as stated at n = 13, γ = 4, with s = 22 > 21 = m(13,4); the γ = 3 strip is not refuted. | dual-checker | RESULTS.md · problem tree |
| Solubilizer Conjecture A.1 is refuted as stated at G = A5 with x a 5-cycle, where Sol = D10 has no nontrivial normal subgroup. | dual-checker | RESULTS.md · problem tree |
| Solubilizer Conjecture A.13 is refuted as stated at G = A5 × S3. | audit-panel | RESULTS.md · problem tree |
| Solubilizer Conjecture A.16 is refuted as stated at G = A5 × S4, where Sol = D10 × S4 has derived length 3 and is not metabelian. | audit-panel | RESULTS.md · problem tree |
Artifacts
The Lean results are kernel-checked, the finite certificates are dual-checked, and the statements were frozen verbatim from their sources; none of the results has been externally refereed.
python verify_all.py.Limitations
These results have not been externally refereed. Mechanical verification establishes the formal claim checked, not its novelty or the fidelity of the formalization to the cited informal statement. Those questions were reviewed internally and are documented separately for each result. Refutations apply to the conjectures as stated; the catalog records any surviving variant, untested range, reading dependence, or other limitation.