SAIR launches the Open Math Model initiative for community-governed open-weight math AI, plus Lean Kernel and Andrews–Curtis challenges
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. The goal is open-weight, community-governed AI models for everyday mathematical work (understanding proofs, checking references, exploring examples, coding, formalising), trained only on consented data. SAIR also ran two XTX-funded competitions: an Andrews–Curtis conjecture challenge (from 11 Sep, with Caltech) and a Lean Kernel Challenge (from 15 Sep, with Lean FRO).
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
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.
Changelog
- 2026-09-29: created (lead from data/leads.md). Competition details come from search snippets of SAIR/Tao pages, and prize amounts were not found
Related events
- Palomar launches: a registry of Lean-verified mathematics to curb misrepresented AI proof claims ★★★
- Fields Medallists' open letter 'A Severe Misalignment of AI in Mathematics' criticises labs' race for famous problems ★★★
Sources (8)
- officialTerence Tao: SAIR's Open Math Model initiative
- officialSAIR: Open Math Model
- officialTerence Tao: SAIR competition, Andrews–Curtis challenge
- officialTerence Tao: SAIR competition, Lean Kernel Challenge
- officialSAIR: Lean Kernel Challenge Stage 1 overview
- codeGitHub: SAIRcompetition/lean-kernel-challenge
- officialSAIR on X: Lean Kernel Challenge announcement
- pressXTX Markets: 2026 update on AI for Maths philanthropy
id: 2026-09-18-sair-open-math-model-initiative · updated 2026-09-29 · open in the interactive timeline