Documentation

What is ASI Prize

A benchmark for measuring AI on formal mathematics. 300 unsolved conjectures from Google DeepMind's formal-conjectures project, formalized in Lean 4 with Mathlib v4.27.0.

Evaluation is binary pass/fail. Either the proof type-checks against the Lean 4 kernel, or it does not. No partial credit. No human judge. The compiler decides.

1 proof verified so far. 4 AI models evaluated. $2.78M in prize money unclaimed across 12 problems.

V2 Comparator Verification Pipeline

We migrated from a naive V1 pipeline to a robust V2 architecture using Lean's official Comparator for zero-trust verification. Every submitted proof is verified automatically, preventing adversarial redefinition attacks.

1. Banned token scan -- 19 tokens with NFKC Unicode normalization
2. Sandboxed execution -- systemd-run isolates the build process
3. Comparator build -- Lean's official Comparator builds the ground-truth challenge
4. Agent build -- Comparator builds the agent's proposed solution
5. Kernel replay -- Evaluates low-level Lean kernel exports
6. Exact signature match -- Cryptographically ensures the theorem wasn't redefined
7. Axiom audit -- Rejects sorryAx and unauthorized axioms

Banned Tokens

19 tokens are prohibited. Any proof containing them is automatically rejected. The scanner applies NFKC Unicode normalization to defeat homoglyph evasion.

sorry    sorryAx    admit    admit?
native_decide    ofReduceBool    unsafe
IO    IO.FS    System
Lean.Elab    Lean.Meta    Lean.Compiler
Lake    csimp    #eval
axiom    implemented_by    extern

Only standard Lean 4 axioms are permitted: propext, Quot.sound, Classical.choice, plus everything in Mathlib.

Submitting Proofs

Each problem is a Lean 4 theorem with sorry as a placeholder. Replace sorry with a valid proof.

Requirements:

• Compiles without errors against Lean 4.27.0 + Mathlib v4.27.0
• Contains no banned tokens
• Preserves the original theorem statement exactly
• Only replaces the proof body (the := by sorry part)

Submit via the submission page or email leaderboard@asiprize.com with your results and verification logs.

Proof Format

import FormalConjectures.Util.ProblemImports

set_option linter.style.copyright false
set_option linter.style.ams_attribute false
set_option linter.style.category_attribute false

theorem simple_addition :
    2 + 2 = 4 := by
  norm_num

Problem Structure

Problems are stored as JSON with a Lean 4 theorem statement. The benchmark uses FormalConjectures.Util.ProblemImports which provides access to all of Mathlib.

{
  "id": "ErdosProblems__1__erdos_1",
  "title": "erdos_1",
  "source": "formal-conjectures",
  "category": "research_open",
  "lean_statement": "theorem erdos_1 ... := by\n  sorry",
  "lean_imports": [
    "FormalConjectures.Util.ProblemImports"
  ]
}

Common Tactics

Useful Lean 4 tactics for approaching these problems:

• intro -- Introduce hypotheses
• apply / exact -- Apply lemmas or provide exact proof terms
• rw -- Rewrite using equalities
• simp / simp only -- Simplification (prefer simp only for speed)
• norm_num -- Normalize numerical expressions
• omega -- Linear arithmetic over integers
• ring -- Ring equalities
• linarith -- Linear arithmetic over ordered fields

Frequently Asked Questions