On the Nature of Nature is the title of my book. The framework developed through that work is the Shadow Framework. GPPVerify is the Lean 4 repository where its mathematical claims are sorted into four categories that matter: proved, conditional, numerically supported, and open.
sorry does not mean “the whole theory is proved.” The repository also counts explicit axioms and deliberately parked True := trivial stubs. Those are open mathematics, not proofs. The distinction is enforced precisely because a clean compiler result by itself can otherwise be misleading.How the work is sorted
Every statement in the formalization lands in one of four places. Proved means a kernel-checked theorem with no custom axiom. Conditional means a theorem whose hypothesis is named in its own statement. Numerically supported means the evidence lives in the exploratory repository, where nothing is claimed as proved. Open means a named, counted placeholder. The formalization has grown enormously, and the audit scripts grew with it: tautologies, blueprint entries that point nowhere, and landing-page claims that outrun the tree all fail the build.
The result is a substantial kernel-checked core and a sharp map of what remains.
Examples of genuinely closed mathematics
The Haar self-duality layer and the functional-equation machinery are formalized without custom axioms.
Gr(2,4) is modelled as the type of two-dimensional subspaces of ℂ⁴, and orthogonal complement is a genuine involution of it: the geometric ℤ₂ used by the shadow construction.
RH is equivalent to positivity of the paired Weil form, proved in both directions. Holographic reflection positivity holds exactly when there are no off-equator mirror pairs.
In the centered coordinate z = s − ½ the two half-flips z ↦ −z and z ↦ z̄ generate the quartet {±δ ± iγ}, and RH is equivalent to the vanishing of the odd part of every zero, stated against Mathlib’s own Riemann Hypothesis.
∫₀^∞ ts−1/sinh t dt = 2(1−2−s)Γ(s)ζ(s) for every real s > 1, with exact special values in place of numerical checks.
Each Euler factor is a Poisson kernel; the von Mangoldt current is the excess group delay of the prime’s Blaschke channel; and the Schatten threshold is exact: the second-order determinant fails and the third-order one works at σ = ½.
Subgroup states of ℤ/Nℤ have Gram matrix gcd(d,e)/√(de), the finite Fourier transform exchanges vd and vN/d, and the Möbius parity vector is an eigenvector with eigenvalue ∏(1−p−1/2).
Fisher-zero log-concavity, globalizing the prime inner channels, static Bost–Connes projections, and diagonal reweighting of the prime Hilbert space are each proved not to work, so each route is explored once.
The critical line is appearing structurally
One of the cleanest recent results concerns the half-density dilation character
For nontrivial positive scale, the critical line Re(s)=1/2 is exactly the locus on which this character has unit modulus. The shadow involution s ↦ 1−s sends it to its reciprocal:
That does not prove RH. It does show that the ubiquitous one-half is not being inserted by hand at this layer: it is the center of the unitary half-density representation.
What is not proved
The Riemann Hypothesis itself is open in GPPVerify. So are substantial parts of the Yang–Mills, Wightman, twistor-googly, Majorana, and arithmetic-geometry towers. The decisive RH gap is no longer “why one-half?”; it is the global analytic positivity/transport bridge that forces the actual arithmetic zeros onto the unitary locus.
The same discipline applies elsewhere. If a physical theorem depends on a geometric object that has not yet been built in Lean, the correct next move is not to leave the consequence as an eternal stub. It is to formalize the object and prove the prerequisite.
Three numbers that must always be reported together
This accounting rule was adopted after the repository itself exposed how easy it is to make a formalization sound more complete than it is. That lesson is now part of the method.
The next phase
GPPVerify is moving beyond isolated consequences. The next serious phase is foundational: genuinely formalize the geometry and analysis that the Shadow construction is supposed to live on—Grassmannians, Plücker coordinates and charts, the relevant bundles and dualities, celestial kinematics, measure structures, representation-theoretic objects, and then the physical constructions built on top of them.
That is how the stub count should fall: not by deleting placeholders, weakening statements, or renaming assumptions, but by proving the mathematics underneath them.
Follow the formalization live
The proof tree is public. The live blueprint exposes theorem dependencies; the source repository exposes the actual Lean files, history, CI, and audit scripts.