TCSExam

How far can LLMs advance
TCS research?

Evaluating large language models across theoretical computer science. From complete proofs and reusable solvers to verified constructions and open conjectures.

Results Tasks Paper GitHub Docs
Task protocols
Submit
Complete Lean proof
Verify
Lean kernel + axiom checks

5 Lite / 20 Full tasks

Submit
Reusable solver program
Verify
Executable task checker

5 Lite / 30 Full tasks

Submit
Object or bound + Lean proof
Verify
Lean kernel + certificate checks

5 Lite / 20 Full tasks

Submit
Proof or refutation in Lean
Verify
Independent main proof slots

5 Lite / 30 Full tasks

TCSExam-Lite

20 tasks
Download CSV

Loading results…

Index & evaluation details

TCSExam-Full

100 tasks
Download CSV

Loading results…

Index & evaluation details

Research outcomes

These constructions improve on the best previously known results, to the best of our knowledge.

629 → 630 edges

Kimi K3 · Verified construction

More edges, no short cycles

Kimi K3 constructed a 630-edge graph, improving on the 629-edge construction of Goedgebeur et al.

Connect 124 vertices with as many edges as possible, while forbidding triangles and four-edge cycles.

124 vertices. No triangles or four-cycles.

A shortest cycle has five edges.

Each extra edge makes the cycle restrictions harder to satisfy. This construction raises the lower bound on the maximum possible edge count for 124 vertices, a concrete advance in extremal graph theory.

Distance 5 → 6

GPT-6 Astra · Quantum error correction

A stronger quantum code

Astra’s code detects every damaging error affecting up to five qubits, improving the reference code’s limit of four.

Protect 7 logical qubits using 25 physical qubits.

Select a cell to change its error.

Reference · distance 5Error missed
Astra · distance 6Error detected
How it works

Each cell is a physical qubit. Select it to cycle through no error (·), a bit flip (X), both flips (Y), and a phase flip (Z).

Reference · distance 5

0 of 18 checks triggered

Astra · distance 6

10 of 18 checks triggered

The same five-qubit error is missed by the reference code and detected by Astra’s code.

Stronger error detection with the same number of qubits.

References

Graph: Goedgebeur et al. (2025), Table 1, version 1 gives the 629-edge construction on 124 vertices.

Quantum code: Grassl’s code tables list the [[25,7,5]] reference. Astra’s [[25,7,6]] code increases the distance from 5 to 6.

Explore the task library

Get started

Task Suite

Solver protocol

Agent harness

Lite · 20 tasks / Offline / Kimi Code

# After Install and Configure, in the same shell:
tcsexam source-inputs
tcsexam build --suite lite --solver-protocol offline \
  --output build/lite-offline-images.json
tcsexam doctor --suite lite --solver-protocol offline \
  --agent kimi-code --artifacts build/lite-offline-images.json \
  --output build/lite-offline-readiness.json
# Resolve doctor blockers before starting model API usage.
tcsexam run --suite lite --solver-protocol offline \
  --agent kimi-code --artifacts build/lite-offline-images.json \
  --attempts 1 --concurrency 1 \
  --output build/lite-offline-job.json

Complete Install and Configure before Run. Run starts model API usage.

Read the complete getting-started guide Source code

Citation & contributions

Citation

Download paper

Contributions

Help improve task statements, evaluation rules, and verification code with feedback and corrections.

Report an issue or suggest a correction

We welcome new tasks in theorem proving, solver engineering, constructions, and open conjectures.

Contribute a task

Sources & acknowledgements

We thank the researchers, competition organizers and benchmark maintainers whose problems, instances and reference results make TCSExam possible.

TCSExam brings this existing work into a shared evaluation of AI research capabilities through task interfaces, formal specifications and verification. Each task page credits its original paper or benchmark source.