3 Conjectures Formally Solved

9-Point Planar Configuration Bounds

The model extracted the exact algebraic Cartesian coordinates for Lothar Piepmeyer's 9-point planar configuration using the algebraic seed constant x = (1+√2)√(2-√3) and formally verified the DistancesSeparated bounds over all 9 points.

To avoid ring and norm_num timeouts over the highly nested radicals, the model autonomously constructed a custom Term Rewriting System mapping the Euclidean distances to a finite set.

Coprime Sums of Reciprocals

Resolves the erdos_307_coprime undergraduate variant. The proof formally verifies the known configuration sets {1, 5} and {2, 3}.

The model demonstrated that the product of the sums of their reciprocals is exactly 1, satisfying all pairwise coprime and disjoint constraints of the problem statement.

max013AffineTranslates n ≤ n²

The model proved the trivial upper bound for Green's Open Problem 24. The failure-and-correction trajectory demonstrated reasoning under compiler feedback, not memorization.

In previous attempts, the model hallucinated Nat.sSup_le, then corrected to sSup_le (wrong type class), and finally verified using csSup_le (conditional supremum) and constructed the correct nonemptiness witness.

V2 Zero-Trust Pipeline

Migrated to Lean's official Comparator. No agent self-reports are trusted.

How It Works

You don't need to trust us. The Lean 4 kernel is the arbiter.

When lake lean exits with code 0 and #print axioms shows only standard axioms (propext, Classical.choice, Quot.sound), the proof is mechanically verified.