lanyonai
Featured
GeneralRelativisticMaxwell
A formally verified solver for the general relativistic Maxwell equations in curved spacetime, automatically generated by the Lanyon system with both Lean 4 proofs and C code.
Why it is worth attention
It is the first AI theorem prover to attain a perfect score at the world's most prestigious pre-college mathematics competition, with all formal statements and proofs autonomously generated and verified.
Who it is for
- Researchers in automated theorem proving and AI
- Lean 4 users and formal verification practitioners
- Mathematicians interested in formalized competition problems
- Participants and organizers of mathematical olympiads
Use cases
- Formalizing and verifying solutions to competition-level mathematics
- Benchmarking automated theorem provers on real-world problems
- Studying multi-agent ensemble methods for formal proof generation
- Building verified libraries of olympiad solutions in Lean 4
Strengths
- Perfect 42/42 score across all six IMO 2026 problems
- Autonomous generation of both problem statements and complete proofs
- All proofs verified using Axle's verify_proof and validated locally
- Multi-agent ensemble architecture that scales to complex problems (up to 4229 lines)
Considerations
- Some problems require substantial compute time (e.g., Q3 at 869 minutes)
- Dependence on Axle external verification service and Mathlib v4.31.0
- Requires familiarity with Lean 4 and mathlib for comprehension and reuse
README quick start
AxiomProver at IMO 2026
IMO 2026, the world's most prestigious pre-college mathematics competition, was held in Shanghai on July 15–16, 2026. AxiomProver solved all six problems, achieving a perfect score of 42/42. AxiomProver is an autonomous multi-agent ensemble theorem prover for Lean 4, developed by Axiom Math.
This repository contains the formal Lean 4 statements and solutions for all six problems of the competition.
The official source of the problems is https://www.imo-official.org/problems/2026/.
Each problem lives under IMO2026//:
problem.lean— the formal statement, with the bodies left assorry, autonomously generated by AxiomProver.solution.lean— the verified formal proof, autonomously generated by AxiomProver.
Problems
- 2026 Q1: [statement] [solution] (521 lines, 24 minutes).
- 2026 Q2: [statement] [solution] (1224 lines, 360 minutes).
- 2026 Q3: [statement] [solution] (4229 lines, 869 minutes).
- 2026 Q4: [statement] [solution] (520 lines, 39 minutes).
- 2026 Q5: [statement] [solution] (457 lines, 65 minutes).
- 2026 Q6: [statement] [solution] (771 lines, 139 minutes).
Building
Built against Mathlib v4.31.0 (see lean-toolchain).
lake exe cache get # fetch the prebuilt Mathlib cache
lake build # build all problem/solution libraries
Verification
One can verify that each problem.lean and solution.lean are compatible
using verify.py, which calls Axle's verify_proof:
python3 verify.py
Q1: okay=True (passed)
Q2: okay=True (passed)
Q3: okay=True (passed)
Q4: okay=True (passed)
Q5: okay=True (passed)
Q6: okay=True (passed)
This is expected to complete very quickly, as the results are cached by Axle.
To bypass this, pass --no-cache to the call, which will force Axle to recompute everything,
at the cost of a slower time:
python3 verify.py --no-cache
Q1: okay=True (passed)
Q2: okay=True (passed)
Q3: okay=True (passed)
Q4: ok
Related repositories
Similar projects matched by category, topics, and programming language.