Brandon Charles Emerick

URB #517 — Lean 4 Formal Proofs for TI Sigma Mathematical Claims

2026 · Zenodo (CERN European Organization for Nuclear Research)

We present formal Lean 4 proofs for the core mathematical claims of TI Sigma theory. Lean 4 is a dependently-typed theorem prover with the Mathlib4 library providing extensive real and complex number infrastructure. The proofs …