# Tsinghua and Moonshot AI release TCSExam, a theoretical computer science research benchmark

> Original title: New Tsinghua and Moonshot AI paper finds that GPT-6 Astra proves 70.0% of research-level computer science theorems in Lean, yet the same ...

- Source: Rohan Paul
- Published: 2026-11-08T18:45:52.000Z
- Bad Influence: https://badinfluence.news/items/ww78cv1f26ypiao0zy2a1neye
- Original: https://x.com/rohanpaul_ai/status/2119501674465439786

## Summary

Tsinghua University and Moonshot AI introduce TCSExam, a benchmark of 100 expert-reviewed tasks across Lean theorem proving, solver engineering, record-setting constructions, and 30 open conjectures. Without supplied lemmas, GPT-6 Astra fully proved theorems in 70.0% of attempts, and Kimi K3.1 Pro in 38.3%. The same model resolved 0 of 30 open conjectures, and the few accepted conjecture submissions adapted counterexamples and proofs OpenAI had already published.

## Post

New Tsinghua and Moonshot AI paper finds that GPT-6 Astra proves 70.0% of research-level computer science theorems in Lean, yet the same model resolves 0 of 30 open conjectures in theoretical computer science (TCS).

Theoretical computer science is a natural test for AI research, because proofs can be machine-checked and records can be beaten. Existing benchmarks cover only slices, like proofs or code.

TCSExam has 100 expert-reviewed tasks in 4 tracks: Lean theorem proving, solver engineering, record-setting constructions, and 30 open conjectures. The Lean kernel or a task checker verifies every submission.

Without supplied lemmas, GPT-6 Astra fully proved theorems in 70.0% of attempts, Kimi K3.1 Pro in 38.3%, and the other 6 agents in at most 11.7%. The few accepted conjecture submissions adapted counterexamples and proofs OpenAI had already published.

![](https://badinfluence.news/api/img-proxy?u=https%3A%2F%2Fpbs.twimg.com%2Fmedia%2FHWn6ttkaAAAPHim.jpg&mode=thumb&exp=1794528000&sig=4580087b025a6038)