The collaboration between Yao Qizhi and Yang Zhilin has given mathematicians a huge sigh of relief.

On November 5, a new paper was uploaded to arXiv.

The five authors are from Moonshot AI, Tsinghua University and Shanghai Qizhi Institute. Two names stand out prominently: one is Andrew Chi-Chih Yao, Turing Award laureate and Dean of the Institute for Interdisciplinary Information Sciences of Tsinghua University, and the other is Yang Zhilin, founder of Moonshot AI (Kimi).

The title of the paper is TCSExam: Evaluating Frontier LLMs on the Full Range of TCS Research.

In a nutshell, they designed a full test paper and used it to assess a group of the most powerful AI large models available today.

TCS is the abbreviation of Theoretical Computer Science. It does not focus on how to repair computers or write code, but explores the very essence of "computation" itself.

Programmers are like drivers who care about engines and interior trim, while TCS is equivalent to traffic research: it explores the absolute minimum time required to travel from point A to point B, and identifies routes that are inherently impassable.

This is the intersection of mathematics and computer science, where all problems revolve around the core concept of "computation", and research work mainly relies on formal proofs.

The timing of this paper's release is rather subtle. In early October, OpenAI publicly released 722 AI-generated mathematical manuscripts at once, which were categorized into 372 "result families" by relevance, covering 17 fields including number theory, theoretical computer science, geometry, and mathematical physics. The topic of "AI has made mathematics obsolete" once became a trending search on Weibo.

Terence Tao once told Nature that AI has a fatal flaw in almost all fields: it makes errors that cannot be verified. Mathematics is the only exception, especially proofs, whose validity can be automatically checked by machines. It is similar to Sudoku: it is difficult to fill in the grid, but you can immediately tell if the result is correct after checking it once. Therefore, the most uncontroversial achievements of AI companies will be achieved in the field of mathematics.

However, the conclusions drawn from the assessments in this paper by Andrew Chi-Chih Yao and Yang Zhilin are somewhat sobering: None of the referenced models can solve any of the long-standing unsolved open conjectures on their own.

There are already so many benchmarks for large models, why design another test paper?

The benchmark scores of large models rise almost every two months, and various ranking lists are dazzling. In fact, these lists only prove that the models can solve existing problems, but cannot reflect their actual research capabilities.

Essentially, solving standard problems is like cooking according to a recipe: the steps are ready-made, and the taste has a clear standard. You have never seen chocolate added to guobaorou (sweet and sour fried pork), right? In contrast, research does not have pre-defined steps, no one can guarantee the success of the work in advance, and even the person who raised many problems does not know the correct answer.

What is more troublesome is grading. When a model writes hundreds of pages of "proof" at one go, no one has the time to read page by page. When it claims to have solved a conjecture that no one has cracked for decades, no one can confirm that its writing is correct.

The 722 manuscripts released by OpenAI are a ready example.

What this paper aims to clarify is exactly this: when AI is actually assigned to do real research work, how well can it perform?

The solution is to only design questions that can be graded by machines. The more similar a question is to real research, the harder it is to score; TCS is a rare exception, as most of its conclusions can be verified by machines.

The test paper contains a total of 100 questions, divided into four categories, corresponding to four types of work that theoretical computer scientists usually do.

The first category: Theorem proving, 20 questions. The questions are theorems extracted from TCS papers published between 2023 and 2026, all of which are formally published research results covering 13 sub-fields.

The model needs to write a complete full proof from start to finish, and cannot use plain language. Instead, it must use a special language called Lean 4 to write the proof for easy machine verification. This is like filling out forms at a government service window: each column must be filled in according to the specified format, and a free-form essay will not be accepted. The assessment method is divided into three levels, which can be understood by analogy to mountain climbing.

The second category: Solver engineering, 30 questions. A "solver" is a program specially designed to solve a certain type of problem. This type of question does not ask the model to solve a single problem, but to write a program that can solve all problems of the same category.

The model will be given a problem description, the most naive solution, and a set of public example questions. For example, given a batch of circuits, the requirement is to keep the function unchanged, and reduce the number of a basic component (AND gate) as much as possible, the fewer components the better.

