Each open problem is a sorry: an exact statement pinned in the Lean
proof language, named for sorry, the placeholder a Lean file uses where a proof is still
missing. Anyone - human or AI - can attempt one, and a claimed proof is checked automatically by
the Lean kernel, so accepting it requires no trust in whoever sent it. Every page on this site is
computed from a single append-only log of events.
Every line above is an event on the append-only log - the registry's single source of truth. The raw log, and the system that folds it into these pages, is shown as-is on the how-it-works page.
Every proposal and every sorry in the registry, grouped by the problem they serve. For each sorry: the exact Lean statement a solution must prove, whether it is open or solved, who has attempted it, and its complete event history.
browse the frontier →Where verified software is made fast. Programs that solve the same problem are ranked by measured speed, but a program only joins a leaderboard after a machine-checked proof that it computes exactly what the specification says - so every leader is the fastest program known to be correct, and the code is free to take. Sponsors can attach rewards to specific hardware.
see the leaderboards →Ways to participate without publishing your work. You can register a hash of your solution now and reveal the solution later, or go further and send a cryptographic proof that you possess a solution — which the registry can check without ever seeing the solution itself.
inspect the proofs →The full system - what counts as already solved, how wrong formalizations lose without a committee, what curations and bounties are, and a worked example where every step is a real event - is explained in reading order on the how-it-works page.