# SAIR Competitions

> Open, community-driven mathematics and AI competitions hosted by SAIR (the Foundation for Science and AI Research), co-founded by Terence Tao. Tagline: "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)](https://competition.sair.foundation/competitions/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: https://competition.sair.foundation/competitions/igp24.md
- [Modular Arithmetic Challenge](https://competition.sair.foundation/competitions/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: https://github.com/SAIRcompetition/modular-arithmetic-challenge
- [Mathematics Distillation Challenge — Equational Theories (Stage 1)](https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage1): 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: https://github.com/SAIRcompetition/equational-theories-stage1-judge
- [Mathematics Distillation Challenge — Equational Theories (Stage 2)](https://competition.sair.foundation/competitions/mathematics-distillation-challenge-equational-theories-stage2): 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: https://github.com/SAIRcompetition/equational-theories-lean-stage2

## Community & tools

- [Contributor Network](https://competition.sair.foundation/contributor-network): Community-contributed items that connect to the Playground.
- [Playground](https://playground.sair.foundation): Interactive workspace for SAIR challenges.
- [Zulip](https://zulip.sair.foundation/): Community chat.
- [Hugging Face](https://huggingface.co/SAIRfoundation): Datasets and models.
- [GitHub](https://github.com/SAIRcompetition): Open-source competition code.

## About SAIR

- [SAIR Foundation](https://sair.foundation): Mission, programs, and events.
- [Blog](https://blog.sair.foundation/)
- Contact: press@sair.foundation