Formal verification — Lean 4 · Coq · Agda · Isabelle¶
The formal layer is the machine-checked wing of the AB-Cloud program. Four independent proof assistants certify the exact algebraic skeleton of the verification suite, and the Lean 4 executable re-derives the frozen reference numbers of the flagship run directly from the raw ζ-zero dataset — an exit-code-gated CI check, not a promise.
Why¶
The 10-language suite answers "could this be a numerical accident?". The formal layer answers the next question — "who verifies the verifier?":
- Exactness where exactness is possible. The algebraic skeleton — the residual sum behind \(b(N) = \tfrac{1}{N}\sum_{k\le N}|\gamma_k - \tilde\gamma_k|\), the Gram offset lattice behind \(\tilde\gamma_k = 2\pi k / W(k/e)\), the flux certificates, the Hurwitz group orders and the trace identity \(\operatorname{Tr}(AB) = \operatorname{Tr}(BA)\) — is proved, not computed.
- A 12th language, inside a proof assistant. The Lean executable is a dependency-free Float64 port of the Python reference pipeline (Lambert W → Gram points → b(N) ladder → unfolded spacings → GUE CDF → KS / Cramér–von Mises → log–log fit) reading the same frozen dataset.
- CI gates.
formal.ymlcompiles all four assistants on every push; the Lean executable fails the build if any frozen number drifts beyond its committed tolerance.
The re-derivation ledger¶
lake exe abcloud-verify (in formal/lean4/) currently reproduces
8/8 frozen reference checks with Δ = 0.000000:
| Check | Recomputed (Lean 4) | Frozen reference | Tolerance | Verdict |
|---|---|---|---|---|
| b(100) | 3.0586168316 | 3.0586168316 | 1e-6 | PASS |
| b(500) | 2.1928840613 | 2.1928840613 | 1e-6 | PASS |
| b(1000) | 1.9321062630 | 1.9321062630 | 1e-6 | PASS |
| b(5000) | 1.4942244142 | 1.4942244142 | 1e-6 | PASS |
| KS distance D | 0.0310483738 | 0.0310483738 | 5e-4 | PASS |
| Cramér–von Mises W² | 1.5383040905 | 1.5383040905 | 5e-3 | PASS |
| Decay slope | −0.1831023444 | −0.1831023444 | 1e-3 | PASS |
| Decay R² | 0.9946087105 | 0.9946087105 | 1e-3 | PASS |
The reference block is generated by the Python reference implementation
(verification/python/ab_cloud_verify.py) from the same frozen Odlyzko
dataset — so the agreement is a genuine cross-language result: the 12th
implementation of the same mathematics, living inside a proof assistant.
What is machine-checked (exact layer)¶
| Statement | Lean 4 | Coq | Agda | Isabelle/HOL |
|---|---|---|---|---|
| b(N) sum nonnegativity | ✅ | ✅ | ✅ by type | ✅ |
| Monotone accumulation (Test 2 discipline) | ✅ | — | ✅ | ✅ |
| Additivity over ledger splits | ✅ | ✅ | ✅ | ✅ |
| Triangle stability | ✅ | ✅ | — | ✅ |
| Fixed-point mean ≥ 0 | ✅ | ✅ | ✅ by type | ✅ |
| Gram lattice positivity + monotonicity | ✅ | ✅ | ✅ by type | ✅ |
| Flux equality certificate | ✅ | ✅ | ✅ | ✅ |
| Magnetic translation q(p+1) = qp + q | ✅ | ✅ | ✅ | ✅ |
| |PSL(2,7)| = 168 · |PSL(2,8)| = 504 · |PSL(2,13)| = 1092 | ✅ | ✅ | ✅ | ✅ |
| Klein orbit decomposition 28+21+7+7+1 = 64 | ✅ | ✅ | ✅ | ✅ |
| Tr(AB) = Tr(BA) for 2×2 matrices | ✅ | ✅ | ✅ | ✅ |
Quick start¶
cd formal/lean4
lake build && lake exe abcloud-verify
Toolchain pinned in lean-toolchain (v4.19.0); no Mathlib — the build
finishes in under a minute.
cd formal/coq
coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq -j2
cd formal/agda
agda -i . -i . ABCloud.agda
Builtins only — no standard-library dependency.
isabelle build -D formal/isabelle
Imports Main only; works with Isabelle2024/2025.
Honesty notes¶
- Nothing here proves the Riemann Hypothesis — it proves the arithmetic the numerical program stands on, and re-derives its numbers.
- The KS p-value is reported informationally but not tolerance-checked (exponentially libm-sensitive); D, W², the b(N) ladder and the fit are gated instead.
- All four developments have zero external dependencies — the audit surface is the repository itself.
Full details and the design notes: formal/README.md.