Euler's Partition Theorem — Lean proofs

The number of partitions of n into distinct parts equals the number into odd parts, formalized in Lean 4 by two prover harnesses from the same blueprint. Each opens in the in-browser Lean editor; the kernel re-checks it live.

• Numina — euler_partition (Mathlib-idiomatic)
  397 lines · #print axioms → {propext, Classical.choice, Quot.sound}
  ▶ Open in live Lean ⬇ Download .lean
• Numina — euler_equiv (no Classical.choice)
  762 lines · #print axioms → {propext, Quot.sound}
  ▶ Open in live Lean ⬇ Download .lean
• Archon — euler_partition (Mathlib-idiomatic)
  377 lines · #print axioms → {propext, Classical.choice, Quot.sound}
  ▶ Open in live Lean ⬇ Download .lean

Written against Mathlib v4.30. The live editor uses its own (latest) Mathlib, so a lemma name may have shifted; the proofs and #print axioms results above are from the pinned build. Source files are the exact, full proofs (download for the byte-perfect copy).