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 June 2026, the core theorems of the ONON framework have been formalized in Lean 4 using Mathlib 4.19.0. The repository is public. The CI pipeline runs on every commit. The build is green.
What “Sorry” Means
In Lean, the sorry tactic is a placeholder that tells the proof assistant to accept a gap without checking it. It is the formal equivalent of "it can be shown that." A proof containing sorry compiles but proves nothing — the compiler is simply being told to trust you.
Eliminating every sorry from a Lean file means the entire logical chain has been verified from first principles down to the axioms of Lean's type theory. No step is assumed. No gap is papered over.
GPPVerify currently contains zero sorry tactics in any proof body. Every theorem that compiles clean is machine-verified in the full sense.
What Is Actually Proved
The formalized results fall into several categories. The cleanest — proved with zero external assumptions — 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.
What It Does Not Prove
Formal verification checks logical structure, not physical truth. A theorem in Lean is a statement about mathematical objects as defined within the formalization. Whether those objects faithfully model physical reality is a separate question that no proof assistant can answer.
More concretely: the Riemann Hypothesis is not proved by GPPVerify. What is proved is that the L² admissibility condition on the adèlic space forces Re(s) = ½, conditional on the axioms declared in the file. Those axioms include the Meyer spectral identity and the Weil explicit formula — established results that are not yet formalized in Mathlib. When Mathlib gains those tools, the axioms close automatically.
This is honest. The alternative — claiming a complete proof while hiding the gaps — is what the sorry tactic enables. GPPVerify uses neither.
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
The repository uses Lean 4 with Mathlib 4.19.0. The build system is Lake. CI runs on GitHub Actions on every push to main. The build target is lake build; a passing build with zero sorry tactics constitutes verification. The repository is at github.com/GoldenPhysicsProject/GPPVerify.
The blueprint is generated by leanblueprint from a LaTeX source in blueprint/src/web.tex and deployed automatically to lean.goldenphysics.org on each successful build. The theorem dependency graph is live and reflects the current state of the repository.