New Benchmark Finds GPT-6 Astra Proves 70% of Lean Theorems but No Open Conjectures

The benchmark, called TCSExam, was built by researchers from Tsinghua University and Moonshot AI, the Beijing company behind the Kimi models. The authors include Moonshot founder Zhilin Yang and the Turing Award winner Andrew Chi-Chih Yao. It sets 100 tasks across four tracks: proving theorems in the Lean 4 proof assistant, writing solver programs, finding mathematical constructions, and attacking open conjectures. "Every submission is checked by the Lean kernel or an executable task checker," the authors wrote, so a persuasive but flawed argument earns nothing.

The results give a more measured picture of AI's research mathematics ability than the headline claims of recent months. In August OpenAI released ten machine-checkable proofs of open problems from an internal model called Astra, later made public as GPT-6 Astra. On TCSExam, models proved most known results well but almost never closed a genuinely open question.

GPT-6 Astra led the full 100-task suite with a TCSExam Index score of 71.9. It proved 70% of the theorems, scored 64.7% on solver engineering and 104.9% on constructions, a figure above 100 because constructions that beat the reference are not capped. Its open-conjecture score was zero. Moonshot's own Kimi K3.1 Pro came second with 57.4, proving 38.3% of theorems. Kimi K3, DeepSeek V4.1 Flash, Zhipu's GLM-5.3, Alibaba's Qwen3.8 Max and xAI's Grok 4.6 followed, each scoring between 40.4 and 46.8, with theorem-proving rates of 11.7% or lower.

Anthropic's Claude Opus 5.5 appears only in the results for TCSExam-Lite, a 20-task subset with five tasks per track. There it ranked first with 72.3, ahead of GPT-6 Astra's 67.0, and proved 80% of its theorems against Astra's 60%. The authors said rankings on the full and lite versions were closely aligned across the eight agents tested on both.

Only two agents were credited with resolving any conjecture in the full set, and the paper says both did so by adapting counterexamples and Lean proofs that OpenAI had already published for two problems, known as Ryser and MIRUP. Kimi K3.1 Pro scored 1.1% on the conjecture track and the October version of DeepSeek V4.1 Flash scored 5.6%. The other 28 conjectures have no accepted complete solution, the researchers wrote.

The conjecture work still produced some verified partial results. GPT-6 Astra proved the Alon-Jaeger-Tarsi conjecture over the finite field F5 for all n up to 9, and the authors report four further verified special cases or bounds. Some solver programs and constructions improved on the reference answers, including a 630-edge graph of girth five and a new quantum error-correcting code.

The scoring weights theorems, solvers and constructions at 30% each and open conjectures at 10%. Each attempt had a 12-hour wall-clock budget, which puts a single pass over the full suite at about 1,200 hours. The Kimi and DeepSeek models were given three attempts per task, while the other agents, including GPT-6 Astra, had one.

The authors flag several limits. Single attempts make the results noisy, the construction and conjecture tracks allowed agents to search the literature, and the full and lite versions judged solver programs under different protocols. They suggest future rounds test agents without internet access. The paper is a preprint and has not been peer reviewed. Task sources, Docker build recipes and evaluation tools have been released on GitHub so other groups can rerun the tests.