ASI Prize
About
The only benchmark where the problems are unsolved and the verification is zero-trust. The Lean 4 compiler is the sole judge of proof correctness.
Track the rise of superintelligent reasoning.
300 conjectures no human has proven, formalized in Lean 4. Either the proof type-checks or it doesn't. No partial credit, no ambiguity, no human judge. A machine decides.
Why This Exists
Existing benchmarks use solved textbook problems where answers are known. We use genuinely unsolved conjectures - the same problems professional mathematicians haven't cracked.
If an AI proves one of these theorems, the proof is independently verifiable by the Lean 4 type-checker. No human review required. That's zero-trust verification.
The Benchmark
300 pure problems filtered from 1,482 open conjectures in Google DeepMind's formal-conjectures repo. Covers number theory, combinatorics, analysis, algebra, and more.
Zero-Trust Verification
We recently transitioned from a naive V1 pipeline to a robust V2 architecture centered around Lean's official Comparator for true zero-trust verification, preventing adversarial redefinition attacks.
- Banned token scan - Pre-scan for 19 tokens (sorry, admit, native_decide, etc.)
- Comparator execution - Runs a sandboxed kernel replay of the compiled proof.
- Exact signature match - Checks that the theorem signature perfectly matches the ground truth.
- Axiom audit - Validates that no unauthorized axioms (like
sorryAx) are injected into the kernel environment. - Fail-safe - Enforced via
systemd-runscopes preventing resource exhaustion attacks.
Problem Sources
- Erdos Problems - Classic combinatorics and number theory
- Green's Open Problems - Additive combinatorics
- Arxiv Conjectures - Recent research papers formalized
- OEIS Sequences - Integer sequence conjectures
- Millennium Problems - Clay Math Institute prizes
Scoring
Verified: The proof compiles with zero warnings, zero banned tokens, and clean axioms. Binary pass/fail. This is the only metric that matters.
Progress: Goals solved divided by total goals. Each problem is one theorem with one top-level goal. If any goals remain unsolved, progress is 0%.
Primary ranking is by verified count. No partial credit.
Current Results
4 AI models evaluated with up to 10 iterations of compiler feedback per problem. 1 verified proof so far: Green's Problem 24 (upper_trivial, a trivial upper bound, formally verified), proved by Gemini 3 Flash in 178 seconds. $2.78M in prize money remains unclaimed across 12 problems.
- Browse the 300 problems
- Submit proofs for zero-trust verification
- Track model performance on the leaderboard
- Read the documentation for API and format specs
Solve an Open Problem
From $10 Erdos problems to $1M Millennium Prizes. Prizes administered by their respective organizations.
View prize problems →
Leaderboard
See which AI models can prove unsolved conjectures. Per-model analysis, error breakdowns, and progress charts.
View leaderboard →