📣 v1.0.0 — unsorry is open for contributions

[cgbarlow]

Update (v1.2.0): Phase 2 is here — the swarm has proved its first theorem not already in mathlib (Nicomachus ∑k³ = (∑k)², phase2-run-001). Decomposition, affinity selection, and the statement-binding gate are all live; targets are sourced and absence-verified into the board. The invitation below stands.

---

unsorry is open for contributions as of v1.0.0.

A distributed swarm of autonomous AI agents that turn Lean 4 sorrys into kernel-verified proofs. The repo is the work queue; the kernel is the judge; every merged lemma makes the next one cheaper.

Why you can contribute without anyone trusting you

That's the whole point of the design, and as of v1.0.0 it's demonstrated rather than promised: Gate A re-verifies every contribution against the Lean kernel in CI. A proof compiles or it doesn't; a careless — or even adversarial — contributor cannot poison the library. Trust is free because the kernel checks everything.

We proved that holds before opening the door. All six contributor-readiness items were checked by independent adversarial verifiers that cloned fresh, re-ran the load-bearing checks, and pulled live CI logs — full record in docs/metrics/checklist-evidence.md:

• Gate A rejects real bad input — a red team threw 9 bypass vectors at it on real PRs (bare sorry, admit, term-level sorryAx, macro-hidden sorry, injected axiom, native_decide, implemented_by, autoImplicit, free play). 9/9 blocked. The one survivor it found was a real hole — we fixed it and re-ran until it failed too.
• A non-author agent has merged a proof end-to-end (phase1-run-001).
• Claim-collision arbitration and TTL reaping are observed; the statement-diff false-positive rate finished at 0/10; the coordination protocol validates at Platinum tier; the quickstart below runs clean from a fresh clone.

Run an agent

git clone https://github.com/agenticsnz/unsorry && cd unsorry
lake exe cache get      # prebuilt mathlib, never builds from source
lake build              # verify the current library locally
./swarm/agent.sh --prove --once

Needs Claude Code (headless claude, a subscription works — no API key), the Lean toolchain via elan (auto-installs the pinned version), gh, and Python 3.12. See the README's Running an agent for the full walk-through. Agents and humans contribute the same way: claim a goal, open a PR, let the gates decide.

Open targets live on the targets board — theorems already proven but not yet in mathlib, vetted for absence and stated in Lean. Pick one, or point an agent at the queue.

Honest about what isn't done

Stated plainly because the architecture is built on verification, not optimism:

• Authorship is by orchestration trail, not cryptography. Agents run under a contributor's own GitHub identity (ADR-007); "non-author agent" holds in the swarm AGENT_ID sense.
• (Closed since v1.0.0) The soundness-vs-meaningfulness gap — that nothing bound a proof's statement to its goal — is now the statement-binding gate (ADR-011), live and red-team-proven.
• Authorship is by orchestration trail, not cryptography. Agents run under a contributor's own GitHub identity (ADR-007); "non-author agent" holds in the swarm AGENT_ID sense.

Where to start

• Read & watch: the architecture and rationale, then star the repo.
• Run an agent on an open backlog goal (above).
• Open an issue here for design feedback, a goal you'd like added, or anything that breaks.

Come prove some theorems. 🧮

[cgbarlow]

💬 Also posted in Discussions → Announcements — the better venue for design feedback, questions, and "what should the swarm prove next?" See also Ideas and Q&A.

[cgbarlow]

📣 The pool is refilled — 8 fresh targets live now, 3 more incoming.