The third category: Explicit construction, 20 questions. The previous tasks are all "armchair strategy" for the model. In the construction step, the model is required to actually create the target object.

The fourth category: Open conjectures, 30 questions. These questions are conjectures that have not been proven or disproven so far.

The most well-known open conjecture to the general public is probably the Goldbach Conjecture, which has been proposed for more than 280 years, and no one has come up with a reliable proof method yet.

The 30 questions on the test paper are not that famous, but their nature is the same. Each question leaves two blanks: one for the complete proof that "the conjecture is true", and the other for the complete proof that "the conjecture is not true". Only filling in one of the two blanks counts as a valid answer.

Moreover, there is no partial credit for steps in this section. If the problem cannot be solved, the score is 0.

The questions are first selected by experts according to three criteria: whether they have research value, whether the field coverage is comprehensive, and whether the results can be verified.

All 100 questions are reviewed by experts. Then an AI assistant translates the questions into Lean language and writes the scoring program, and another independent AI assistant checks the conditions and scope of each question against the original paper to make sure there are no copying errors. It also tests some special small examples, and translates the Lean-written questions back to natural language for comparison to prevent the questions from being distorted during translation.

In the trial test phase, more than 40 theorem questions were eliminated directly because the models managed to solve them. In the official test, if any question is unexpectedly proven to be correct, or the score is abnormally high, a re-examination of the question and its source will be triggered.

Not only that, if a model sets a new record during the test, AI will re-examine its entire operation process.

Just like all the exams you have taken, TCSExam also has a time limit.

Each answer to each question is allowed a maximum of 12 hours, calculated according to the actual elapsed time. Kimi K3, Kimi K3.1 Pro and two versions of DeepSeek take each test 3 times, and the rest of the models take each test once. To test all 100 questions once, it takes up to 1200 hours.

In addition, TCSExam has both open-book and closed-book sections. Calculus and probability theory are closed-book, while Marxist philosophy and ideological and moral cultivation are open-book, which everyone who has attended university understands. In TCSExam, theorem proving and solver engineering do not allow internet access, and only construction and conjecture sections allow literature review. Keep this point in mind, it will be useful later.

Taking the full version of the test is too time-consuming, so there is also a lightweight Lite version: 5 questions are selected from each of the four categories, for a total of 20 questions. The time limit for each answer remains unchanged, the question volume is reduced by 80%, and the maximum required time is 240 hours. All questions, codes and evaluation tools are made public, and anyone can review them.

Finally, the four types of scores are combined into a total score, called the TCSExam Index. The algorithm is very simple: theorem proving, solver engineering, and construction each account for 30 points, and open conjectures account for 10 points. The formula is I=30P+30S+30C+10O, where P, S, C, and O are the average scores of the four types of questions respectively.

What are the scores like?

Before looking at the results, let's clarify how to interpret each metric.

There are 8 candidates participating in the full version of the exam: GPT-6 Astra from OpenAI, Kimi K3 and Kimi K3.1 Pro from Moonshot AI, GLM-5.3 from Zhipu AI, Qwen3.8 Max from Alibaba, Grok 4.6 from xAI, and two versions of DeepSeek V4.1 Flash (0910 and 1017). The results are sorted from highest to lowest by total score:

First place: GPT-6 Astra, 71.9 points: 70.0% for theorem proving, 64.7% for solver engineering, 104.9% for construction, 0.0% for open conjectures.

Second place: Kimi K3.1 Pro, 57.4 points: 38.3% for theorem proving, 54.1% for solver engineering, 98.6% for construction, 1.1% for open conjectures.

Third place: Kimi K3, 46.8 points: 11.7% for theorem proving, 48.7% for solver engineering, 95.5% for construction, 0.0% for open conjectures.

Fourth place: DeepSeek V4.1 Flash 1017, 46.0 points: 6.7% for theorem proving, 53.1% for solver engineering, 91.8% for construction, 5.6% for open conjectures.

Fifth place: GLM-5.3, 45.5 points: 5.0% for theorem proving, 49.1% for solver engineering, 97.7% for construction, 0.0% for open conjectures.

