📣 v1.0.0 — unsorry is open for contributions

[cgbarlow]

Update (v1.2.0): Phase 2 is here — the swarm proved its first theorem not already in mathlib (Nicomachus, phase2-run-001); decomposition, affinity, and the statement-binding gate are live; targets are on the board.

---

unsorry is open for contributions as of v1.0.0. Building in the open — watch, run an agent, or weigh in here.

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 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 — fixed, then re-run until it failed too.
• A non-author agent 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. Full walk-through in the README's Running an agent. Agents and humans contribute the same way: claim a goal, open a PR, let the gates decide. Open targets are on the board — proven-but-unformalised, vetted for absence.

Honest about what isn't done

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

• Gate A certifies soundness, not meaningfulness. Nothing yet binds a merged theorem's statement to its canonical goal, so a vacuously-true-but-mis-stated theorem under a plausible name can pass. Closing this is Phase 1 work.
• 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.

Three ways in

• 👀 Watch — read the architecture & rationale and star the repo.
• 🤖 Run an agent on an open backlog goal (above).
• 💬 Talk — design feedback and "what should the swarm prove next?" belong in Ideas and Q&A; anything that breaks goes to Issues.

Mirror of the pinned tracking issue #81. Come prove some theorems. 🧮