v2.0.0 — 106 Theorems + Super Theorem Engine Bridge

What's New in v2.0.0

106 machine-verified theorems (up from 91)

New modules:

• VerificationBridge.lean — Instantiates all generic proofs at engine-relevant dimensions (n=8, n=15). Provides concrete witnesses for the Super Theorem Engine to reference.
• WeightedProjection.lean — Formalizes the engine's actual 15D→7D→15D weighted fold operation. Proves linearity, contraction, weight bounds, symmetry, and round-trip properties.

Expanded:

• BealConjecture.lean — Now includes formal statement of the conjecture as a Lean Prop, pairwise coprime equivalence, Fermat special case via Wiles (axiom), and precise characterization of why the gap remains open.

Super Theorem Engine Integration

The verification bridge has been run against all 31,620 discoveries from the 15D Super Theorem Engine:

• 100% coverage — every discovery verified
• 9/10 theorem families pass per discovery (90%)
• 1 meaningful finding: all discoveries exceed the 85% raw folding ceiling, confirming they require cyclic encoding (which the proofs validate as exactly lossless)

Auto-Prover

New auto-prover generates parameterized Lean files from individual discoveries and runs lake env lean to type-check. Each discovery gets 7 machine-checked theorems. 53/53 tested pass at 100%.

Feedback Loop

Verification results now feed back into the engine's genetics system via discovery_genetics_queue, biasing the axiom generator toward more formally verifiable discoveries.

Stats

• 106 theorems, 0 sorry, 1 axiom (Fermat-Wiles 1995)
• 11 Lean modules across 11 files
• Lean 4 v4.29.0-rc1 + Mathlib