SAIR launches the Open Math Model initiative for community-governed open-weight math AI, plus Lean Kernel and Andrews–Curtis challenges
Confirmed
The takeaway
On 18 Sep 2026 Terence Tao announced that SAIR (Foundation for Science and AI Research), a nonprofit he co-founded, is speeding up an “Open Math Model” initiative.
Status
- Claim
Confirmed
- Our reporting
- High confidence
- Importance
- 3 of 5
- Last verified
- 20 October 2026
Your AI and this story
- GPT-6 Astra141 days after its cutoff
- Claude Opus 5.580 days after its cutoff
- Gemini 4 Hydrogen171 days after its cutoff
- Grok 4.7110 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 80 days before it.
Key facts
- Principles: open-licensed weights and code, published training methods; explicit consent for training data; Apache 2.0 / MIT / CC BY 4.0 style licences; public community governance; independence from industry partners even when accepting compute
- Support for competitions from XTX Markets and Susquehanna; SAIR seeks funding, compute and expertise partners
- Andrews–Curtis Conjecture Challenge: organised by Sergei Gukov, Terence Tao and Lucas Fagan (Caltech Math-AI group); AI tools welcome; closes 30 Nov 2026
- Lean Kernel Challenge: co-organised with Lean FRO (Joachim Breitner, Leonardo de Moura, Kim Morrison, Terence Tao); improve verified computation in the Lean 4 kernel; Stage 1 has eight problems, deadline 20 Nov 2026
- Framed as an open, non-corporate alternative to frontier labs’ closed math models
- Oct 16, 2026: SAIR soft-launched ‘Open Math OS’ (openmathmodel.org), a web chat service running open models (DeepSeek V4.1 Flash, Kimi K3, GLM 5.3 Flash) on donated compute; team accounts let members see each other’s prompts; free accounts for academics. Tao: the models are about a year behind the frontier, not up to the recent one-shot problem solving, but ‘capable enough for many other useful mathematical tasks’ such as medium-sized Lean formalization. SAIR is seeking partners to post-train an open model for mathematics
What happened
In response to closed frontier-lab math systems and the controversies of September 2026, SAIR moved up its plan for open mathematical AI. Tao’s post describes it as models “for everyday mathematical work” under community control. SAIR’s competitions put AI tools to work on an open problem in combinatorial group theory and on Lean’s own infrastructure.
Why it matters
It is the most concrete attempt by leading mathematicians to build an open, independent alternative to frontier labs’ math AI, with governance and data-consent rules written in from the start.
Sources
10 sources from 7 sites. Numbers match the chips in the text.
10 sources: 9 primary, 1 press
Primary
- Terence Tao: SAIR Open Math OS released (Oct 16, 2026)terrytao.wordpress.com, official
- SAIR Open Math OSopenmathmodel.org, official
- Terence Tao: SAIR’s Open Math Model initiativeterrytao.wordpress.com, official
- SAIR: Open Math Modelsair.foundation, official
- Terence Tao: SAIR competition, Andrews–Curtis challengeterrytao.wordpress.com, official
- Terence Tao: SAIR competition, Lean Kernel Challengeterrytao.wordpress.com, official
- SAIR: Lean Kernel Challenge Stage 1 overviewcompetition.sair.foundation, official
- GitHub: SAIRcompetition/lean-kernel-challengegithub.com, code
- SAIR on X: Lean Kernel Challenge announcementx.com, official
Press
- XTX Markets: 2026 update on AI for Maths philanthropyxtxmarkets.com, press
Changes
- Video added: SAIR interview with Terence Tao and Yu Deng on the Open Math Model (Oct 19)
- Open Math OS soft launch (Tao blog)
- Filed. Competition details come from search snippets of SAIR/Tao pages, and prize amounts were not found
