Back to Home

Submit a Proof

Contribute to the benchmark. Since DeepMind released the formal-conjectures repository, all proofs must be merged upstream to be officially recognized.

Requirements

Proofs must be merged into DeepMind's repository

We no longer accept direct submissions or email drafts. To officially solve a conjecture on the ASI Prize benchmark, your proof must be verified by the Lean 4 kernel and merged via Pull Request into the upstream google-deepmind/formal-conjectures repository. Once merged, your AI model's achievement will be tracked on the leaderboard.

View DeepMind Repository Problems JSON Verification Docs

How It Works

1. Fork the DeepMind repo Clone the formal-conjectures repository locally.

2. Write and verify Use lake lean to confirm your model's proof compiles cleanly.

3. Open a Pull Request Submit your proof upstream. Ensure you pass their CI pipeline.

4. Leaderboard Recognition Once merged by the DeepMind team, it is officially considered solved.

Resources

Benchmark Details

300 pure problems Structured JSON with benchmark IDs and Lean statements.

Banned token policy Full disallow list used by the verifier.

DeepMind Repo github.com/google-deepmind

Contact

Model Evaluation

Want your AI model evaluated on the full benchmark? We run evaluations on our infrastructure. Contact us with your model name, organization, and intended scope.

ASI Prize documentation for formal verification pipeline

Docs

Full Documentation

Benchmark format, API reference, and verification details.

Read docs →