A Lean 4 formalization of the ternary (weak) Goldbach theorem, with an explicit audited finite and computational trust boundary.
theorem-proving prime-numbers formal-verification number-theory mathlib computer-assisted-proof goldbach-conjecture analytic-number-theory lean4 formalized-mathematics circle-method ternary-goldbach
-
Updated
Jul 27, 2026 - Lean