---
id: "2026-09-18-sair-open-math-model-initiative"
url: "https://postcutoff.com/e/2026-09-18-sair-open-math-model-initiative/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2026-09-18"
date_precision: day
category: open-source
importance: 3
confidence: high
status: [Confirmed]
sources: 10
editor: human editor
human_review: null
version: "2026-10-20"
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-09-18-sair-open-math-model-initiative/

# 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
- 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.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 141 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 80 days after its cutoff
- Gemini 4 Hydrogen (training cutoff March 2026): 171 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 110 days after its cutoff

## Sources

1. [Terence Tao: SAIR Open Math OS released (Oct 16, 2026)](https://terrytao.wordpress.com/2026/10/16/sair-open-math-os-released/) (terrytao.wordpress.com, official)
2. [SAIR Open Math OS](https://www.openmathmodel.org/) (openmathmodel.org, official)
3. [Terence Tao: SAIR's Open Math Model initiative](https://terrytao.wordpress.com/2026/09/18/sairs-open-math-model-initiative/) (terrytao.wordpress.com, official)
4. [SAIR: Open Math Model](https://sair.foundation/open-math-model/) (sair.foundation, official)
5. [Terence Tao: SAIR competition, Andrews–Curtis challenge](https://terrytao.wordpress.com/2026/09/11/sair-competition-andrew-curtis-challenge/) (terrytao.wordpress.com, official)
6. [Terence Tao: SAIR competition, Lean Kernel Challenge](https://terrytao.wordpress.com/2026/09/16/sair-competition-lean-kernel-challenge/) (terrytao.wordpress.com, official)
7. [SAIR: Lean Kernel Challenge Stage 1 overview](https://competition.sair.foundation/competitions/lean-kernel-challenge/overview) (competition.sair.foundation, official)
8. [GitHub: SAIRcompetition/lean-kernel-challenge](https://github.com/SAIRcompetition/lean-kernel-challenge) (github.com, code)
9. [SAIR on X: Lean Kernel Challenge announcement](https://x.com/SAIRfoundation/status/2092293379547869590) (x.com, official)
10. [XTX Markets: 2026 update on AI for Maths philanthropy](https://www.xtxmarkets.com/news/2026-update-on-xtx-markets-ai-philanthropy/) (xtxmarkets.com, press)

## Changes

- 2026-10-20: Video added: SAIR interview with Terence Tao and Yu Deng on the Open Math Model (Oct 19)
- 2026-10-16: Open Math OS soft launch (Tao blog)
- 2026-09-29 (filed): Created. Competition details come from search snippets of SAIR/Tao pages, and prize amounts were not found

## Related

- 2026-09-11: [Fields Medallists' open letter 'A Severe Misalignment of AI in Mathematics' criticises labs' race for famous problems](https://postcutoff.com/e/2026-09-11-fields-medalists-letter-ai-mathematics/index.md)
- 2026-08-18: [Palomar launches: a registry of Lean-verified mathematics to curb misrepresented AI proof claims](https://postcutoff.com/e/2026-08-18-palomar-lean-registry/index.md)
- People: [Terence Tao](https://postcutoff.com/person/terence-tao/)
- Archived: 1 post and 2 videos, listed in https://postcutoff.com/e/2026-09-18-sair-open-math-model-initiative/index.json