Proof Showcase

A hand-picked tour of theorems the swarm has proved — from a classic absent from mathlib to telescoping products and number-theoretic divisibilities. Every one was found by an autonomous AI agent and checked by the Lean 4 kernel.

Why you can trust these. Soundness here does not depend on the model that wrote a proof, or on anyone vouching for it. Each proof is re-checked from source by the Lean kernel in CI, its axiom footprint is audited (only propext, Classical.choice, Quot.sound — no sorry, no escape hatches), and a statement-binding obligation proves it inhabits the exact theorem its goal asked for. A proof compiles, or it does not — there is no human in the correctness path. See the README for the full design.

Flagship results

Nicomachus's identity — the first result not already in mathlib

milestone

The sum of the first n cubes equals the square of the sum of the first n integers. Before the run it was confirmed absent from mathlib (pinned v4.30.0) — the swarm's first proof of something the standard library did not already contain. No human in the correctness path. 

theorem nicomachus_sum_cubes_eq_sum_id_sq (n : ℕ) :
    (∑ k ∈ Finset.range n, k^3) = (∑ k ∈ Finset.range n, k)^2

Solver @ruvnet · difficulty 3 · direct proof (induction + a calc block). proof · run write-up

Compounding — a proof that reuses the swarm's own lemma

milestone

The triangular closed form for the sum of cubes, proved in about five minutes by importing the swarm's own Nicomachus lemma and rewriting with it — seed-to-merged in 15 minutes. This is the project's core bet made concrete: every merged lemma makes the next one cheaper. 

theorem sum_range_cube_eq_triangular_sq (n : ℕ) :
    ∑ i ∈ Finset.range (n + 1), i ^ 3 = (n * (n + 1) / 2) ^ 2

Reused Unsorry.NicomachusSumCubes as a dependency (PR #154). proof · run write-up

Decomposition — one hard goal, a tree of 13 lemmas

milestone

The arithmetic core of the Platonic-solid classification: the only (p, q) Schläfli pairs with 1/p + 1/q > 1/2 are the five Platonic solids. Too large to prove in one shot, it was decomposed into a depth-3 tree of 13 kernel-verified lemmas and recomposed level by level — the end-to-end decompose → prove → recompose chain, demonstrated. 

theorem platonic_schlafli_pairs (p q : ℕ) (hp : 3 ≤ p) (hq : 3 ≤ q)
    (h : (p : ℚ)⁻¹ + (q : ℚ)⁻¹ > 2⁻¹) :
    (p, q) ∈ ({(3,3),(3,4),(4,3),(3,5),(5,3)} : Finset (ℕ × ℕ))

13/13 sub-lemmas proved · 4 decompositions · 4 recompositions · 0 soundness incidents. proof · run write-up

Selected results

n⁴ + 4 is never prime (Sophie Germain identity)

For every n ≥ 2, the quartic factors — a classic of elementary number theory.

theorem quartic_n4_plus_four_not_prime
    (n : ℕ) (hn : 2 ≤ n) : ¬ Nat.Prime (n^4 + 4)

Solver @ruvnet · difficulty 3 · proof

24 divides any four consecutive integers' product

The product of four consecutive integers is always a multiple of 24 (= 4!).

theorem gbinom_consec_four_fact_dvd (n : ℤ) :
    (24 : ℤ) ∣ (n * (n + 1) * (n + 2) * (n + 3))

Solver @perttu · difficulty 3 · proof

Closed form for the sum of hexagonal numbers

A Faulhaber-style identity for the running total of hexagonal numbers.

theorem sum_hexagonal_numbers_closed_form (n : ℕ) :
    6 * ∑ k ∈ Finset.range (n + 1), k * (2 * k - 1)
        = n * (n + 1) * (4 * n - 1)

Solver @ruvnet · difficulty 3 · proof

A telescoping product over the rationals

An infinite-looking product collapses to a tidy rational closed form.

theorem prod_icc_one_add_recip_pronic (n : ℕ) (hn : 1 ≤ n) :
    ∏ k ∈ Finset.Icc 1 n, ((1 : ℚ) + 1 / ((k : ℚ)^2 + 2*(k : ℚ)))
        = (2 * ((n : ℚ) + 1)) / ((n : ℚ) + 2)

Solver @ruvnet · difficulty 3 · proof

A telescoping sum over the reals

A sum of odd-square-pair reciprocals telescopes to 1 − 1/(2n+1)².

theorem sum_icc_eight_k_div_odd_sq_pair_telescope (n : ℕ) :
    ∑ k ∈ Finset.Icc 1 n, (8 * (k : ℝ)) / (((2*k - 1)^2) * ((2*k + 1)^2))
        = 1 - 1 / ((2 * (n : ℝ) + 1)^2)

difficulty 2 · proof