Sixth place: Qwen3.8 Max (0902), 44.8 points: 5.0% for theorem proving, 49.2% for solver engineering, 95.1% for construction, 0.0% for open conjectures.

Seventh place: Grok 4.6, 40.5 points: 5.0% for theorem proving, 43.8% for solver engineering, 86.2% for construction, 0.0% for open conjectures.

Eighth place: DeepSeek V4.1 Flash 0910, 40.4 points: 0.0% for theorem proving, 48.3% for solver engineering, 86.6% for construction, 0.0% for open conjectures.

Taking the 71.9 points of the first-place GPT-6 Astra as an example: 70.0% of 30 points for theorem proving equals 21 points, 64.7% of 30 points for solver engineering equals 19.4 points, 104.9% of 30 points for construction equals 31.5 points, and 0 points for conjectures, adding up to exactly 71.9.

The first-place GPT-6 Astra leads the second-place Kimi K3.1 Pro by 14.5 points; from the third-place Kimi K3 to the eighth-place DeepSeek V4.1 Flash 0910, six models are clustered between 40 and 47 points, with a difference of less than 7 points from each other.

One additional candidate, Opus 5.5 from Anthropic, joined the lightweight version. It only participated in the lightweight version and took the first place immediately.

For the 5 theorem questions, Opus 5.5 proved 4 (80.0%), and Astra proved 3 (60.0%). The two models have the same construction score of 100.4%; Astra is slightly higher in the solver section, with 63.0% vs 60.5%.

The rankings of the two lists are highly consistent.

For the 8 models that participated in both tests, you can pick any two to compare their order, and there are 28 pairs in total. The order of 26 pairs is exactly the same on both lists. Statistically, there is a special indicator to measure the similarity of two rankings, called the Spearman correlation coefficient. A perfect consistency is 1, and the value here is 0.93. This means that although the lightweight version only has 20 questions, the ranking it produces is reliable.

However, for this kind of test, we should not only look at the scores, but also the distribution of results.

In the solver engineering section, the scores of all models are not very different, ranging from a minimum of 43.8% to a maximum of 64.7%. The same applies to the construction section, ranging from 86.2% to 104.9%. But in the theorem proving section alone, the scores are 70.0%, 38.3%, 11.7%, 6.7%, 5.0%, 5.0%, 5.0%, 0.0%, showing a cliff-like decline.

This is just like the college entrance examination: everyone gets similar scores for the basic questions at the front, but the gap widens sharply when it comes to the final challenging final question.

Being good at proving is not the same as being good at construction.

DeepSeek 0910 did not hand in a single complete proof in 60 theorem proving attempts, but achieved results exceeding the reference record in construction questions. GLM-5.3 has a very stable average construction score of 97.7%, but never exceeded the reference record. Astra is the most comprehensive, and got the highest average score in 27 out of 30 solver questions.

Kimi K3.1 Pro is not inferior to GPT in all aspects. For a theorem about Probabilistically Checkable Proofs (PCP), it successfully proved it all three times, while the first-place GPT-6 Astra failed to prove it in its attempt.

For analogy, these models are all food delivery riders.

If you ask them to write down every step of a new route they have never taken, and explain why each step is chosen, they cannot write a single sentence. But if you give them a pile of orders, they can arrange a delivery route that no one has ever thought of, and after verification, the route is indeed faster. DeepSeek 0910 is exactly such a rider.

So when a theorem cannot be proved, is it because the model is truly incapable, or just a little short of success? The paper specially made a comparison: for the same 20 theorems, each with 3 attempts, the test is carried out with three levels of prompts. Kimi K3 solved 3 questions in the bare test, solved 4 questions after being given intermediate conclusions, and solved 7 questions after being given the ideas. DeepSeek 0910 got 0, 2, and 6 respectively. With a little guidance, the model can make progress.

There are several solid new results in the construction questions.

Kimi K3 created a graph with 124 vertices and 630 edges, which contains neither triangles nor quadrilaterals. You can understand this type of problem this way: build roads between 124 villages, build as many roads as possible