A mathematical proof written on paper is only as reliable as the chain of reasoning the reader is willing to follow. Gaps get papered over. Assumptions sneak in unlabeled. Reviewers miss things. This is not a criticism of mathematicians — it is a feature of human cognition operating at the limits of complexity.
Lean 4 is a proof assistant: software that checks every step of a mathematical argument against a formal type theory. It does not follow arguments. It does not infer intent. It either compiles or it does not. There is no partial credit.
As of July 2026, the core theorems of the ONON framework have been formalized in Lean 4 using Mathlib 4.19.0. All theorems compile clean with zero sorry tactics. The repository is public. The CI pipeline runs on every commit. The build is green.
The Difference Between Axioms and Sorries
In Lean, two mechanisms allow you to declare an unproven step: sorry and axiom. A sorry is a hole — a placeholder the compiler ignores. An axiom is a named assumption that becomes part of the system. Both can appear in a proof.
GPPVerify contains zero sorry tactics. Every proof is complete and checkable. However, some theorems depend on declared axioms — explicitly named mathematical assumptions documented in the source code. Each axiom is labeled with its mathematical justification and a note on when it will close (once Mathlib expands).
This is more honest than sorries: it makes the logical dependencies explicit and auditable. You can read the file and immediately see what is proved unconditionally and what depends on external results.
What Is Actually Proved
The formalized results include both unconditionally proved theorems and spectral-theory results depending on documented axioms. Fully machine-verified examples include:
A second category of results — proved via explicitly declared axioms — covers theorems whose proofs depend on established results not yet formalized in Mathlib. Each axiom is labeled and documented. The dependency map is exact: you can read the Lean file and see precisely which steps invoke which external results.
Every axiom in GPPVerify is an explicitly labeled IOU. The logical architecture is verified. The external inputs are documented. Nothing is hidden.
Current Axioms and Future Closure
Formal verification checks logical structure, not truth assumptions. A theorem in Lean proves what it claims given its axioms. Whether those axioms correspond to established mathematics is a question for the community — and GPPVerify documents this with complete transparency.
Currently, eight axioms remain in RHSpectralMultiplicity.lean:
- riemannZeta_conj_axiom: Conjugation identity (closure: analytic continuation in Mathlib)
- schwartz_integral_clm_axiom: Integration as CLM (closure: SchwartzMap.integrable in Mathlib)
- schwartz_exp_not_tempered: Exponential growth (closure: ~150 lines of Schwartz infrastructure)
- K_compact, K_trace_class: Adelic theory (closure: Tate's thesis formalization)
- plancherel_atom_one, meyer_spectral_weil: Spectral weight (closure: Duke 2005 theory)
- arithmetic_admissibility: The Riemann Hypothesis itself
Three of these have clear Mathlib closure paths and are now being actively formalized. The adelic axioms require substantial new mathematics, which we are prepared to formalize ourselves if needed.
The Dependency Map
One of the most useful outputs of the formalization is the theorem dependency graph. The blueprint site at lean.goldenphysics.org renders this graph interactively. Each node is a theorem. Green nodes are proved clean. Yellow nodes depend on declared axioms. The edges show which results depend on which.
This graph did not exist before formalization. The informal papers contain a logical structure, but that structure is implicit — embedded in prose, indexed by page numbers rather than dependency relations. Making it explicit required formalizing the entire argument, and the result is a precise map of what has been done and what remains.
Why Independent Research Needs This
Independent researchers face a credibility problem that institutional researchers do not. There is no department, no co-authors, no seminar audience providing informal verification. Claims must stand entirely on the quality of the written argument. That is a high bar to clear, and it should be.
Formal verification raises that bar further and simultaneously clears it. A Lean proof that compiles is not a claim — it is a fact about a mathematical object, checkable by anyone with a Lean installation. The verification is not an opinion. It does not depend on the reviewer's expertise or patience. It either runs or it does not.
GPPVerify is the infrastructure for making that standard apply to the ONON framework. Every paper published under the Golden Physics Project is being progressively formalized. As Mathlib grows, the remaining axioms close. The long-term goal is a fully closed formalization — a proof that no human reviewer needs to trust because no step asks for trust.
Technical Details
Stack: Lean 4 (v4.19.0+) with Mathlib 4.19.0. Build system: Lake. CI: GitHub Actions on every push to main.
Verification standard: A theorem compiles without sorry or unapproved axioms if and only if it is machine-verified. All named axioms are documented in-code with proof sketches and closure conditions.
Repository: goldenphysicsproject/website, subdirectory lean/GppVerify/. The main entry point is GppVerify.lean.
Modules:
CoreTheorems.lean— 12 core theorems on involutions and shadow symmetryHaarSelfDuality.lean— Haar measure invariance (3 theorems, fully verified)RHSpectralMultiplicity.lean— RH via spectral multiplicity (conditional on 8 axioms)RiemannZetaConjugate.lean— Conjugation identity (stages 1–2 complete)WeilPositivity.lean— Yakaboylu's RH equivalence (main result sketched)SchwartzSupport.lean— Schwartz space infrastructure (CLM closure path)
Blueprint: Available at lean.goldenphysics.org. Interactive dependency graph coming soon.