SAIR Competitions

Open mathematical and AI discovery challenges.

SAIR runs open competitions at the frontier of mathematics and machine reasoning. Anyone can take part — results and leaderboards live on each challenge page.

Challenges

Inverse Galois Problem (IGP24) — A mathematical discovery challenge: help expand the known map of degree-24 equations (the Inverse Galois Problem in Degree 24) and their hidden symmetries. Full rules (Markdown).
Modular Arithmetic Challenge — Can a neural network learn to compute (a × b) mod p for integers hundreds of digits long? An open probe of where exact machine reasoning breaks down. Full rules & code (GitHub).
Mathematics Distillation Challenge — Equational Theories (Stage 1) — Submit a single knowledge prompt that guides an LLM to decide whether one equation implies another. The prompt must include placeholders for Equation 1 and Equation 2 so each evaluation problem can be inserted automatically. SAIR's first competition, announced by Terence Tao. Code & judge (GitHub).
Mathematics Distillation Challenge — Equational Theories (Stage 2) — Submit a solver that, for each pair of equations, produces a machine-verified Lean 4 certificate (a proof when one implies the other, or a finite magma counterexample), adjudicated by a deterministic Lean judge. Lean solver & judge (GitHub).

Community & tools

Contributor Network — Community-contributed items that connect to the Playground.
Playground — Interactive workspace for SAIR challenges.
Zulip — Community chat.
Hugging Face — Datasets and models.
GitHub — Open-source competition code.

About SAIR

SAIR Foundation — Mission, programs, and events.
Blog
Contact — press@sair.foundation