analysis@home

Spare AI, turned into proven math.

A crowdsourced corpus of machine-checked theorems about algorithms — not just that they're correct, but how fast they run: worst-, best- and average-case cost, even the limiting distribution. Every proof is re-checked line by line by a proof-assistant kernel (Rocq/Coq, Lean, Agda, Isabelle). Bring your own LLM, prove an open job, open a PR — CI runs the kernel. Verified, not trusted.

Contribute a proof → GitHub repo

0/0 backend targets kernel-verified across 4 proof assistants.

How it works (30 seconds)

1 · Pick a job. An open theorem about an algorithm's cost or correctness, with a ready-to-paste prompt.
2 · Prove it. Paste the prompt into your own LLM (Claude, …); take the proof it returns.
3 · Kernel checks. Open a PR. CI runs the proof assistant; if every line holds it's merged and you're credited.
The server never runs an LLM and never sees your credentials. The kernel does the believing — so anyone (or anything) can contribute and nobody has to be trusted.

What's proven so far

By cost claim:

By area:

Spanning sorting & searching, divide-and-conquer recurrences (the master-theorem regimes), graph algorithms (BFS/DFS O(V+E), shortest-path relaxation), data structures (AVL, union-by-rank), number theory, and many summation identities — all kernel-verified.

Research highlight: verified average-case cost

Worst-case complexity has been mechanized before; average-case (expected) cost is comparatively unformalized. Our angle is a small reused Rocq library plus a computation oracle that checks the cost statement before it is proved.

A reused library. framework/Permutations.v (axiom-free) proves the permutation core (perms_correct, length_perms = n!, NoDup_perms) and one general counting lemma count_first_value. Two results reuse it: quicksort and records.
Quicksort, end to end. The average 2(n+1)Hₙ − 4n is kernel-checked from an instrumented comparison counter — cmp → cmp_eq_pairsum → compared_count (2·n!/d per pair) → the closed form — not just a recurrence.
Kept honest by an oracle. A wrong cost statement survives a kernel proof; tools/fault_corpus.py shows the deterministic enumeration oracle catches 12/12 plausible-but-wrong closed forms (random testing can miss the near-misses).
A unit may Require Import the framework: the verifier precompiles it from source, so it is still kernel-checked end to end while contributors build on the library instead of re-deriving it.

Two tracks: compute, then prove

The conjecture track (pure-Python computer algebra + exhaustive enumeration) computes the cost distribution and its limiting law — fast, but not trusted. The verify track promotes the provable part (the exact mean) to a kernel-checked theorem.

Computed distributions & limit laws (not trusted)

Conjecture-track jobs — promote a computed mean to a theorem

You can contribute to the cost-statistics track two ways. (1) Promote: these distributions have an exact computed mean but no kernel-checked twin yet — prove the mean as a theorem in a new work unit and link it with conjecture_artifact. (2) Compute: add a brand-new distribution/limit-law to tools/conjecture/conjecture.py (pure stdlib); CI re-runs the solver and rejects results that don't reproduce from the committed script. Twins wanted: 0.

Pick an open job

Each is a port of a kernel-verified theorem to another proof assistant. Copy the prompt into your LLM, then Create a PR. Showing the first 30 of 0 open jobs.

Full verification matrix

Show all 0 units × 4 backends
Bite-sized leaves (good first contributions) — 0

Hard theorems are split into small, independently kernel-checked leaves (★ = difficulty, green = ★1–2).

Contributions licensed Apache-2.0 (code) / CC-BY-4.0 (proofs). Repo: github.com/.