GitHub - AxiomMath/IMO2026 · GitHub
/" data-turbo-transient="true" />
Skip to content
Search or jump to...
Search code, repositories, users, issues, pull requests...
-->
Search
Clear
Search syntax tips
Provide feedback
--><br>We read every piece of feedback, and take your input very seriously.
Include my email address so I can be contacted
Cancel
Submit feedback
Saved searches
Use saved searches to filter your results more quickly
-->
Name
Query
To see all available qualifiers, see our documentation.
Cancel
Create saved search
Sign in
/;ref_cta:Sign up;ref_loc:header logged out"}"<br>Sign up
Appearance settings
Resetting focus
You signed in with another tab or window. Reload to refresh your session.<br>You signed out in another tab or window. Reload to refresh your session.<br>You switched accounts on another tab or window. Reload to refresh your session.
Dismiss alert
{{ message }}
Uh oh!
There was an error while loading. Please reload this page.
AxiomMath
IMO2026
Public
Notifications<br>You must be signed in to change notification settings
Fork
Star<br>13
main
BranchesTags
Go to file
CodeOpen more actions menu
Folders and files<br>NameNameLast commit message<br>Last commit date<br>Latest commit
History<br>1 Commit<br>1 Commit
IMO2026
IMO2026
.gitignore
.gitignore
LICENSE
LICENSE
README.md
README.md
formalization.yaml
formalization.yaml
lake-manifest.json
lake-manifest.json
lakefile.lean
lakefile.lean
lean-toolchain
lean-toolchain
logo.svg
logo.svg
verify.py
verify.py
View all files
Repository files navigation
AxiomProver at IMO 2026
IMO 2026, the world's most prestigious pre-college mathematics competition, was<br>held in Shanghai on July 15–16, 2026. AxiomProver solved all six problems, achieving a<br>perfect score of 42/42. AxiomProver is an autonomous multi-agent ensemble theorem<br>prover for Lean 4, developed by Axiom Math.
This repository contains the formal Lean 4 statements and solutions for all six<br>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 as sorry, 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<br>lake build # build all problem/solution libraries
Verification
One can verify that each problem.lean and solution.lean are compatible<br>using verify.py, which calls Axle's verify_proof:
python3 verify.py<br>Q1: okay=True (passed)<br>Q2: okay=True (passed)<br>Q3: okay=True (passed)<br>Q4: okay=True (passed)<br>Q5: okay=True (passed)<br>Q6: okay=True (passed)
This is expected to complete very quickly, as the results are cached by Axle.<br>To bypass this, pass --no-cache to the call, which will force Axle to recompute everything,<br>at the cost of a slower time:
python3 verify.py --no-cache<br>Q1: okay=True (passed)<br>Q2: okay=True (passed)<br>Q3: okay=True (passed)<br>Q4: okay=True (passed)<br>Q5: okay=True (passed)<br>Q6: okay=True (passed)
About
No description, website, or topics provided.
Resources
Readme
License
MIT license
Uh oh!
There was an error while loading. Please reload this page.
Activity
Custom properties
Stars
13<br>stars
Watchers
watching
Forks
forks
Report repository
Releases
No releases published
Packages
Uh oh!
There was an error while loading. Please reload this page.
Contributors
Uh oh!
There was an error while loading. Please reload this page.
Languages
Lean<br>99.7%
Python<br>0.3%
You can’t perform that action at this time.