A public, evidence-graded record of what has actually been proved, what has a machine-checked proof candidate, what is only partially formalized, and what remains open. Updated 15 July 2026.
The exact Formal Conjectures theorem is discharged, and the formal development proves the stronger strict positivity statement for every positive input.
A short structural argument bounds both custom distance terms and supplies a two-vertex induced forest. Dedicated CI and an axiom audit passed.
The exact research-open Formal Conjectures statement has a full Lean proof based on classifying the non-pendant core and the minimal total dominating sets.
A direct recursive Bernstein-style coloring proves the exact repository variant. The proof actually uses only infinitude of each indexed set.
Discrete Fourier orthogonality and Parseval prove sup |P(z)| ≥ √(n+1). The stronger uniform (1+c)√n research conjecture is not solved.
New defect-moment bounds and a claimed exact four-direction LP limit at α≈1.5768233969. The actual every-slope checkerboard NTIL lower bound remains open.
| Project | Current status | Exact boundary |
|---|---|---|
| WOWII 143 | Complete modular Lean proof; independent kernel-audit infrastructure is under review. | Proof source exists and compiles; external novelty and upstream acceptance remain separate. |
| WOWII 160 | Exact Formal Conjectures statement disproved by a five-vertex counterexample. | The historical graph conjecture may differ from the repository specification. |
| Erdős 865 | Exact-statement bridge and independent kernel verification are complete. | The underlying combinatorial solution is external and explicitly credited. |
| OEIS A387471 | Mathematical proof manuscript plus green Lean reductions. | The published weight-six classification and final finite-cardinality packaging are not yet formalized. |
Normalized square-addition packets, five elliptic quotients, rank/Selmer computations, multi-level Mordell–Weil sieves, ghost-tower analysis, and a current product-localization certification branch.
A structural classification reduces connected triangle-free induced-P5-free graphs to chain-graph and complete-C5-blow-up families. One global top-level lemma remains.
The work isolated the parity obstruction, a reflected Möbius correlation, and a conditional rough-sieving bridge. None of this currently constitutes a proof of Goldbach.
The campaign narrowed Dmono(22) to 33 or 34, with many canonical boundary cases eliminated and no 34-point witness found.
Conjectures 65, 133, 143, 160, 314, and 316.
602, 865, 885, 1150, 366, and related formal variants.
Concurrence counting formula and formalization frontier.
Substantial investigations that did not produce a complete proof.