Atlas

Benchmarks

TCSExam theorem proving

GitHub

TCSExam's theorem track: 20 Lean 4 theorems from theoretical computer science, each a success only with a complete proof the Lean kernel accepts. The rate counts every scheduled attempt.

Models
8
Top score
70.0
Leader
GPT-6 Astra
Updated
Nov 5, 2026
Resolution
—
Saturation
—
Signal
92ndpercentile
205 benchmarks from 0.8 to 3.6219 benchmarks from 3.6 to 6.4134 benchmarks from 6.4 to 9.393 benchmarks from 9.3 to 12.155 benchmarks from 12.1 to 14.925 benchmarks from 14.9 to 17.713 benchmarks from 17.7 to 20.55 benchmarks from 20.5 to 23.37 benchmarks from 23.3 to 26.27 benchmarks from 26.2 to 29.01 benchmark from 29.0 to 31.83 benchmarks from 31.8 to 34.66 benchmarks from 34.6 to 37.43 benchmarks from 37.4 to 40.21 benchmark from 40.2 to 43.11 benchmark from 45.9 to 48.71 benchmark from 65.6 to 68.4

61st strongest of 779

Signal-to-noise +16.16 for the TCSExam family

Difficulty
Not estimated

Another benchmark represents this family in the fit.

8 dated models · 2 frontier modelsClosed weightsOpen weights
Data: Moonshot AIatlas.village.dev
#ModelSettingScoreSource
1GPT-6 Astramax · Codex
70.0
TCSExam paper Table 2 (Full, GPT-6 Astra)
2Kimi K3.1 Promax · Kimi Code
38.3
TCSExam paper Table 2 (Full, Kimi K3.1 Pro)
3Kimi K3max · Kimi Code
11.7
TCSExam paper Table 2 (Full, Kimi K3)
4DeepSeek V4.1 Flash 1017max · Claude Code
6.7
TCSExam paper Table 2 (Full, DeepSeek V4.1 Flash 1017)
5GLM-5.3max · Claude Code
5.0
TCSExam paper Table 2 (Full, GLM-5.3)
6Grok 4.6x-high · Grok Build
5.0
TCSExam paper Table 2 (Full, Grok 4.6)
7Qwen3.8 Max (0902)max · Claude Code
5.0
TCSExam paper Table 2 (Full, Qwen3.8 Max (0902))
8DeepSeek V4.1 Flashmax · Claude Code
0.0
TCSExam paper Table 2 (Full, DeepSeek V4.1 Flash 0910)
Loading Atlas data…