This page provides verification reports, certificates, and supporting evidence for two separately coordinated Lean formalization efforts: an author-coordinated Codex development and a development coordinated by Daniel Zhou.
The author-coordinated verification reports Level K for all 65 numbered mathematical assertions (64 distinct results), under the documented formalization and statement-correspondence conventions. The reports describe the verification scope and its limitations.
The complete author-coordinated Lean source code and reproducibility scripts will also be made available here.
Author's package
author's report.pdf author's report.md author's certificate.md
Lean formalization and verification materials — Lean 4/Mathlib source code, verification certificates, correspondence audits, and reproducibility instructions.
Daniel Zhou's package