FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models

# FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
Source: [https://arxiv.org/html/2608.20153](https://arxiv.org/html/2608.20153)
Dingzirui Wang Xuanliang Zhang Keyan Xu Qingfu Zhu Wanxiang CheHarbin Institute of Technology\{dzrwang,xuanliangzhang,kyxu,qfzhu,car\}@ir\.hit\.edu\.cn

###### Abstract

Large language models \(LLMs\) have shown growing potential for automated theoretical computer science \(TCS\) research, yet existing benchmarks remain far from realistic research settings\. We introduceFormalTCS, an expert\-validated benchmark for evaluating LLMs on frontier, end\-to\-end TCS research\.FormalTCScontains175175instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025\-2026, preserving paper\-specific definitions, assumptions, and proof dependencies, with expert\-verified Lean formalizations and proofs\. Evaluations of leading LLMs reveal that current models remain far from reliably completing the full research pipeline\. In particular, autoformalization is the sharpest bottleneck: the best model achieves only11\.511\.5on translating natural\-language claims into formal theorem statements, compared with28\.628\.6Pass@8 when proving human\-provided formal statements\. Building onFormalTCS, we further develop an automated TCS research framework that generates, formalizes, filters, and proves new claims\. Of6464generated claims, only66ultimately pass expert evaluation and proof verification, indicating that beyond formalization, limited research taste remains another major barrier to autonomous TCS research111Our code is released in[https://github\.com/zirui\-HIT/FormalTCS](https://github.com/zirui-HIT/FormalTCS)\.\.

## 1Introduction

Theoretical computer science \(TCS\) studies the fundamental principles of computation through mathematical methods, including models of computation, algorithms, computational complexity, and the limits of computability\([26](https://arxiv.org/html/2608.20153#bib.bib31);[27](https://arxiv.org/html/2608.20153#bib.bib32)\)\. TCS is an important research topic as it provides the theoretical foundation for understanding which problems can be computed and how efficiently they can be solved\. Given the fundamental importance of TCS and the increasingly strong autonomous research capabilities demonstrated by large language models \(LLMs\)\([3](https://arxiv.org/html/2608.20153#bib.bib29)\), a growing body of work has begun to investigate how well LLMs can perform TCS\-related research tasks\. For example, LCS\-Bench\([8](https://arxiv.org/html/2608.20153#bib.bib19)\)constructs a benchmark from TCS knowledge extracted from textbooks, while TCS\-Bench\([4](https://arxiv.org/html/2608.20153#bib.bib14)\)evaluates the ability of LLMs to generate proofs of TCS theorems from natural\-language statements\.

However, existing TCS benchmarks still exhibit a substantial gap from real\-world TCS research:\(i\) Incomplete research pipeline\.Existing benchmarks primarily evaluate isolated capabilities such as autoformalization or proof generation\. They do not provide an end\-to\-end evaluation of whether LLMs can conduct TCS research from scratch, making it difficult to identify where current models fail throughout the research process\.\(ii\) Outdated content\.Existing benchmarks are largely constructed from textbook material or theorems already available in libraries such as Mathlib\([15](https://arxiv.org/html/2608.20153#bib.bib20)\)\. As a result, they provide limited insight into an LLM’s ability to reason about frontier TCS research and may also suffer from contamination when benchmark theorems or closely related material have appeared in the model’s training data\.\(iii\) Simplified problem settings\.Existing benchmarks typically focus on relatively self\-contained theorems with complete and explicit definitions\. In contrast, real TCS papers involve paper\-specific definitions and assumptions, as well as multi\-layered dependencies among lemmas and theorems\. Existing benchmarks, therefore, fall short of measuring whether LLMs can solve complex, research\-level TCS problems in realistic settings\.

To bridge these gaps, we introduceFormalTCS, a benchmark designed to provide a more realistic evaluation of LLMs’ ability to engage with frontier TCS research\. With assistance fromGPT\-5\.6\-sol\([18](https://arxiv.org/html/2608.20153#bib.bib27)\), we employ five human experts to collect and annotate examples from papers accepted by top conferences in TCS\. Compared with existing benchmarks,FormalTCSprovides a more faithful evaluation of TCS research capabilities in three respects:\(i\) End\-to\-end evaluation\.FormalTCSdecomposes the TCS research pipeline into five stages and evaluates, step by step, an LLM’s ability to transform a natural\-language TCS core claim into a corresponding rigorous Lean proof\. This design enables a fine\-grained diagnosis of the capabilities and bottlenecks of LLMs throughout the TCS research process\.\(ii\) Frontier research content\.FormalTCSis constructed from papers accepted to FOCS, STOC, SODA, and COLT in 2025 and 2026\. We additionally filter the source papers based on whether they are likely to have been previously exposed to the evaluated LLMs, thereby maintaining the timeliness of the benchmark while reducing the risk of data contamination\.\(iii\) Realistic research problems\.FormalTCSevaluates core theoretical problems drawn directly from real TCS papers while preserving their paper\-specific definitions, assumptions, and proof dependencies\. It therefore more accurately measures the ability of LLMs to reason about and prove research\-level TCS results\.

Table 1:The main findings revealed byFormalTCS\.We evaluate a range of leading LLMs onFormalTCS, with the findings summarized in Table[1](https://arxiv.org/html/2608.20153#S1.T1)\. Overall, current state\-of\-the\-art models still struggle to perform end\-to\-end TCS research effectively, highlighting the need for further advances in LLM\-based TCS reasoning and demonstrating the necessity ofFormalTCS\. In particular, we find thatthe primary bottleneck lies in translating a natural\-language core claim into appropriate formal definitions and theorem statements, where the current most advanced LLMs can only achieve the performance of10%10\\%\. This suggests that the mathematical modeling capabilities of current LLMs remain a major limitation for TCS research\. In addition, building onFormalTCS, we develop an end\-to\-end TCS research framework that supports the complete pipeline from proposing a TCS core claim to producing a rigorous Lean proof\. Our experiments show that existing LLMs are able to produce rigorous proofs for the core claims they propose themselves\. However, human inspection reveals that most of these proposed claims exhibit limited novelty, suggesting thatthe research taste of current models in TCS remains underdeveloped\.

Our contributions can be summarized as follows:

1. 1\.We introduceFormalTCS, a benchmark based on real research problems for evaluating the end\-to\-end capabilities of LLMs in frontier TCS research\.
2. 2\.Our experiments reveal that a key bottleneck for current LLMs is translating natural\-language core claims into appropriate formal definitions and theorem statements, indicating that mathematical modeling remains a major weakness of current LLMs\.
3. 3\.Building onFormalTCS, we develop an end\-to\-end LLM research framework for TCS and find that, although current models can often prove claims of their own construction, their ability to formulate novel and meaningful research claims, i\.e\., their research taste, remains limited\.

## 2Introduction ofFormalTCS

### 2\.1Overall Statistics

29222018141312998876Learning TheoryNeural & Generative ModelsStatistics & TestingComplexity & Lower BoundsFairness & PrivacyAlgorithms & Data Struct\.Online Learning & BanditsEcon\. & Game TheoryOptimizationAlgebra & CSPCoding & CommunicationGeometry & ClusteringGraphs & CombinatoricsFigure 1:The distribution of research areas covered byFormalTCS\.FormalTCSis an expert\-validated benchmark designed to evaluate the end\-to\-end capabilities of LLMs in frontier TCS research\. It consists of175175instances, each derived from a distinct research paper, covering175175papers in total\. We use Lean 4\.32\.2\([15](https://arxiv.org/html/2608.20153#bib.bib20)\)together with the corresponding version of Mathlib, which is the latest version available at the time of annotation\. We ensure the quality ofFormalTCSalong the following dimensions:\(i\) High difficulty\.Across all instances, the expert\-validated Lean proofs contain an average of22\.022\.0statements and29\.629\.6nodes, indicating that the benchmark involves substantial formalization and proof complexity\.\(ii\) High diversity\.As shown in Figure[1](https://arxiv.org/html/2608.20153#S2.F1),FormalTCSspans1313major research areas in TCS\. This broad coverage enables the benchmark to evaluate LLM research capabilities across a diverse range of TCS problems\.

### 2\.2Data Format

Table 2:Data fields ofFormalTCS\.CategoryNameTypeMeaningMetainfoidstringData id\.conferencestringConference of the accepted paper\.yearintAccepted year of the paper\.paperstringName of the paper\.core\_labelstringLabel in the paper of claim used\.Natural Languagecore\_claimstringCore finding ofcore\_labelclaim\.nl\_claimstringFull statement ofcore\_labelclaim\.nl\_proofstringProof sketch ofcore\_labelclaim\.Formal Languagefl\_theoremLean fileTheorem to be proved ofcore\_labelclaim\.fl\_proofLean projectFull Lean\-format proof ofcore\_labelclaim\.The data format ofFormalTCSis summarized in Table[2](https://arxiv.org/html/2608.20153#S2.T2)\. Each instance contains information corresponding to the different stages of the end\-to\-end TCS research pipeline, enabling us to diagnose the capabilities and bottlenecks of current LLMs at each stage of the research process\. Importantly, every instance is accompanied by a rigorous Lean proof that has been manually verified by experts\. This expert validation ensures the correctness and reliability of the formalization and, consequently, the overall quality ofFormalTCS\. We provide representative cases fromFormalTCSin Appendix[C](https://arxiv.org/html/2608.20153#A3)\.

## 3Annotation ofFormalTCS

![Refer to caption](https://arxiv.org/html/2608.20153v1/annotate_pipeline.png)Figure 2:The annotation pipeline ofFormalTCS\.This section describes the annotation pipeline used to constructFormalTCS, as illustrated in Figure[2](https://arxiv.org/html/2608.20153#S3.F2)\. Five human experts participate in the annotation process\. Each annotator has published multiple papers at top\-tier TCS conferences and has substantial research experience in the field\. Given the considerable difficulty of formalizing proofs from the selected papers, we employ LLM assistance to reduce annotation costs while maintaining data quality usingGPT\-5\.6\-solalongsideCodex\. The prompts used during annotation are provided in Appendix[B\.1](https://arxiv.org/html/2608.20153#A2.SS1), while Appendix[A](https://arxiv.org/html/2608.20153#A1)reports information about the annotators and additional annotation details\. Although LLMs are used as assistive tools, all final annotations are manually inspected and revised when necessary to ensure semantic faithfulness, type correctness, and concise formulations rather than preserving stylistic artifacts introduced by the models\. Additional results on inter\-annotator agreement and human verification pass rates are provided in Appendix[E](https://arxiv.org/html/2608.20153#A5)\.

### 3\.1Source Paper

Our source\-paper pool consists of papers accepted to STOC, FOCS, SODA, and COLT in 2025 and 2026\. This selection is intended to ensure a high level of research quality while reducing the likelihood of benchmark contamination\. We first use automated scripts to scan all accepted papers and perform an initial filtering step to identify works that appear to study TCS problems\. Human experts then manually inspect every candidate paper to verify its relevance and determine whether it contains a suitable core result together with a rigorous proof of that result\. In addition, we conduct a black\-box audit to assess whether the retained papers may have been exposed during model training\. Specifically, we queryGPT\-5\.6\-solandClaude\-Opus\-5without providing retrieval access or paper metadata\. The inputs consist of partial theorem statements, initial fragments of proofs, and anonymized descriptions of paper results, and the models are asked to reconstruct the missing content\. We find that the completion similarity of both models is below9\.6%9\.6\\%, suggesting a relatively low risk of contamination for the selected data\. The detailed black\-box audit is discussed in Appendix[G](https://arxiv.org/html/2608.20153#A7)\.

### 3\.2Core Claim

For each retained paper, human experts produce a concise summary of one of its central theoretical results\. The summary must contain fewer than3636words and should avoid mathematical notation whenever it is not necessary, so that the resulting claim is both compact and understandable without additional context\. When multiple claims from the same paper could reasonably serve as the core claim, annotators select the one that best represents the paper’s central contribution\. This criterion reflects the primary objective ofFormalTCS, which is to evaluate whether an LLM can recover the relevant theorem and its proof from a given core claim, rather than whether the model can identify which result in a paper is the most important\. For each paper, two experts independently write candidate core claims\. A third expert then compares the two candidates and selects the stronger formulation as the final annotation\.

### 3\.3Natural Language Claim

We next construct a natural\-language claim corresponding to the theorem in the source paper associated with the selected core claim\. If the original theorem is already understandable independently of the surrounding paper, where its statement contains all necessary assumptions and definitions, we directly retain the theorem statement as its informal version\. If the theorem depends on definitions or assumptions introduced elsewhere in the paper, a human expert collects the missing information and rewrites the theorem into a self\-contained statement while avoiding unnecessary verbosity\. Each rewritten theorem is subsequently reviewed by another expert to verify that it is self\-contained and that its assumptions and definitions remain faithful to those in the source paper\.

### 3\.4Formal Language Theorem and Proof

In this step, we construct the formal theorem to be proved and its corresponding Lean proof for each instance, providing a reliable basis for evaluating the TCS proof capabilities of LLMs\. Following previous works\([12](https://arxiv.org/html/2608.20153#bib.bib22);[35](https://arxiv.org/html/2608.20153#bib.bib21)\), we first use the LLM, together with the source\-paper content, to generate a proof\-blueprint DAG for the selected core claim\. Human experts then verify that the resulting blueprint faithfully follows the proof structure of the original paper and that the statement associated with each node is consistent with its corresponding result in the source paper\. We subsequently invoke the LLM to prove the nodes in the DAG one by one according to their dependency order based on the original paper\. After each node is proved, a human expert checks that the Lean proof is rigorous and faithful to the corresponding argument in the original paper and verifies that no proof\-bypassing constructs, such assorryor additional axioms, are used\. Once the complete Lean proof has been constructed, another human expert performs an independent end\-to\-end review and fixes any remaining issues\. The resulting verified artifact is used as the final formal\-language proof\. Finally, we extract from this proof the target theorem together with the definition closure required to state it and replace the proof body of the target theorem withsorry\. The resulting artifact constitutes the formal\-language theorem provided to the model as the proof\-generation task\.

### 3\.5Natural Language Proof

Our preliminary experiments during benchmark construction indicate that current LLMs often struggle to generate rigorous proofs directly from formal\-language theorem statements\. We therefore additionally annotate a natural\-language proof sketch, allowing us to diagnose model limitations at a finer level of granularity\. Each sketch summarizes the main proof ideas used in the source paper, enabling us to evaluate whether an LLM can identify an appropriate high\-level proof strategy before carrying out the formal derivation\. To obtain an initial draft, we provide the LLM with both the verified formal proof described above and the original paper, and ask it to generate a natural\-language proof sketch\. A human expert then checks whether the generated sketch is faithful to the proof strategy in the source paper and whether its reasoning is sufficiently complete\. Finally, unnecessary low\-level derivations and details are removed so that the resulting sketch remains concise while faithfully capturing the overall argument\.

## 4Experiment

In this section, we evaluate a diverse set of mainstream LLMs onFormalTCSto investigate the extent to which current models are capable of conducting TCS research\. Rather than treating aggregate benchmark performance as the sole measure of success, we focus on the capabilities required at each stage of the research pipeline and the corresponding failure modes revealed byFormalTCS\. This stage\-wise evaluation provides a more fine\-grained view of where current LLMs perform well in the TCS research workflow and where substantial challenges remain\. All prompts used in our experiments are provided in Appendix[B\.2](https://arxiv.org/html/2608.20153#A2.SS2)\.

### 4\.1Experiment Setup

##### Models

Given the substantial difficulty of theoretical reasoning tasks, we evaluate three representative families of mainstream LLMs, includingGPT\([18](https://arxiv.org/html/2608.20153#bib.bib27)\),Claude\([1](https://arxiv.org/html/2608.20153#bib.bib28)\), andDeepSeek\([5](https://arxiv.org/html/2608.20153#bib.bib26)\), using their corresponding harnesses\. The selected models span different model scales, allowing us to investigate the relationship between model scale and TCS research performance\. This diverse model selection is intended to provide a more comprehensive characterization of the strengths and limitations of current LLMs\. Detailed model snapshots and harness versions are provided in Appendix[D](https://arxiv.org/html/2608.20153#A4)\.

##### Task

Table 3:Tasks inFormalTCS\.FormalTCSconsists of four tasks that jointly cover the process from understanding a core claim to constructing a machine\-verifiable formal proof\. Table[3](https://arxiv.org/html/2608.20153#S4.T3)provides detailed definitions of the four tasks\. To evaluate each stage independently, we provide human\-annotated inputs for every task rather than using predictions from the preceding stage as inputs\. This design prevents errors introduced early in the pipeline from propagating to subsequent tasks, thereby allowing us to identify the sources of performance degradation more precisely\. The results reported in Table[4](https://arxiv.org/html/2608.20153#S4.T4)further motivate this stage\-wise evaluation, as current LLMs remain unable to reliably complete the entire TCS research pipeline in an end\-to\-end manner\.

##### Metrics

We adopt task\-specific evaluation metrics to measure different aspects of capabilities:

- •LLM\-Rubric\([14](https://arxiv.org/html/2608.20153#bib.bib25)\)\(CC2NC, C2NP\): We adopt an LLM\-based rubric to evaluate the semantic consistency between model predictions and reference answers\. Each response receives four scores normalized to the\[0,1\]\[0,1\]range, corresponding to logical validity \(slogics\_\{\\mathrm\{logic\}\}\), completeness \(scompletes\_\{\\mathrm\{complete\}\}\), correctness \(scorrects\_\{\\mathrm\{correct\}\}\), and clarity \(sclears\_\{\\mathrm\{clear\}\}\)\. These dimensions are aggregated using the following weighted score:Score=0\.4​slogic\+0\.3​scomplete\+0\.2​scorrect\+0\.1​sclear\\mathrm\{Score\}=0\.4s\_\{\\mathrm\{logic\}\}\+0\.3s\_\{\\mathrm\{complete\}\}\+0\.2s\_\{\\mathrm\{correct\}\}\+0\.1s\_\{\\mathrm\{clear\}\}\. To reduce potential evaluation bias, we useQwen3\.8\-MaxwithQoderCLI\([20](https://arxiv.org/html/2608.20153#bib.bib30)\)as the rubric evaluator, which is distinct from all models evaluated in our main experiments\. We additionally examine the rubric agreement between LLM\-based and human evaluations in Appendix[F](https://arxiv.org/html/2608.20153#A6)\.
- •BEq\+\([19](https://arxiv.org/html/2608.20153#bib.bib24)\)\(NC2FT\): For the autoformalization task, we adopt BEq\+, which determines whether a generated Lean theorem statement is equivalent to the reference statement through bidirectional theorem proving\. Given a reference theoremtrt\_\{r\}and a generated candidate theoremtct\_\{c\}, the metric attempts to prove bothtr⇒tct\_\{r\}\\Rightarrow t\_\{c\}andtc⇒trt\_\{c\}\\Rightarrow t\_\{r\}in Lean\. Unlike evaluation methods based on LLM judges, this procedure relies on deterministic symbolic proof search\. A candidate theorem is considered equivalent to the reference theorem only if proofs in both directions are successfully constructed\.
- •Pass@kk\([6](https://arxiv.org/html/2608.20153#bib.bib23)\)\(FT2FP\): For the theorem\-proving task, we use Pass@kk, which measures the proportion of instances for which at least one of thekksampled proofs is accepted by the Lean compiler\. The metric therefore reflects the probability that the model produces at least one syntactically valid and formally verified proof across multiple generation attempts\. To prevent models from bypassing the proof obligation, our automated verification environment enablesset\_option warningAsError trueso that the use ofsorryresults in an error\. We additionally use a custom linter or invoke\#print axiomson the target theorem with an explicit whitelist of permitted axioms, thereby preventing models from circumventing proof construction throughsorry, customaxiomdeclarations, or similar mechanisms\.

##### Generation Parameters

Following the experimental settings of prior work on formal reasoning\([21](https://arxiv.org/html/2608.20153#bib.bib15);[13](https://arxiv.org/html/2608.20153#bib.bib16)\), we generate88candidate outputs for each instance in the NC2FT and FT2FP tasks to balance evaluation cost and reliability while using a single generation for CC2NC and C2NP\. We adopt different generation settings because Lean outputs admit reliable automatic verification, allowing us to sample multiple formal candidates and evaluate them objectively using symbolic verification\. In contrast, natural\-language responses lack an equally reliable automatic verifier, making single\-sample evaluation more appropriate for these tasks\. For tasks requiring multiple generations, we use a temperature of0\.60\.6and set top\_p to0\.90\.9\. For single\-generation experiments, we use deterministic decoding with a temperature of0\.00\.0and top\_p of1\.01\.0\.

### 4\.2Experimental Results

Table 4:Performance of mainstream LLMs and their corresponding harnesses onFormalTCS\. The best performance on each task is marked inbold\.Table[4](https://arxiv.org/html/2608.20153#S4.T4)reports the performance of all evaluated models onFormalTCS\. Overall,Claude\-Opus\-5achieves the best performance on most tasks, indicating the strongest TCS research capability among the evaluated models\. Beyond the overall comparison, the results reveal several important findings about the capabilities and limitations of current LLMs\.

#### 4\.2\.1Finding 1: Current LLMs Struggle with End\-to\-End TCS Research

Our results show that even the strongest current models remain limited when completing the full TCS research pipeline\. For example, the best\-performing model,Claude\-Opus\-5, achieves scores of66\.966\.9and68\.768\.7on natural\-language claim understanding \(CC2NC\) and proof\-strategy generation \(C2NP\), respectively\. However, substantial bottlenecks remain in the formal stages of the pipeline, with its final formal proof generation performance \(FT2FP\) reaching only28\.628\.6Pass@8\. These results suggest that, although current LLMs exhibit meaningful theoretical reasoning capabilities, they still struggle to reliably complete the end\-to\-end TCS research process from a high\-level research claim to a machine\-verifiable formal proof\.

#### 4\.2\.2Finding 2: Formalization Tasks Are Substantially More Difficult Than Natural\-Language Tasks

The results show that LLMs perform substantially better on natural\-language tasks than on formalization tasks\. For example,Claude\-Opus\-5achieves68\.768\.7on C2NP, whereas its performance on the corresponding theorem formalization task \(NC2FT\) is only11\.511\.5\. Similarly,GPT\-5\.6\-solachieves67\.967\.9on C2NP but only10\.610\.6on NC2FT\. This substantial performance gap suggests that current LLMs can understand and articulate high\-level theoretical ideas considerably better than they can translate those ideas into rigorous formal representations\.

#### 4\.2\.3Finding 3: Autoformalization Is the Primary Bottleneck for LLM\-Based TCS Research

Across the entire pipeline, NC2FT is the lowest\-performing stage, with no evaluated model exceeding11\.511\.5\. In contrast, when provided with a human\-annotated formal theorem statement, models achieve up to28\.628\.6Pass@8 on the subsequent formal proof generation task \(FT2FP\)\. This result suggests that the primary difficulty for current models is not merely generating Lean proofs\. Rather, the more fundamental challenge lies in correctly identifying the mathematical objects, assumptions, and logical structure underlying a natural\-language claim and translating them into appropriate formal definitions and theorem statements\. Improving autoformalization capabilities is therefore a key direction toward enabling LLMs to conduct automated end\-to\-end TCS research\.

## 5End\-to\-End Automated TCS Research withFormalTCS

![Refer to caption](https://arxiv.org/html/2608.20153v1/inspire_pipeline.png)Figure 3:Our end\-to\-end TCS research pipeline using LLMs based onFormalTCS\.AlthoughFormalTCSprimarily focuses on evaluating theoretical reasoning capabilities rather than the quality of newly proposed research ideas, generating meaningful TCS core claims remains an essential component of a fully automated research pipeline\. Directly evaluating such claims is challenging since determining whether a research idea is genuinely useful remains an open problem and lacks reliable evaluation metrics\([24](https://arxiv.org/html/2608.20153#bib.bib17);[23](https://arxiv.org/html/2608.20153#bib.bib18)\)\. To investigate this capability, we develop a multi\-agent framework in this section that enables LLMs to propose candidate claims, translate them into formal statements, and automatically filter them before human evaluation\.In contrast to §[4](https://arxiv.org/html/2608.20153#S4), which primarily evaluates the bottlenecks of current LLMs in TCS research, this section investigates whether current LLMs, when guided byFormalTCS, can autonomously discover valuable TCS claims and produce correct end\-to\-end proofs for them\.The overall system is illustrated in Figure[3](https://arxiv.org/html/2608.20153#S5.F3)and the prompts used in this section are provided in Appendix[B\.3](https://arxiv.org/html/2608.20153#A2.SS3)\.

### 5\.1Framework Design

#### 5\.1\.1Agent\-Loop Generation

Our framework is inspired by the iterative nature of real\-world TCS research\. Researchers typically do not commit to a fixed problem formulation from the outset\. Instead, they repeatedly revise assumptions, definitions, modeling choices, and proof directions until they identify a result worth pursuing\. We simulate this iterative process using three agents: a planner, a formalizer, and a judger\.

##### Planner\.

Based on the content ofFormalTCSand the derivations accumulated so far, the planner proposes a new research objective\. The objective is not restricted to extending the current line of reasoning\. The planner may reformulate the problem, introduce auxiliary concepts, strengthen or relax assumptions, or explore alternative analytical directions\. This flexibility allows the system to search over a diverse space of potential theoretical research directions\.

##### Formalizer\.

The formalizer translates the proposed research objective into a precise Lean statement and repeatedly queries the Lean compiler to identify and correct formalization errors\. For each proposal, we allow at most three rounds of compiler feedback\. Candidate claims that still fail to compile within this interaction budget are discarded from the subsequent pipeline, and the failure information is returned to the planner\.

##### Judger\.

Once a formal statement successfully compiles, the judger translates it back into a concise natural\-language claim that summarizes its potential theoretical significance and assesses the value of the proposed result\. If the claim is judged to lack sufficient novelty, it is discarded, and the corresponding feedback is returned to the planner\. Claims that pass this filtering stage are added to a candidate pool and subsequently evaluated by human experts\.

All agents operate within a shared workspace usingGPT\-5\.6\-soltogether withCodex\. At initialization, the workspace contains only data fromFormalTCS\. Each agent can freely read or write to the shared workspace while proposing and validating new claims\. For each claim, every agent maintains exactly one persistent session, allowing the corresponding context to be reused throughout the iterative process\. To encourage diversity across generated claims, at the beginning of each new generation run, we randomly sample1616instances fromFormalTCSand place them in the workspace\. We use a temperature of0\.60\.6and set top\_p to0\.90\.9\.

#### 5\.1\.2Human\-Expert Evaluation

We next conduct a human evaluation of the candidate claims retained after the agent\-based generation and filtering process\. As an initial screening step, human experts remove candidates whose conclusions have already been established in the existing literature\. The remaining claims are then evaluated according to two criteria: whether they provide a sufficiently novel observation and whether that observation has potential value for theoretical research\. Each candidate claim is independently reviewed by two experts to reduce subjectivity in the evaluation process\. Since automatically and reliably estimating novelty and research value is itself a difficult research problem, we do not incorporate an automated claim\-quality evaluator into the current framework\. We instead view this capability as an important direction for future work\. For every claim retained after expert evaluation, we subsequently follow the stage\-wise procedure introduced in §[4](https://arxiv.org/html/2608.20153#S4)to construct its corresponding formal statement and formal proof, ensuring that the resulting claims are rigorously and reliably verified\.

### 5\.2Experimental Results

All 64 generated cases8 cases passed human\-expert evaluation39Lack of novelty17Lack of value2No proof6Proof available8Remainingzoom\-in of the8 remaining

Figure 4:The distribution of generated TCS cases using our framework\.Table 5:The TCS cases discovered by our framework\.Based on the framework described above, we use the agent loop to synthesize6464core claims, of which66remain after human\-expert evaluation and proof verification\. The pass rates at each stage are shown in Figure[4](https://arxiv.org/html/2608.20153#S5.F4)\. We also present two representative cases of the accepted claims in Table[5](https://arxiv.org/html/2608.20153#S5.T5)\. These results indicate that, for current LLMs, the primary bottleneck in conducting end\-to\-end TCS research lies in generating claims that are both novel and valuable, suggesting that their research taste remains limited\. Therefore, in addition to improving autoformalization capabilities as discussed in §[4\.2\.3](https://arxiv.org/html/2608.20153#S4.SS2.SSS3), advancing the end\-to\-end TCS research capabilities of LLMs also requires substantially stronger research taste\. Interestingly, among the claims that pass human\-expert evaluation, the proof success rate is substantially higher than the FT2FP performance reported in Table[4](https://arxiv.org/html/2608.20153#S4.T4)\. The explanation is that these claims are generated by the LLMs themselves, making it easier for the LLMs to construct proofs for claims that align with their own reasoning trajectories\.

## 6Related Work

LLM for TCS refers to the use of large language models, together with tools such as formal proof assistants, program execution, and search algorithms, to assist with or automate theorem proving, algorithm discovery, and research exploration in theoretical computer science\. Its development can be roughly divided into three stages\. Early works, including Autoformalization\([29](https://arxiv.org/html/2608.20153#bib.bib1)\), Draft, Sketch, and Prove\([11](https://arxiv.org/html/2608.20153#bib.bib2)\), LeanDojo\([32](https://arxiv.org/html/2608.20153#bib.bib3)\), and DeepSeek\-Prover\([30](https://arxiv.org/html/2608.20153#bib.bib4);[31](https://arxiv.org/html/2608.20153#bib.bib5)\), primarily explored the translation of natural\-language mathematics into formal proofs, as well as the use of retrieval, proof\-assistant feedback, and search to improve machine\-verifiable reasoning capabilities\. Meanwhile, FunSearch\([22](https://arxiv.org/html/2608.20153#bib.bib6)\)began combining LLMs with program search to automatically discover new constructions and algorithms for problems in combinatorics and algorithms\. Since 2025, research has increasingly targeted TCS directly\. AlphaEvolve\([17](https://arxiv.org/html/2608.20153#bib.bib7)\)combines LLMs with evolutionary search for the discovery of algorithms and combinatorial structures\. Lean Meets TCS\([34](https://arxiv.org/html/2608.20153#bib.bib8)\)introduced a systematic evaluation of formal reasoning capabilities on TCS problems\. Related work has further used automated search to improve gadgets and hardness bounds in complexity theory\([16](https://arxiv.org/html/2608.20153#bib.bib9)\)\. More recently, LLM for TCS has begun to enter the research\-level stage\. Systems such as Gemini\([28](https://arxiv.org/html/2608.20153#bib.bib10)\), Aletheia\([7](https://arxiv.org/html/2608.20153#bib.bib11)\), and Bolzano\([2](https://arxiv.org/html/2608.20153#bib.bib12)\)attempt to solve open problems in mathematics and TCS through long\-horizon reasoning, multi\-agent collaboration, and automated verification\. Meanwhile, works such as AlphaProof Nexus\([25](https://arxiv.org/html/2608.20153#bib.bib13)\)and TCS\-Bench\([4](https://arxiv.org/html/2608.20153#bib.bib14)\)have extended evaluation toward research\-level formal proofs and theorems drawn from actual conference papers\. Overall, LLM for TCS is evolving from reasoning about and proving existing theorems toward the discovery of algorithms and combinatorial structures, and ultimately toward automated research on open problems\.

Despite this progress, existing LLM\-for\-TCS studies remain disconnected from realistic TCS research by evaluating only partial research pipelines, relying largely on textbook, synthetic, or potentially memorized problems, and simplifying research theorems into relatively self\-contained tasks that omit paper\-specific definitions, assumptions, and multi\-level proof dependencies\. To bridge these gaps,FormalTCSprovides an end\-to\-end, fine\-grained evaluation pipeline grounded in recent STOC, FOCS, SODA, and COLT papers with leakage\-aware filtering, while preserving the structure of real research problems and providing expert\-verified Lean formalizations and proofs\.

## 7Conclusion

We introduceFormalTCS, a benchmark for evaluating LLMs across the end\-to\-end pipeline of frontier TCS research using recent conference papers and expert\-verified Lean formalizations\. Our experiments show that current LLMs perform substantially better at understanding and reasoning about TCS problems in natural language than at expressing them formally, with autoformalization emerging as the primary bottleneck\. Moreover, our automated research experiments show that models can often prove claims that survive expert screening, but only a small fraction of their proposed claims are sufficiently novel and valuable\. Together, these results suggest that progress toward autonomous TCS research requires advances along two complementary dimensions: accurately translating research ideas into rigorous formal objects and developing a stronger research taste for identifying meaningful theoretical claims\. We hopeFormalTCSprovides a realistic testbed for measuring progress toward these goals\.

## References

- AnthropicClaude Opus 5 System Card\.External Links:[Link](https://www.anthropic.com/claude-opus-5-system-card)Cited by:[§4\.1](https://arxiv.org/html/2608.20153#S4.SS1.SSS0.Px1.p1.1)\.
- Balkoet al\.\(2026\)M\. Balko, J\. Grebík, P\. Hubáček, M\. Koutecký, M\. Kripner, V\. Rozhoň, R\. Šámal, and A\. ZámečníkBolzano: case studies in llm\-assisted mathematical research\.External Links:2604\.16989,[Link](https://arxiv.org/abs/2604.16989)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Chenet al\.\(2025\)Q\. Chen, M\. Yang, L\. Qin, J\. Liu, Z\. Yan, J\. Guan, D\. Peng, Y\. Ji, H\. Li, M\. Hu, Y\. Zhang, Y\. Liang, Y\. Zhou, J\. Wang, Z\. Chen, and W\. CheAI4Research: a survey of artificial intelligence for scientific research\.External Links:2507\.01903,[Link](https://arxiv.org/abs/2507.01903)Cited by:[§1](https://arxiv.org/html/2608.20153#S1.p1.1)\.
- Cohen\-Addadet al\.\(2026\)V\. Cohen\-Addad, D\. Paparas, E\. van Wijland, M\. Springer, J\. Canitrot\-Paradis, H\. Lin, D\. Woodruff, A\. Kumarappan, R\. Jayaram, R\. Das, L\. Jain, O\. Svensson, S\. Lattanzi, M\. Balunovic, T\. Weber, and V\. MirrokniTCS\-bench: benchmarking state\-of\-the\-art generative ai theoretical computer science research ability\.External Links:2608\.09538,[Link](https://arxiv.org/abs/2608.09538)Cited by:[§1](https://arxiv.org/html/2608.20153#S1.p1.1),[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- DeepSeek\-AI \(2026\)DeepSeek\-AIDeepSeek\-v4: towards highly efficient million\-token context intelligence\.Cited by:[§4\.1](https://arxiv.org/html/2608.20153#S4.SS1.SSS0.Px1.p1.1)\.
- Donget al\.\(2024\)K\. Dong, A\. V\. Mahankali, and T\. MaFormal theorem proving by rewarding LLMs to decompose proofs hierarchically\.InThe 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24,External Links:[Link](https://openreview.net/forum?id=D83tiHiNfF)Cited by:[3rd item](https://arxiv.org/html/2608.20153#S4.I1.i3.p1.1.1)\.
- Fenget al\.\(2026a\)T\. Feng, T\. H\. Trinh, G\. Bingham, D\. Hwang, Y\. Chervonyi, J\. Jung, J\. Lee, C\. Pagano, S\. Kim, F\. Pasqualotto, S\. Gukov, J\. N\. Lee, J\. Kim, K\. Hou, G\. Ghiasi, Y\. Tay, Y\. Li, C\. Kuang, Y\. Liu, H\. Lin, E\. Z\. Liu, N\. Nayakanti, X\. Yang, H\. Cheng, D\. Hassabis, K\. Kavukcuoglu, Q\. V\. Le, and T\. LuongTowards autonomous mathematics research\.External Links:2602\.10177,[Link](https://arxiv.org/abs/2602.10177)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Fenget al\.\(2026b\)Y\. Feng, F\. Pu, O\. An, O\. Bastani, L\. Zhang, J\. Huang, X\. Si, and Z\. LiTheory\-scale auto\-formalization of logics for computer science\.External Links:2606\.26525,[Link](https://arxiv.org/abs/2606.26525)Cited by:[§1](https://arxiv.org/html/2608.20153#S1.p1.1)\.
- Golchin and Surdeanu \(2023\)S\. Golchin and M\. SurdeanuTime travel in llms: tracing data contamination in large language models\.CoRRabs/2308\.08493\.External Links:[Link](https://doi.org/10.48550/arXiv.2308.08493),[Document](https://dx.doi.org/10.48550/ARXIV.2308.08493),2308\.08493Cited by:[Appendix G](https://arxiv.org/html/2608.20153#A7.p1.1)\.
- Hallinanet al\.\(2026\)S\. Hallinan, J\. Jung, M\. Sclar, X\. Lu, A\. Ravichander, S\. Ramnath, Y\. Choi, S\. P\. Karimireddy, N\. Mireshghallah, and X\. RenThe surprising effectiveness of membership inference with simple n\-gram coverage\.External Links:2508\.09603,[Link](https://arxiv.org/abs/2508.09603)Cited by:[Appendix G](https://arxiv.org/html/2608.20153#A7.p1.1)\.
- Jianget al\.\(2023\)A\. Q\. Jiang, S\. Welleck, J\. P\. Zhou, T\. Lacroix, J\. Liu, W\. Li, M\. Jamnik, G\. Lample, and Y\. WuDraft, sketch, and prove: guiding formal theorem provers with informal proofs\.InThe Eleventh International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=SMa9EAovKMC)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Khrulev \(2026\)R\. KhrulevBlueprintRepair: typed local edits for failed lean proof blueprints\.External Links:2607\.28110,[Link](https://arxiv.org/abs/2607.28110)Cited by:[§3\.4](https://arxiv.org/html/2608.20153#S3.SS4.p1.1)\.
- Linet al\.\(2025\)Y\. Lin, S\. Tang, B\. Lyu, J\. Wu, H\. Lin, K\. Yang, J\. LI, M\. Xia, D\. Chen, S\. Arora, and C\. JinGoedel\-prover: a frontier model for open\-source automated theorem proving\.InSecond Conference on Language Modeling,External Links:[Link](https://openreview.net/forum?id=x2y9i2HDjD)Cited by:[§4\.1](https://arxiv.org/html/2608.20153#S4.SS1.SSS0.Px4.p1.1)\.
- Maet al\.\(2026\)W\. Ma, A\. Cojocaru, N\. Kolhe, H\. Zhang, V\. Zhuang, M\. Zaharia, and S\. MinReliable fine\-grained evaluation of natural language math proofs\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=ky5iqwZSXI)Cited by:[1st item](https://arxiv.org/html/2608.20153#S4.I1.i1.p1.1.1)\.
- Moura and Ullrich \(2021\)L\. d\. Moura and S\. UllrichThe lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings,Berlin, Heidelberg,pp\. 625–635\.External Links:ISBN 978\-3\-030\-79875\-8,[Link](https://doi.org/10.1007/978-3-030-79876-5_37),[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[§1](https://arxiv.org/html/2608.20153#S1.p2.1),[§2\.1](https://arxiv.org/html/2608.20153#S2.SS1.p1.1)\.
- Nagdaet al\.\(2026\)A\. Nagda, P\. Raghavan, and A\. ThakurtaReinforced generation of combinatorial structures: hardness of approximation\.External Links:2509\.18057,[Link](https://arxiv.org/abs/2509.18057)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Novikovet al\.\(2025\)A\. Novikov, N\. Vũ, M\. Eisenberger, E\. Dupont, P\. Huang, A\. Z\. Wagner, S\. Shirobokov, B\. Kozlovskii, F\. J\. R\. Ruiz, A\. Mehrabian, M\. P\. Kumar, A\. See, S\. Chaudhuri, G\. Holland, A\. Davies, S\. Nowozin, P\. Kohli, and M\. BalogAlphaEvolve: a coding agent for scientific and algorithmic discovery\.External Links:2506\.13131,[Link](https://arxiv.org/abs/2506.13131)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- OpenAI \(2026\)OpenAIGPT\-5\.6 Sol Model\.External Links:[Link](https://developers.openai.com/api/docs/models/gpt-5.6-sol)Cited by:[§1](https://arxiv.org/html/2608.20153#S1.p3.1),[§4\.1](https://arxiv.org/html/2608.20153#S4.SS1.SSS0.Px1.p1.1)\.
- Poirouxet al\.\(2025\)A\. Poiroux, G\. Weiss, V\. Kunčak, and A\. BosselutReliable evaluation and benchmarks for statement autoformalization\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing,C\. Christodoulopoulos, T\. Chakraborty, C\. Rose, and V\. Peng \(Eds\.\),Suzhou, China,pp\. 17947–17969\.External Links:[Link](https://aclanthology.org/2025.emnlp-main.907/),[Document](https://dx.doi.org/10.18653/v1/2025.emnlp-main.907),ISBN 979\-8\-89176\-332\-6Cited by:[2nd item](https://arxiv.org/html/2608.20153#S4.I1.i2.p1.1.1)\.
- Qwen Team \(2026\)Qwen TeamQwen3\.8\-Max: a new bar for coding and cowork\.External Links:[Link](https://qwen.ai/blog?id=qwen3.8)Cited by:[1st item](https://arxiv.org/html/2608.20153#S4.I1.i1.p1.1)\.
- Renet al\.\(2025\)Z\. Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang, Z\. F\. Wu, Z\. Gou, S\. Ma, H\. Tang, Y\. Liu, W\. Gao, D\. Guo, and C\. RuanDeepSeek\-prover\-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.External Links:2504\.21801,[Link](https://arxiv.org/abs/2504.21801)Cited by:[§4\.1](https://arxiv.org/html/2608.20153#S4.SS1.SSS0.Px4.p1.1)\.
- Romera\-Paredeset al\.\(2024\)B\. Romera\-Paredes, M\. Barekatain, A\. Novikov, M\. Balog, M\. P\. Kumar, E\. Dupont, F\. J\. R\. Ruiz, J\. S\. Ellenberg, P\. Wang, O\. Fawzi, P\. Kohli, and A\. FawziMathematical discoveries from program search with large language models\.Nature625\(7995\),pp\. 468–475\.External Links:ISSN 1476\-4687,[Document](https://dx.doi.org/10.1038/s41586-023-06924-6),[Link](https://doi.org/10.1038/s41586-023-06924-6)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Siet al\.\(2026\)C\. Si, T\. Hashimoto, and D\. YangThe ideation\-execution gap: execution outcomes of LLM\-generated versus human research ideas\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=Fllp8l6Puy)Cited by:[§5](https://arxiv.org/html/2608.20153#S5.p1.1)\.
- Siet al\.\(2025\)C\. Si, D\. Yang, and T\. HashimotoCan LLMs generate novel research ideas? a large\-scale human study with 100\+ NLP researchers\.InThe Thirteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=M23dTGWCZy)Cited by:[§5](https://arxiv.org/html/2608.20153#S5.p1.1)\.
- Tsoukalaset al\.\(2026\)G\. Tsoukalas, A\. Kovsharov, S\. Shirobokov, A\. Surina, M\. Firsching, G\. Bérczi, F\. J\. R\. Ruiz, A\. Suggala, A\. Z\. Wagner, E\. Wieser, L\. Yu, A\. Huang, M\. Z\. Horváth, A\. Ferraiuolo, H\. Michalewski, E\. Lockhart, C\. Grosu, T\. Hubert, M\. Balog, P\. Kohli, and S\. ChaudhuriAdvancing mathematics research with ai\-driven formal proof search\.External Links:2605\.22763,[Link](https://arxiv.org/abs/2605.22763)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- J\. van Leeuwen \(Ed\.\) \(1990\)J\. van Leeuwen \(Ed\.\)Handbook of theoretical computer science, volume A: algorithms and complexity\.Elsevier and MIT Press\.External Links:ISBN 0\-444\-88071\-2Cited by:[§1](https://arxiv.org/html/2608.20153#S1.p1.1)\.
- Wigderson \(2019\)A\. WigdersonMathematics and computation: a theory revolutionizing technology and science\.Princeton University Press,United States\(English\)\.External Links:ISBN 9780691189130Cited by:[§1](https://arxiv.org/html/2608.20153#S1.p1.1)\.
- Woodruffet al\.\(2026\)D\. P\. Woodruff, V\. Cohen\-Addad, L\. Jain, J\. Mao, S\. Zuo, M\. Bateni, S\. Branzei, M\. P\. Brenner, L\. Chen, Y\. Feng, L\. Fortnow, G\. Fu, Z\. Guan, Z\. Hadizadeh, M\. T\. Hajiaghayi, M\. JafariRaviz, A\. Javanmard, K\. C\. S\., K\. Kawarabayashi, R\. Kumar, S\. Lattanzi, E\. Lee, Y\. Li, I\. Panageas, D\. Paparas, B\. Przybocki, B\. Subercaseaux, O\. Svensson, S\. Taherijam, X\. Wu, E\. Yogev, M\. Zadimoghaddam, S\. Zhou, Y\. Matias, J\. Manyika, and V\. MirrokniAccelerating scientific research with gemini: case studies and common techniques\.External Links:2602\.03837,[Link](https://arxiv.org/abs/2602.03837)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Wuet al\.\(2022\)Y\. Wu, A\. Q\. Jiang, W\. Li, M\. N\. Rabe, C\. Staats, M\. Jamnik, and C\. SzegedyAutoformalization with large language models\.NIPS ’22,Curran Associates Inc\.,Red Hook, NY, USA\.External Links:ISBN 9781713871088Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Xinet al\.\(2024\)H\. Xin, D\. Guo, Z\. Shao, Z\.Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. LiangAdvancing theorem proving in LLMs through large\-scale synthetic data\.InThe 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24,External Links:[Link](https://openreview.net/forum?id=TPtXLihkny)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Xinet al\.\(2025\)H\. Xin, Z\.Z\. Ren, J\. Song, Z\. Shao, W\. Zhao, H\. Wang, B\. Liu, L\. Zhang, X\. Lu, Q\. Du, W\. Gao, H\. Zhang, Q\. Zhu, D\. Yang, Z\. Gou, Z\.F\. Wu, F\. Luo, and C\. RuanDeepSeek\-prover\-v1\.5: harnessing proof assistant feedback for reinforcement learning and monte\-carlo tree search\.InThe Thirteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=I4YAIwrsXa)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Yanget al\.\(2023\)K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. AnandkumarLeanDojo: theorem proving with retrieval\-augmented language models\.InProceedings of the 37th International Conference on Neural Information Processing Systems,NIPS ’23,Red Hook, NY, USA\.Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Zhanget al\.\(2025a\)J\. Zhang, D\. Das, G\. Kamath, and F\. TramerPosition: Membership Inference Attacks Cannot Prove That a Model was Trained on Your Data\.In2025 IEEE Conference on Secure and Trustworthy Machine Learning \(SaTML\),Vol\.,Los Alamitos, CA, USA,pp\. 333–345\.External Links:ISSN,[Document](https://dx.doi.org/10.1109/SaTML64287.2025.00025),[Link](https://doi.ieeecomputersociety.org/10.1109/SaTML64287.2025.00025)Cited by:[Appendix G](https://arxiv.org/html/2608.20153#A7.p1.1)\.
- Zhanget al\.\(2025b\)T\. J\. Zhang, W\. Jiang, R\. Liu, Y\. Wang, N\. M\. Wang, J\. Yang, Y\. Huang, and M\. SachanLean meets theoretical computer science: scalable synthesis of theorem proving challenges in formal\-informal pairs\.In2nd AI for Math Workshop @ ICML 2025,External Links:[Link](https://openreview.net/forum?id=snoHekTbpd)Cited by:[§6](https://arxiv.org/html/2608.20153#S6.p1.1)\.
- Zhanget al\.\(2026\)Y\. Zhang, Y\. Sun, T\. Suzuki, J\. D\. Lee, and F\. LiuLeanMarathon: toward reliable ai co\-mathematicians through long\-horizon lean autoformalization\.External Links:2606\.05400,[Link](https://arxiv.org/abs/2606.05400)Cited by:[§3\.4](https://arxiv.org/html/2608.20153#S3.SS4.p1.1)\.

## Appendix AHuman Annotation Information

### A\.1Annotator Information

##### Annotator Recruitment, Expertise, and Training

Our annotation team consists of five human experts with PhD\-level backgrounds in theoretical computer science\. Each annotator has published multiple papers at top\-tier TCS conferences and has substantial experience in reading, analyzing, and verifying theorem\-based arguments\. Collectively, the team covers the major theoretical research areas represented inFormalTCSand is able to reliably trace each benchmark instance back to the definitions, assumptions, theorem statements, and proof dependencies in its source paper\. Before formal annotation begins, all annotators receive the annotation manual summarized in Table[6](https://arxiv.org/html/2608.20153#A1.T6), which specifies the requirements for each field inFormalTCSas well as consistency constraints across fields\. We additionally conduct pilot annotations on a set of papers drawn from different conferences and research subfields\. The pilot annotations are jointly reviewed to calibrate the desired level of detail, resolve ambiguous cases, and establish shared standards for theorem selection, self\-contained rewriting, and formalization\. Throughout the annotation process,GPT\-5\.6\-sol, accessed throughCodex, is used only as an assistive tool for drafting and formalization\. Any model\-generated annotation must be manually inspected and, when necessary, corrected before it is accepted\.

##### Compensation

All five PhD\-level annotators are members of the research team, and their annotation work is conducted as part of this research project rather than as paid crowd workers\. We therefore do not provide separate per\-instance crowdsourcing compensation\. Model assistance is used only to reduce repetitive annotation effort, while human annotators remain fully responsible for all labels included in the final release\.

##### Quality Control and Agreement

Throughout the annotation pipeline, we apply field\-specific human verification procedures rather than relying solely on a single final review\.

- •Forcore\_claim, two experts independently write candidate summaries, after which a third expert compares the two candidates and selects the final version\.
- •Fornl\_claim, an expert verifies that the rewritten theorem is self\-contained and that all definitions, assumptions, quantifiers, and conclusions remain faithful to the source paper\.
- •Forfl\_theoremandfl\_proof, experts compare the formalization against the source theorem and its proof dependencies, verify that auxiliary statements preserve their intended mathematical meaning, and confirm that all Lean proofs compile successfully in the specified Lean/Mathlib environment without using proof\-bypassing constructs\. The completed formal proof is subsequently reviewed by another expert, who corrects any remaining semantic, typing, dependency, or proof issues before release\.
- •Fornl\_proof, annotators verify that the proof sketch follows the main strategy of the source proof while preserving the key intermediate reasoning steps and omitting only routine derivations\.

We additionally perform independent cross\-checks on a subset of instances to measure agreement across annotators\. Disagreements and difficult cases are resolved through discussion among the expert team, and recurring ambiguities are incorporated into subsequent updates of the annotation manual\.

### A\.2Annotation Manual

##### General Principles

Table 6:Annotation manual for each field ofFormalTCS\.Each instance inFormalTCScorresponds to a retained source paper accepted to STOC, FOCS, SODA, or COLT in 2025 or 2026, and is grounded in an explicitly identified central theorem, proposition, lemma, or corollary from that paper\. Throughout the annotation process, annotators follow three principles:\(i\) source faithfulness, meaning that no assumption, definition, conclusion, or substantive proof step may be altered without support from the source paper;\(ii\) self\-containment, meaning that the annotated result should be understandable without relying on unstated paper\-specific context; and\(iii\) cross\-field consistency, meaning that the natural\-language and formal\-language fields must describe the same target result and use mutually compatible proof strategies\. Table[6](https://arxiv.org/html/2608.20153#A1.T6)provides detailed field\-level annotation guidelines\.

##### Cross\-Field Consistency Check

Before an instance is finalized, annotators jointly inspect the complete annotation chain\.

- •core\_claimmust accurately summarize the result identified bycore\_label\.
- •nl\_claimmust provide a self\-contained statement of the same result\.
- •fl\_theoremmust formalize the proposition expressed bynl\_claimwithout strengthening the assumptions or weakening the conclusion\.
- •fl\_proofmust provide a complete, machine\-verifiable proof of the formal theorem, and its main proof structure should remain consistent with the annotated argument\. If a revision to any field changes the mathematical meaning of the instance, all downstream fields must be re\-checked and revised accordingly\.
- •nl\_proofmust summarize the core proof strategy used in the source paper\.

## Appendix BPrompt

### B\.1Annotation

Table 7:The prompt of annotating natural language proof\.Natural\-Language Proof AnnotationYou are given a compact source context containing a completed Lean proof\. Your task is to generate only the natural\-language proof summary,nl\_proof\. Use only the supplied context\. Do not request tools, inspect files, or search the workspace\.The completed Lean proof is authoritative\. Any selected paper result is background and a localization hint only\. If it differs from the principal theorem actually proved in the Lean context, follow the proved Lean theorem and its completed proof\.Requirements:•Write everything in English\.•Disclose no authors, affiliations, email addresses, usernames, local paths, credentials, session identifiers, or execution metadata\.•Identify the principal completed Lean declaration represented by the compact context and summarize the proof of that declaration\.•Thenl\_proofmust faithfully describe the proof strategy and main reasoning steps actually implemented by the completed Lean proof\.•Preserve the logical direction and dependencies of the Lean proof\. Do not introduce arguments, assumptions, intermediate claims, or proof techniques that are not supported by the supplied context\.•Prefer a concise, self\-contained mathematical explanation over a line\-by\-line description of Lean tactics or implementation details\.Return only the content ofnl\_proof, with no label, metadata, or additional text\.Table 8:The prompt of annotating blueprint of formal language proof\.Formal\-Language Blueprint AnnotationRole\.You are*LeanArchitect*, an agent that converts an unorganized natural\-language mathematical proof or proof sketch into a single Lean 4 blueprint\. The blueprint is the canonical interface between mathematical reasoning and downstream formal proving\.Objective\.Produce a blueprint that simultaneously contains:1\.a rigorous, publication\-quality natural\-language proof encoded in LeanArchitect@\[blueprint\]annotations; and2\.a formally grounded Lean skeleton whose declarations accurately express the intended mathematics\.Every proof body of a blueprintlemmaortheoremmust be exactlysorryorsorry\_using\.Core Principles\.•Mathematical fidelity:preserve the source theorem, hypotheses, proof structure, and logical dependencies exactly\.•Formal grounding:ensure every Lean declaration is correctly typed against the installed Mathlib\. A type\-correct but mathematically inaccurate statement is unacceptable\.•High\-quality exposition:write statements and proof explanations with explicit hypotheses, quantifiers, dependencies, and rigorous justification, at the standard of a research mathematics paper\.•Repair\-radius minimization:decompose the proof so that uncertain, incorrect, or incomplete source steps are isolated behind small declarations with as few dependents as possible\.•Context discipline:inspect only information necessary for the current phase and avoid loading irrelevant material\.Hard Constraints\.•Do*not*repair, strengthen, or complete gaps in the source mathematics\. Preserve questionable steps and isolate them structurally\.•Do*not*formalize proofs with Lean tactics or proof terms\.•Use the designated Mathlib retrieval interface as the authoritative source for declaration discovery and API verification\.•Validate the working blueprint with Lean diagnostics and resolve statement\-level typing errors before delivery\.•Respect the provided workspace and tool boundaries; use only authorized tools for file editing, version control, and delivery\.Workflow\.Proceed sequentially through:Understand⟶Ground⟶Draft⟶Validate⟶Deliver\.\\text\{Understand\}\\;\\longrightarrow\\;\\text\{Ground\}\\;\\longrightarrow\\;\\text\{Draft\}\\;\\longrightarrow\\;\\text\{Validate\}\\;\\longrightarrow\\;\\text\{Deliver\}\.First reconstruct the intended mathematical argument and dependency structure\. Then retrieve and verify the relevant Mathlib concepts and declarations\. Next design the decomposition to minimize repair radius, write the annotated natural\-language proof and Lean skeleton, and finally run Lean diagnostics before delivery\.Output Standard\.The final blueprint must be self\-contained, mathematically faithful, structurally modular, and formally well\-typed\. Its natural\-language annotations should make the complete intended argument understandable to a mathematician, while its Lean declarations should provide precise and stable proof obligations for downstream provers\.Table 9:The prompt of annotating formal language proof\.Formal\-Language Proof AnnotationRole\.You are a node\-level Lean formalization agent\. Your goal is to complete the assignedtarget\_node: prove its fixed Lean statement and, when necessary, polish only its local title and natural\-language statement/proof descriptions\.Core Principles\.•Context discipline:Load only the information required by the current workflow phase\. Prioritize mathematical reasoning over unrelated context\.•Strict local scope:Modify only the editable region associated withtarget\_node\. Never change unrelated declarations or the formal statement of the target\.•Local refinement:When the proof is decomposable, introduce complete local helper nodes—such as intermediate lemmas, case analyses, algebraic identities, bounds, or API\-bridge facts—inside the target’s refinement region\. Preserve the global dependency DAG and keep the target as the unique terminal node\.•Completion first:The target and every newly introduced helper node must contain nosorry\. A long or difficult proof, or the absence of a convenient upstream lemma, is not by itself a valid blocker\.Hard Constraints\.•Never alter the target Lean statement\.•Never introduce axioms or usenative\_decide\.•Do not modify files outside the explicitly allowed Lean region and procedural state/delivery records\.•Use the designated MCP interfaces for Lean verification, Mathlib retrieval, dependency analysis, editing, Git operations, and repository delivery; do not bypass them with shell\-based alternatives\.•Treat the designated Mathlib retrieval tool as the sole source for Mathlib API discovery and the DAG tracker as the sole oracle for blueprint dependencies\.Workflow\.Read the runtime inputs and procedural state, determine the active phase, and execute only that phase’s required work\. Progress through validation, numerical analysis when needed, prose polishing, and Lean formalization\. Verify the completed proof with the provided Lean tools before delivery\.If the target can be completed under the current contracts, solve it directly or by adding complete local refinements\. File an issue only when there is concrete evidence that completion is impossible under the fixed specification, such as a false target statement, a genuinely missing hypothesis, inconsistent Lean/Mathlib behavior, invalid runtime input, or an unrecoverable tool failure\.Delivery\.A successful result must contain a fully verified proof oftarget\_nodeand all local refinement nodes, with no placeholders remaining\. Deliver the completed changes through the prescribed Git and repository tools; otherwise report the concrete blocking defect through the prescribed issue workflow\.The prompts used for annotation are shown in Table[7](https://arxiv.org/html/2608.20153#A2.T7), Table[8](https://arxiv.org/html/2608.20153#A2.T8), and Table[9](https://arxiv.org/html/2608.20153#A2.T9)\.

### B\.2Evaluation

Table 10:The prompt of the theorem elicitation\.Theorem Elicitationinput/core\_claim\.mdcontains a short informal claim describing the central result of a research paper\. Turn it into a precise natural\-language theorem statement\.Deliverable:write the statement tooutput/nl\_claim\.md\.Requirements:•Read the input with your own tools\. Never modify anything underinput/\.•State one theorem: quantify every object, name every hypothesis explicitly, and give the exact conclusion\. A reader must be able to formalize it without access to the paper\.•Keep it self\-contained: define or characterize every non\-standard notion you use\.•Write the statement only\. Do not include a proof, a proof sketch, or commentary\.•English only\. Mathematical notation is allowed\.•Finish only afteroutput/nl\_claim\.mdexists and contains the final statement\.Table 11:The prompt of the autoformalizationAutoformalizationinput/nl\_claim\.mdcontains a natural\-language theorem statement\.input/imports\.leancontains the Mathlib import lines the reference formalization uses\. No definitions are given: choosing the Lean representation of every notion in the claim is part of the task\.Deliverable:write one self\-contained Lean 4 file tooutput/statement\.lean\.Requirements:•Read the inputs with your own tools\. Never modify anything underinput/\.•output/statement\.leanmust hold, in this order: the import lines, then every auxiliarydef,abbrev,notation, orinstanceyour formalization needs, then exactly one top\-leveltheoremthat formalizes the claim and ends with:=, with no proof\. Keep imports narrow; add further Mathlib imports only when you actually need them\.•Formalize the claim faithfully: every hypothesis and the exact conclusion of the informal statement must appear, with no extra assumptions that weaken it and no definition that makes it vacuous\.•project/candidate\.leanis a scratch file seeded with the same imports\. Develop there, append:= by sorryto your theorem, and run\./check\.shto type\-check against the shared Mathlib build\. The script compiles concurrently, so run it as often as you need\. Adeclaration uses ’sorry’warning is expected; any error is not\.•Equivalence with the reference formalization is checked mechanically in both directions, so a file that merely type\-checks but weakens, strengthens, or trivializes the claim scores zero\.•Finish only afteroutput/statement\.leantype\-checks \(with:= by sorryappended\) and holds the statement without its proof\.Table 12:The prompt of the proof elicitationProof Elicitationinput/nl\_claim\.mdcontains a natural\-language theorem statement andinput/theorem\.leancontains its Lean 4 formalization, including the auxiliary definitions it depends on\. The Lean proof itself is withheld \(by sorry\)\.Deliverable:write a complete natural\-language proof tooutput/nl\_proof\.md\.Requirements:•Read the inputs with your own tools\. Never modify anything underinput/\.•Prove the stated theorem, using the Lean definitions as the authoritative meaning of every notion that appears in it\.•Justify every step\. State which hypothesis, standard theorem, or computation licenses each inference, and make the overall structure \(induction, contradiction, case analysis\) explicit\.•Cover every case: the proof must be complete, not a sketch, and must not assume the result\.•Lean code is neither required nor forbidden; mathematical rigour is what is graded\.•English only\. Finish only afteroutput/nl\_proof\.mdcontains the final proof\.Table 13:The prompt of the theorem proof\.Theorem Provingproject/is a ready\-to\-build Lake project\.project/theorem\.leanholds narrow Mathlib imports, the auxiliary definitions of this problem, and exactly one theorem whose proof isby sorry\. The shared prebuilt Mathlib is already linked intoproject/\.lake/packages, so never download, copy, or rebuild Mathlib or any dependency\.Deliverable:write the complete proved file tooutput/proof\.lean\.Requirements:•Prove the theorem by replacingsorrywith a real proof\. Work inproject/theorem\.lean\.•Do not change the theorem statement, its name, its binders, or the existing definitions\. You may add auxiliary lemmas above the theorem and may add narrow Mathlib imports\.•Forbidden anywhere in the file:sorry,admit,stop,sorryAx,axiom,native\_decide, and anyset\_optionthat relaxeswarn\.sorryorwarningAsError\. Verification recompiles the file strictly, audits the environment axioms of the target declaration, and replays the proof in a fresh kernel, so none of these can pass\.•\./check\.shcompilesproject/theorem\.leanwith\-Dwarn\.sorry=true \-DwarningAsError=trueand with parallel workers\. Iterate with it until it reports no errors and no warnings\.•Then copy the final file verbatim tooutput/proof\.lean\.•Partial credit does not exist: only a fully verified proof counts\. If time runs out, still copy your best complete\-file attempt tooutput/proof\.lean\.The prompts used for evaluation are shown in Table[10](https://arxiv.org/html/2608.20153#A2.T10), Table[11](https://arxiv.org/html/2608.20153#A2.T11), Table[12](https://arxiv.org/html/2608.20153#A2.T12), and Table[13](https://arxiv.org/html/2608.20153#A2.T13)\.

### B\.3Generation

Table 14:The prompt of the planner\.Prompt of PlannerYou are the planner of an autonomous theoretical\-computer\-science research loop\. The workspace is shared with the other agents of this loop\.Workspace layout:•benchmark/<id\>/— one sampled benchmark instance per directory, holdingcore\_claim\.md,nl\_theorem\.md\(the natural\-language theorem\), andtheorem\.lean\(its formal statement\)\.•accepted/claim\-<k\>/— claims already accepted by the judger earlier in this run, holdingclaim\.md\(natural\-language summary\) andtheorem\.lean\.•feedback/claim\-<k\>\.md— why earlier attempts were discarded, written by the loop\.•objectives/claim\-<k\>\.md— the research objectives you have proposed so far\.Your job this turn:propose exactly one new research objective and write it to the objective file named in the instructions\. Base it on the benchmark content and everything accumulated in the workspace so far\. You are not restricted to extending the current line of reasoning: you may reformulate the problem, introduce auxiliary concepts, strengthen or relax assumptions, or explore an alternative analytical direction\. The objective must be a self\-contained result that is plausible to state precisely and to formalize in Lean 4 with Mathlib\.The objective file must be markdown with these sections:•\#\# Motivation— why this result is worth pursuing and how it relates to what is in the workspace\.•\#\# Informal Claim— the precise mathematical statement you want, with all symbols defined\.•\#\# Assumptions— every assumption on the setting, explicitly listed\.•\#\# Proof Direction— a sketch of how the result could be proven\.•\#\# Novelty— what distinguishes it from the benchmark instances and the accepted claims\.Write the file, then stop\. Do not write any other file\.Table 15:The prompt of the formalizer\.Prompt of FormalizerYou are the formalizer of an autonomous theoretical\-computer\-science research loop\. Your working directory holds one proposed research objective:•objective\.md— the objective you must formalize now\.•project/— a ready\-to\-build Lake project\.project/theorem\.leanis where you write the formal statement\. The shared prebuilt Mathlib is already linked intoproject/\.lake/packages, so never download, copy, or rebuild Mathlib or any dependency\.•\./check\.sh— compilesproject/theorem\.leanwith parallel workers\. Run it as often as you need from your working directory\.Deliverable:a compilingproject/theorem\.leanthat contains•narrow Mathlib imports \(neverimport Mathlib\),•any auxiliary definitions the statement needs,•exactly one main theorem or lemma, as the last declaration, whose proof is exactlyby sorry, and no othersorryanywhere in the file\.Requirements:•Do not prove the theorem\. The main declaration must end with:= by sorry\.•You may adjust the informal claim’s internal representation \(definitions, naming, auxiliary lemmas\) to keep the formalization tractable, but the overall conclusion must match the objective\.•Forbidden anywhere in the file:axiom,native\_decide,sorryAx,admit,stop, and anyset\_optionthat relaxeswarn\.sorryorwarningAsError\.•Keep iterating with\./check\.shuntil it reports no errors\. Only warnings about thesorryof the main declaration are acceptable\.•If you conclude the objective cannot be formalized within your budget, writefailure\.mdin your working directory explaining precisely what failed and why, and stop\.Table 16:The prompt of the judger\.Prompt of JudgerYou are the judger of an autonomous theoretical\-computer\-science research loop\. Your working directory holds one candidate formal claim:•objective\.md— the research objective that was formalized\.•project/theorem\.lean— the formal Lean statement that compiles; its last declaration is the main theorem and its proof isby sorry\.•\.\./\.\.— the shared workspace, whosebenchmark/holds the sampled benchmark instances and whoseaccepted/holds claims already accepted in this run\.Your job this turn: translate the formal statement back into one concise natural\-language claim that summarizes what it asserts and its potential theoretical significance, then judge whether the proposed result is worth keeping\.Deliverable:write a JSON object with exactly these keys tojudgement\.jsonin your working directory, and make your final message exactly that JSON object:```
{
    "nl_claim": "...",
    "significance": "...",
    "novel": true,
    "rationale": "..."
}
```

•nl\_claim: the concise natural\-language claim, self\-contained and precise\.•significance: one or two sentences on the potential theoretical significance\.•novel:trueonly if the claim is sufficiently novel and valuable to keep — not a trivial restatement of a benchmark instance or an accepted claim, not a degenerate or vacuous statement, and not an elementary exercise\.•rationale: the reasoning behind thenovelverdict\.The prompts used by our auto research framework are shown in Table[14](https://arxiv.org/html/2608.20153#A2.T14), Table[15](https://arxiv.org/html/2608.20153#A2.T15), and Table[16](https://arxiv.org/html/2608.20153#A2.T16)\.

## Appendix CCase Study

Table 17:The case ofFormalTCSfrom STOC\.Table 18:The case ofFormalTCSfrom FOCS\.Table 19:The case ofFormalTCSfrom SODA\.Table 20:The case ofFormalTCSfrom COLT\.In this part, we show several representative cases of each conference in Table[17](https://arxiv.org/html/2608.20153#A3.T17), Table[18](https://arxiv.org/html/2608.20153#A3.T18), Table[19](https://arxiv.org/html/2608.20153#A3.T19), and Table[20](https://arxiv.org/html/2608.20153#A3.T20)\. Due to the page limit, we omit the natural\-language claims and proof\.

## Appendix DLLM and Harness Version

Table 21:The versions of LLMs and harnesses used in our evaluation and auto research\.The versions of LLMs and harnesses used in our evaluation and auto research are shown in Table[21](https://arxiv.org/html/2608.20153#A4.T21)\.

## Appendix EAnnotation Agreement

Table 22:The annotation agreement ofFormalTCS\.Inter\-Expert Agreementdenotes the percentage of annotations on which two experts independently reach the same judgment or result\.Expert Modification of LLM Outputdenotes the percentage of LLM\-generated annotations that require substantive correction by an expert\.To assess the reliability of the annotation process ofFormalTCS, we measure agreement both among human experts and between experts and LLM\-assisted annotations, as reported in Table[22](https://arxiv.org/html/2608.20153#A5.T22)\. Overall, our annotation pipeline exhibits high inter\-expert agreement and relatively low rates of substantive human revision\. For annotation stages requiring independent expert cross\-validation, the agreement rates for core claims, natural language claims, and formal language proof reach86%86\\%,90%90\\%, and93%93\\%, respectively, indicating that different experts largely agree on the identification of central research results, theorem semantics, and the correctness of formal proofs\. For annotations generated with LLM assistance, the proportion requiring substantive expert revision ranges from13%13\\%to31%31\\%\. Specifically, the revision rates for natural language proof and formal language proof are only13%13\\%and15%15\\%, respectively, while the proof blueprint requires revision in24%24\\%of cases, and the formal language theorem has the highest revision rate at31%31\\%\. This difference suggests that, compared with generating complete proofs, accurately translating mathematical statements from research papers into type\-correct formal theorems with complete assumptions and equivalent semantics remains more prone to errors that require expert correction\. Overall, these results show that LLM assistance can substantially reduce the manual effort required during annotation while also confirming that expert review remains indispensable for ensuring semantic faithfulness in formalization and the quality of the final benchmark\.

## Appendix FRubric Agreement

Table 23:The rubric agreement between LLMs and human experts\. Considering the cost, we randomly sample1616examples fromFormalTCSin this table\.Δ\\Deltais calculated as\|𝙻𝙻𝙼−𝙷𝚞𝚖𝚊𝚗\|\(𝙻𝙻𝙼\+𝙷𝚞𝚖𝚊𝚗\)/2\\frac\{\|\\mathtt\{LLM\}\-\\mathtt\{Human\}\|\}\{\(\\mathtt\{LLM\}\+\\mathtt\{Human\}\)/2\}to measure the difference between human and LLMs\.Table[23](https://arxiv.org/html/2608.20153#A6.T23)compares the LLM\-based rubric scores with human expert evaluations on the randomly sampled examples\. Overall, the LLM\-based evaluator exhibits strong consistency with human judgments across both CC2NC and C2NP\. Although the LLM evaluator systematically assigns slightly higher scores than human experts, the relative discrepancy remains limited, ranging from3\.17%3\.17\\%to6\.57%6\.57\\%on CC2NC and from6\.77%6\.77\\%to10\.67%10\.67\\%on C2NP, with average discrepancies of4\.43%4\.43\\%and8\.14%8\.14\\%, respectively\. More importantly, the LLM and human evaluations produce exactly the same ranking of all evaluated model configurations on both tasks, identifyingGPT\-5\.6\-solas the best\-performing model on CC2NC andClaude\-Opus\-5as the best\-performing model on C2NP\. This rank\-level agreement indicates that, despite a modest difference in absolute score calibration, the LLM\-based rubric reliably preserves the relative performance differences among models\. The somewhat larger discrepancy on C2NP also suggests that evaluating proof\-strategy generation may involve greater judgment ambiguity than evaluating natural\-language claim understanding\. Overall, these results support the use of the LLM\-based rubric as a scalable proxy for human evaluation in our main experiments\.

## Appendix GBlack\-Box Audit for Paper Leakage

Because the training corpora of proprietary LLMs are not publicly available, we perform an output\-only audit following prior contamination and membership\-inference studies that probe memorization by reconstructing held\-out text from partial context\([9](https://arxiv.org/html/2608.20153#bib.bib34);[10](https://arxiv.org/html/2608.20153#bib.bib33)\)\. For each retained paper, we construct three complementary probes:*\(i\) theorem completion*, where the model receives only an initial fragment of a theorem statement;*\(ii\) proof continuation*, where only the beginning of a proof is provided; and*\(iii\) result reconstruction*, where the model is given a short anonymized description of a main result\. We remove titles, author names, venue information, theorem numbers, citations, and other identifying metadata, and queryGPT\-5\.6\-solandClaude\-Opus\-5without retrieval access\. Each generated response is compared only against the withheld source content using token\-level lexical similarity \(ROUGE\-L/LCS\)\. We deliberately emphasize lexical rather than semantic similarity since near\-verbatim reconstruction provides a more specific signal of memorization, whereas an independently derived but semantically equivalent answer does not\. The aggregate completion similarity is below9\.6%9\.6\\%for both models, providing no strong evidence of memorized reconstruction in the retained papers\. We treat this audit as evidence of relatively low contamination risk rather than proof of non\-exposure since failure to reproduce a passage cannot rule out its presence in the training data\([33](https://arxiv.org/html/2608.20153#bib.bib35)\)\.