Sep 27 - Oct 2, 2026 · Hybrid kickoff at MIT · Worldwide online
Join a global competition to formalize mathematics, attack open problems, and create verifiable public results with any combination of human reasoning and AI.
Read the Competition and Judging Handbook (PDF)Scoring, judging, eligibility, and the submission cutoff are set out in the handbook. The submission workspace and checker instructions will be linked here before submissions open.
The strongest AI systems can now explore mathematical ideas at extraordinary speed. A serious challenge for those systems can no longer stop at familiar exercises with known answers. It has to reach the frontier: open problems, reusable formalizations, decisive counterexamples, meaningful reductions, and new mathematical variations.
OpenMath concentrates many human and machine research loops into one public effort. Teams propose, compute, test, criticize, revise, formalize, and verify. They may attempt as many independently meaningful claims as they can finish. The objective is not a spectacle of confident answers. It is a large, inspectable body of mathematics that other researchers can check, reuse, and build upon.
The workflow is open. The standard of acceptance is not.
A model-generated proof sketch, numerical pattern, informal argument, or persuasive manuscript may be valuable research evidence. It is not, by itself, an accepted competition result. A score-bearing claim must be encoded as an exact formal artifact or approved formal certificate, reproduce in a pinned environment, disclose its dependencies and material tools, and pass both machine checking and human semantic-fidelity review.
Machine checking answers whether the encoded object passes the specified formal system. Human review answers whether that object faithfully captures the mathematical claim being presented, whether the result is genuinely new or correctly classified, and whether attribution and provenance are complete. Both are required.
Fast generation + exact verification + public provenance.
Work on a versioned focus set selected for special emphasis. The organizers expect a substantial set, but will not publish a final count until import, deduplication, statement review, and status checking are complete. Accepted focus-set results earn a 1.1x focus bonus, as set out in the handbook.
Create useful formalizations of established theorems, arguments, structures, or bodies of knowledge. Credit belongs to the new formal artifact and its authors, while historical mathematical attribution remains intact. This path can expand the libraries and infrastructure needed for future open-problem work.
Pursue admitted open problems outside the focus set. A target must have a precise canonical statement, provenance, open-status review, family identity, and difficulty assessment before it becomes score-eligible.
Formulate and solve a substantive new variation connected to a canonical Open Mathematics parent. A meaningful change in hypotheses, objects, or conclusion can qualify. Cosmetic restatements, equivalent formulations, and artificial fragmentation do not create separate results.