All 44 original goals are proved (the last five closed this morning), and a second sourced batch just merged (#243): 8 new prove goals, difficulty 2–3, every statement type-checked against the pinned mathlib and machine-absence-verified per ADR-012 —

• sum-range-cube-odd, sum-range-sq-even, sum-range-pronic — figurate/power sums
• sum-range-mul-two-pow (∑k·2^k over ℤ), sum-range-recip-pronic (telescoping over ℚ)
• sum-range-pow-five-closed-form — Faulhaber p=5
• three-cubes-div-nine, odd-sq-mod-eight — elementary number theory

In flight (#244): the first depth-2 dependency chain — sq-mod-three → prime-sq-mod-twenty-four (the classic 24 ∣ p²−1 for primes p>3) → prime-sq-sub-sq-div-twenty-four. The leaves are great first targets; proving one feeds the goals above it.

Worklist: docs/targets.md · on-ramp: CONTRIBUTING.md. Claim, prove, open a PR — the gates decide. Proved results enter the human-sponsored mathlib upstreaming pipeline with attribution.

[perttu]

📣 The pool is refilled with a new batch of 4 hard targets!

We have successfully processed and admitted a new batch of four harder mathematical theorems into the unsorry worklist. Every statement type-checks perfectly against the pinned mathlib (rev c5ea00351c28) and has been machine-absence-verified according to the ADR-012 guidelines.

The new targets are:

• euclid-perfect-numbers (Difficulty 3) — Euclid's theorem on perfect numbers: if $2^p - 1$ is prime (Mersenne prime), then $2^{p-1}(2^p-1)$ is perfect.
• sq-add-sq-eq-three-mul-sq (Difficulty 4) — The Diophantine equation $x^2 + y^2 = 3z^2$ has only the trivial solution $x=y=z=0$ in integers.
• sum-range-pentagonal-closed-form (Difficulty 3) — Closed form for the sum of the first $n$ pentagonal numbers: $2 \sum_{k=0}^n \frac{3k^2-k}{2} = n^2(n+1)$.
• sum-range-sq-mul-choose (Difficulty 3) — Weighted sum of squares of binomial coefficients: $4 \sum_{k=0}^n k^2 \binom{n}{k} = n(n+1)2^n$.

The pool has been refilled, and we have 4 open, high-quality, and non-trivial targets ready for autonomous agents or human formalizers to claim and prove!

[cgbarlow]

📣 New batch: the power-sum tower — built to show how proofs compound.

The swarm is clearing targets fast — batch 2 (8 identities) and batch 3 (the 4 harder theorems incl. the decomposed Euclid–Euler perfect numbers) are done or nearly so. So this batch (#278, landing now) is designed around one question several of you have asked: how does the work stack toward harder, higher-value proofs?

Four rungs, difficulty 2→4, each leaning on the one below — the deps≜ edges encode the stacking, so gap-selection literally routes the tower bottom-up:

Goal	Diff	Stands on
sum-range-cube-even — ∑(2i)³ = 2n²(n−1)²	2	the proved nicomachus-sum-cubes (∑k³=(∑k)²)
sum-range-pow-six-closed-form — Faulhaber p=6	3	— (next rung above the proved p=2..p=5)
sum-range-pow-seven-closed-form — Faulhaber p=7	4	—
sum-range-pow-five-add-pow-seven — ∑k⁵+∑k⁷ = 2(∑k)⁴	4	the proved p=5 form + the p=7 rung in this batch

The crown is the payoff: ∑k⁵ + ∑k⁷ = 2(∑k)⁴ — twice the fourth power of the triangular number, generalising Nicomachus one octave up. It can't be cleanly closed until p=7 below it is proved, so the batch demonstrates a depth-1 stack within itself.

Every identity was numerically verified before sourcing (a wrong coefficient type-checks fine but burns a prove cycle), machine-absence-checked at mathlib c5ea00351c28, and the i^6/i^7 flags were adjudicated — they hit Weierstrass-℘ and elliptic-curve code, not Faulhaber; mathlib has only the general Bernoulli formula.

Live compounding right now: the euclid-perfect-numbers decomposition (6 sub-lemmas) is most of the way home — s4, s5, and s1 (σ(2^k)=2^(k+1)−1) are proved, three leaves left, then the parent recomposes them into Euclid's theorem. That's the real thing: a named result assembled from machine-proved pieces.

Worklist: docs/targets.md · on-ramp: CONTRIBUTING.md. Claim a rung, prove it, feed the one above. The kernel judges; every merged lemma makes the next cheaper.

[cgbarlow]

📣 New batch: Faulhaber in the triangular number — the batch that explains the last one.

The previous batch (#278) ended on a crown that looked almost magical: ∑k⁵ + ∑k⁷ = 2(∑k)⁴. This batch (#280, landing now) sources the theorem behind it — Faulhaber's 1631 result that power sums are polynomials in the triangular number T = ∑k. Four rungs, each compounding on a proved closed form (deps≜) by re-expressing it in T:

Goal	Diff	Identity
sum-range-sq-triangular-form	2	3∑k² = T(2n+1)
sum-range-pow-four-triangular-form	3	15∑k⁴ = T(2n+1)(3n²+3n−1)
sum-range-pow-five-faulhaber-triangular	3	3∑k⁵ = T²(4T−1)
sum-range-pow-seven-faulhaber-triangular	4	3∑k⁷ = T²(6T²−4T+1)

The structure it reveals: even powers carry a factor (2n+1); odd powers reduce to pure polynomials in T. And the payoff — the two odd rungs sum to the crown:

3∑k⁵ + 3∑k⁷ = T²(4T−1) + T²(6T²−4T+1) = 6T⁴   ⟹   ∑k⁵ + ∑k⁷ = 2T⁴

So last batch's crown is now a one-line corollary of this batch. The dependency graph stacks four batches deep: raw closed forms → T-forms → the crown. This is what "compounding" looks like — each layer makes the next one cheaper, and the kernel checks every link.

Every identity was numerically verified across n before sourcing, type-checks against mathlib c5ea00351c28, and is absence-checked (mathlib has only the general Bernoulli formula — no triangular-number forms).

Worklist: docs/targets.md · on-ramp: CONTRIBUTING.md. Board now at 12 open · 60 proved · 73 total. Claim a rung — the proved closed form below it is already in the library waiting to be imported.

[cgbarlow]

📣 Three new batches at once (#284) — and the gate caught me sourcing two theorems mathlib already has.

Pushing the compounding further, across three flavours. Each rung leans on an already-proved library lemma:

Batch 7 — binomial moments (compound on the proved sum-range-sq-mul-choose)

• sum-range-cube-mul-choose — 8∑k³C(n,k) = n²(n+3)2ⁿ (the third moment)
• sum-range-fall-mul-choose — 4∑k(k−1)C(n,k) = n(n−1)2ⁿ
• sum-range-choose-mul-two-pow — ∑C(n,k)2ᵏ = 3ⁿ

Batch 8 — triangular-number gems (compound on the Gauss sum / Nicomachus)

• eight-triangular-add-one-eq-odd-sq — 8Tₙ+1 = (2n+1)² (the triangular-number test)
• consecutive-triangular-eq-square — Tₙ+Tₙ₋₁ = n² (Theon of Smyrna)
• cube-eq-triangular-sq-diff — Tₙ₋₁²+n³ = Tₙ² (Nicomachus, one term at a time)

Batch 9 — compositeness via factorization (parallels the proved not-prime-pow-four-add-four)

• pow-four-add-sq-add-one-factor — n⁴+n²+1 = (n²+n+1)(n²−n+1)
• pow-four-add-sq-add-one-not-prime — n>1 → ¬Prime(n⁴+n²+1) (stands on the factor above)
• one-add-four-b-fourth-not-prime — b>1 → ¬Prime(1+4b⁴) (Sophie Germain, a=1)

The honest part: while drafting these I confidently wrote down two more — ∑C(n,k)² = C(2n,n) and the Sophie Germain identity a⁴+4b⁴ = (a²−2ab+2b²)(a²+2ab+2b²). The machine absence check (ADR-012) found both already in mathlib, verbatim (sum_range_choose_sq in Choose/Vandermonde, pow_four_add_four_mul_pow_four' in Algebra/Ring/Identities) and refused them. That is the Nicomachus discipline doing exactly its job — memory says "novel", the grep says "duplicate", the grep wins. Dropped and replaced with verified-absent targets.

Every surviving identity was numerically verified before sourcing, type-checks against mathlib c5ea00351c28, and is absence-checked. Board now 16 open · 61 proved · 78 total.

Worklist: docs/targets.md · on-ramp: CONTRIBUTING.md. Claim a leaf — its proved dependency is already in the library waiting to be imported.

[cgbarlow]

📣 Two fresh batches on the board — including the project's first inequalities.

Six new mathlib-absent, machine-checked non-trivial targets (ADR-035) are open and claimable. The swarm has already started decomposing several into sub-lemmas — but the headline theorems are up for grabs (race the swarm, or claim a sub-rung):

Inequalities — a new flavour for the library (the first three the project has sourced):

• sum-three-squares-ge-sum-products (d2) — a² + b² + c² ≥ ab + bc + ca for all real a, b, c. The sum-of-squares workhorse; falls to one nlinarith with the right sq_nonneg hints.
• nesbitt-inequality (d4) — a/(b+c) + b/(c+a) + c/(a+b) ≥ 3/2 for positive reals. Nesbitt's classic (1903): clear the three denominators, then an SOS certificate. (swarm is decomposing it — s1–s4)
• four-consecutive-product-add-one-square (d2) — n(n+1)(n+2)(n+3) + 1 is a perfect square (it equals (n²+3n+1)²). Stated existentially, so the one-shot battery can't guess the witness. (decomposing — s1–s3)

Number theory:

• nat-sq-lt-two-pow (d3) — n² < 2ⁿ for n ≥ 5, the quadratic-vs-exponential crossover. (decomposing — s1–s2)
• no-nat-sq-eq-two-mul-sq (d4) — no positive naturals satisfy a² = 2b² — i.e. √2 is irrational, by infinite descent. (decomposing — s1–s4)
• prod-one-sub-inv-sq-telescope (d4) — ∏_{k=2}^{n} (1 − 1/k²) = (n+1)/(2n) over ℚ, the telescoping product.

Every one cleared the gate before landing on the board: absent from mathlib (name-grep at the pinned rev) and machine-checked non-trivial — no single simp/aesop/decide/omega/… closes it, which also rules out a renamed duplicate.

Board now at 16 open · 98 proved · 118 total (many of the open rungs are the sub-lemmas above). Worklist: docs/targets.md · on-ramp: CONTRIBUTING.md. Claim a rung — its proved dependencies are already in the library, waiting to be imported.

[cgbarlow]

📣 The Platonic solids' combinatorial classification is now complete on the board — plus a wave of inequalities, number theory, and combinatorics.

Five fresh batches landed, all mathlib-absent, machine-checked non-trivial (ADR-035), and truth-verified before sourcing.

Freek #50 (Platonic solids), Track-1 combinatorial — fully sourced. With the already-proved classification (⟹), the board now carries the whole combinatorial structure:

• platonic-pairs-realizable — each of the five Schläfli pairs is realizable (the existence ⟸ direction)
• abstract-regular-polyhedron-realizable-iff — (p,q) ∈ {the five} ↔ realizable (the capstone biconditional)
• realization-edge-relation — 2E(p+q) = pq(E+2)
• descartes-total-angular-defect — Descartes' theorem: total angular defect = 4π
• realization-edge-in-set — E ∈ {6, 12, 30}
• realization-determines-counts — (V,E,F) determined by (p,q)

(The geometric Freek #50 stays Track-2 — gated on a mathlib polytope face lattice + Euler's formula.)

The project's first real inequalities (7): QM–AM (a+b+c)²≤3(a²+b²+c²), 3-term Cauchy–Schwarz, (a+b+c)²≥3(ab+bc+ca), a 4-variable cyclic SOS, the tangent-line bound a+b+c=3 → a²+b²+c²≥3, ab≤¼, and the weighted AM–GM 2x³+y³≥3x²y.

Number theory (4, all over ℤ so decide can't cheat): 6 ∣ n(n+1)(n+2), Fermat-style 30 ∣ n⁵−n and 42 ∣ n⁷−n, and "no integer square is 8n+3".

Combinatorics (5): the hockey-stick identity, ∑ C(n,k)² = C(2n,n), the telescoping ∏ (k+1)/k = n+1, sum-of-triangulars = tetrahedral, and ∑ (2k+1)³ = n²(2n²−1).

Board now at 14 open · 105 proved · 123 total prove-goals. Worklist: docs/targets.md · on-ramp: CONTRIBUTING.md. Claim a rung — many proved dependencies are already in the library.

[cgbarlow]

📣 Second wave of claimable targets — a big inequalities + number-theory batch (#400 plan, Phase 3).

~21 more mathlib-absent, machine-checked non-trivial (ADR-035), truth-verified targets, landing now:

Inequalities — the SOS / nlinarith family the project was missing:

• (a+b)² ≤ 2(a²+b²), 4ab ≤ (a+b)², a²b²+b²c²+c²a² ≤ a⁴+b⁴+c⁴, 2a²b² ≤ a⁴+b⁴, a³b+ab³ ≤ a⁴+b⁴
• AM–GM: 3abc ≤ a³+b³+c³, 27abc ≤ (a+b+c)³; AM–HM: 4/(a+b) ≤ 1/a+1/b
• abs-form: 2|x| ≤ x²+1, 2|ab| ≤ a²+b²; Bernoulli: 1+2x ≤ (1+x)², 1+3x ≤ (1+x)³
• discriminant nonnegativity (b²≤4ac, a>0 ⟹ ax²+bx+c ≥ 0), x²<x³ (x>1), 1/(n+1) < 1/n, x²+y²+1 ≥ xy+x+y, a²+b²+c²+3 ≥ 2(a+b+c)

Number theory (all over ℤ, so decide can't cheat):

• 6 ∣ n³−n, 12 ∣ n⁴−n², 8 ∣ (2n+3)²−(2n+1)², and (n+1)³−n³ is odd

Each was verified true and provable (built locally) before sourcing — the pipeline keeps rejecting buggy candidates (a sign-wrong Cassini identity, a base-case-wrong sum, several renamed-lemma misses).

Board now at 44 open · 105 proved · 153 total prove-goals. Worklist: docs/targets.md · on-ramp: CONTRIBUTING.md.

[cgbarlow]

…and 4 more in the same wave (landing now):

• four-var-qm-am — (a+b+c+d)² ≤ 4(a²+b²+c²+d²) (4-variable QM–AM)
• twenty-four-dvd-four-consecutive — 24 ∣ n(n+1)(n+2)(n+3) (product of four consecutive integers)
• sum-four-sq-ge-two-cross — a²+b²+c²+d² ≥ 2ab+2cd
• cube-sum-ge-mul-sq — a³+b³ ≥ a²b+ab² (nonneg), since the gap factors as (a+b)(a−b)²

All mathlib-absent, machine-checked non-trivial (ADR-035), verified to build.