SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization

# Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization
Source: [https://arxiv.org/html/2608.29270](https://arxiv.org/html/2608.29270)
\\tl\_set:Ne\\codebox

codebox

Hojae HanJongyoon Kim11footnotemark:1Sanghyuk Park11footnotemark:1Dongwook CheonMyungjae Jeon††thanks:These authors contributed equally to this work\.Affiliation:Electronics and Telecommunications Research InstituteAffiliation:Seoul National UniversityAffiliation:University of Maryland, College ParkEmail:[affilSNUhojae\.han@etri\.re\.kr](mailto:[email protected])Sunjong ChoiSoonho KongWonseok HeoSeung\-won HwangDonghoon Hyeon22footnotemark:2††thanks:Corresponding authors\.Email:[˜\{john\.jongyoon\.kim,202123018,seungwonh,dhyeon\}@snu\.ac\.kr](mailto:%CB%9C)Affiliation:Seoul National UniversityAffiliation:Amazon Web Services

###### Abstract

Autoformalization translates informal mathematical theorems into code for proof assistants such as Lean\. A central challenge is that current evaluation metrics can accept type\-correct but misaligned statements or reject correct statements written in a different formulation\. Inspired by Pass@kk, we proposeSA\-Pass\(*Semantic Alignment Pass*\), which tests formal statements using auxiliary statements called*shadows*that characterize the intended statement\. A generated statement receives full credit only when it compiles, implies each shadow \(forward check\), and is implied by their conjunction \(backward check\)\. We instantiateSA\-PassinShadowBench, a Lean 4 full autoformalization benchmark of 178 postgraduate\- to research\-level problems spanning eight mathematical areas\. Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent reaches61\.8%61\.8\\%compile rate and11\.2%11\.2\\%SA\-Pass\. Across outputs generated by six agentic configurations,SA\-Passachieves98\.8%98\.8\\%binary agreement with expert judgments\. An early version ofShadowBenchserved as the benchmark for Track 4 of the ICML 2026 AI4Math Challenge\.111[https://github\.com/ldilab/shadowbench](https://github.com/ldilab/shadowbench)

††Contact information for all authors is provided in[AppendixL](https://arxiv.org/html/2608.29270#A12)\.## 1Introduction

Autoformalization translates informal mathematics written in natural language into code for proof assistants such as Lean\.222[https://lean\-lang\.org/](https://lean-lang.org/)In the full autoformalization setting, the input is an informal theorem statement and proof, and the output is code containing the corresponding formal statement and proof\. The proof assistant can then mechanically check whether the formal proof proves the formal statement\.

T:=A⇒BT:=A\\Rightarrow BS1:=A⇒B1S\_\{1\}:=A\\Rightarrow B\_\{1\}S2:=A⇒B2S\_\{2\}:=A\\Rightarrow B\_\{2\}T⇒S1T\\Rightarrow S\_\{1\}T⇒S2T\\Rightarrow S\_\{2\}S1∧S2⇒TS\_\{1\}\\wedge S\_\{2\}\\Rightarrow T

\(a\)Intended theorem and shadows\.
T^1:=A⇒B1\\widehat\{T\}\_\{1\}:=A\\Rightarrow B\_\{1\}S1:=A⇒B1S\_\{1\}:=A\\Rightarrow B\_\{1\}S2:=A⇒B2S\_\{2\}:=A\\Rightarrow B\_\{2\}T^1⇒S1\\widehat\{T\}\_\{1\}\\Rightarrow S\_\{1\}T^1⇏S2\\widehat\{T\}\_\{1\}\\nRightarrow S\_\{2\}S1∧S2⇒T^1S\_\{1\}\\wedge S\_\{2\}\\Rightarrow\\widehat\{T\}\_\{1\}

\(b\)Forward check failure\.
T^2:=A⇒\\widehat\{T\}\_\{2\}:=A\\RightarrowB1∧B2∧RB\_\{1\}\\wedge B\_\{2\}\\wedge RS1:=A⇒B1S\_\{1\}:=A\\Rightarrow B\_\{1\}S2:=A⇒B2S\_\{2\}:=A\\Rightarrow B\_\{2\}T^2⇒S1\\widehat\{T\}\_\{2\}\\Rightarrow S\_\{1\}T^2⇒S2\\widehat\{T\}\_\{2\}\\Rightarrow S\_\{2\}S1∧S2⇏T^2S\_\{1\}\\wedge S\_\{2\}\\nRightarrow\\widehat\{T\}\_\{2\}

\(c\)Backward check failure\.

Figure 1:Illustrative example of shadow theorem checks\. HereA,B,B1,B2A,B,B\_\{1\},B\_\{2\}are predicates andB⇔B1∧B2B\\Leftrightarrow B\_\{1\}\\wedge B\_\{2\}\. The intended theorem statementTTimplies both shadows \(S1S\_\{1\},S2S\_\{2\}\), and the two shadows jointly implyTT\. The shadow theorem statement checks reject both generated theorems\. The forward check finds thatT^1\\widehat\{T\}\_\{1\}does not implyS2S\_\{2\}, and the backward check finds thatS1∧S2S\_\{1\}\\wedge S\_\{2\}does not implyT^2\\widehat\{T\}\_\{2\}\.The core challenge for evaluation is to assess whether the generated formal statement expresses the same mathematics as the informal statement\([Ospanov et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib56);[Ammanamanchi et al\., 2026](https://arxiv.org/html/2608.29270#bib.bib57)\)\. Existing automatic metrics either rely on compile rate signals that can accept misaligned statements, assign scores without formally checking the intended meaning, or require equivalence to a fixed reference formulation that can reject correct statements expressed differently \([Section2\.2](https://arxiv.org/html/2608.29270#S2.SS2)\)\. An alternative is manual judgment by mathematicians familiar with Lean, which is reliable yet too costly to scale for repeated evaluations\([Wu et al\., 2022](https://arxiv.org/html/2608.29270#bib.bib37);[Fang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib41);[Ying et al\., 2024](https://arxiv.org/html/2608.29270#bib.bib39)\)\.

In this paper, we proposeSA\-Pass\(*Semantic Alignment Pass*\), an automatic metric that scores semantic alignment through forward and backward implication checks\.SA\-Passfollows the Pass@kkidea from code generation, where an output is accepted only if it passes all tests for the task\([Chen et al\., 2021](https://arxiv.org/html/2608.29270#bib.bib31)\)\. For formal statements, we define these checks using a complete set of*shadow theorems*: auxiliary theorems selected such that each shadow is implied by the intended theorem and the shadows together characterize it \([Figure1\(a\)](https://arxiv.org/html/2608.29270#S1.F1.sf1)\)\. During evaluation, a generated formalization receives the maximumSA\-Passscore only if it compiles, its statement implies every shadow in the forward checks \([Figure1\(b\)](https://arxiv.org/html/2608.29270#S1.F1.sf2)\), and its statement is implied by the shadows’ conjunction in the backward check \([Figure1\(c\)](https://arxiv.org/html/2608.29270#S1.F1.sf3)\)\.

This design makes expert supervision reusable: a shadow set is constructed once for each intended theorem rather than separately for every generated formalization\. Experts construct the set by revising LLM\-generated drafts \([Section4\.1](https://arxiv.org/html/2608.29270#S4.SS1)\), and Lean mechanically verifies the set completeness \([Section3\.2](https://arxiv.org/html/2608.29270#S3.SS2)\)\. The same shadow checkers can then be reused to evaluate any number of generated formalizations automatically\.

AlongsideSA\-Pass, we introduceShadowBench, a Lean 4 full\-autoformalization benchmark comprising 178 postgraduate\- to research\-level problems across eight mathematical areas and three difficulty levels\. Each problem is annotated with a complete set of shadow theorems, enabling automatic evaluation withSA\-Pass\. Existing benchmarks such as ProofNet[Azerbayev et al\. \(2023\)](https://arxiv.org/html/2608.29270#bib.bib33)primarily contain short formalizations with a single conclusion\. In contrast,ShadowBenchtargets multi\-conclusion problems whose reference formalizations are about 1\.6 times longer lines on average \([Table9](https://arxiv.org/html/2608.29270#A1.T9)\)\. An early version ofShadowBench, comprising 126 problems, served as the benchmark for Track 4 of the ICML 2026 AI4Math Challenge, with analyses of the results provided in[AppendixG](https://arxiv.org/html/2608.29270#A7)\.

Empirically, Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent[Liu et al\. \(2026a\)](https://arxiv.org/html/2608.29270#bib.bib54)achieves a61\.8%61\.8\\%compile rate onShadowBench, yet only11\.2%11\.2\\%of its outputs passSA\-Pass\([Table3](https://arxiv.org/html/2608.29270#S5.T3)\)\.SA\-Passachieves98\.8%98\.8\\%binary agreement with expert judgments for generated outputs across six agentic configurations, whereas compile rate and BEq\+\([Liu et al\., 2025a](https://arxiv.org/html/2608.29270#bib.bib43);[Poiroux et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib1)\)achieve17\.8%17\.8\\%and80\.6%80\.6\\%, respectively \([Table4](https://arxiv.org/html/2608.29270#S5.T4)\)\.

We summarize our contributions as follows\.

- •We introduceSA\-Pass, an automated metric that evaluates semantic alignment between formal and informal statements through Lean\-checkable shadow theorems\.
- •We constructShadowBench, a Lean 4 full autoformalization benchmark that usesSA\-Passas its main evaluation metric across 178 postgraduate\- to research\-level problems\. Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent reaches61\.8%61\.8\\%compile rate and11\.2%11\.2\\%SA\-Pass\.
- •SA\-Passachieves98\.8%98\.8\\%binary agreement with expert judgments\.

## 2Related Work

### 2\.1Autoformalization Tasks and Benchmarks

Autoformalization is a task that translates an informal theorem into a formal theorem in a proof assistant such as Lean, for either the statement or the proof\. For statement autoformalization, various methods have been proposed\([Wu et al\., 2022](https://arxiv.org/html/2608.29270#bib.bib37);[Liu et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib46);[Lu et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib47);[Fang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib41);[Chen et al\., 2026](https://arxiv.org/html/2608.29270#bib.bib42)\)and evaluated on benchmarks spanning difficulty levels from high school to undergraduate\([Gao et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib38);[Ying et al\., 2024](https://arxiv.org/html/2608.29270#bib.bib39);[Murphy et al\., 2024](https://arxiv.org/html/2608.29270#bib.bib40);[Xie et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib45)\)\.[Lu et al\. \(2024\)](https://arxiv.org/html/2608.29270#bib.bib34);[Jana et al\. \(2026\)](https://arxiv.org/html/2608.29270#bib.bib35)have studied full autoformalization, which produces both the statement and its proof from natural language\. At the proof level, this task is mostly discussed as theorem proving, where various methods\([Yang et al\., 2023](https://arxiv.org/html/2608.29270#bib.bib49);[Xin et al\., 2024](https://arxiv.org/html/2608.29270#bib.bib50);[Lin et al\., 2025a](https://arxiv.org/html/2608.29270#bib.bib51);[Wang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib52);[Liu et al\., 2026a](https://arxiv.org/html/2608.29270#bib.bib54)\)generate a formal proof given the formal statement, evaluated on benchmarks such as miniF2F and ProofNet\([Zheng et al\., 2022](https://arxiv.org/html/2608.29270#bib.bib48);[Azerbayev et al\., 2023](https://arxiv.org/html/2608.29270#bib.bib33)\), and on research\-level Lean projects\([Poiroux et al\., 2025a](https://arxiv.org/html/2608.29270#bib.bib36)\)\. While these benchmarks establish the task setting, our focus is the complementary problem of evaluating whether generated formal statements are semantically aligned with the intended theorem\.

### 2\.2Semantic Alignment Evaluation

#### Compile rate\.

Compile rate runs the generated Lean code through the Lean compiler and counts it as correct when the generated theorem statement and proof type\-check[Azerbayev et al\. \(2023\)](https://arxiv.org/html/2608.29270#bib.bib33)\. It rejects ill\-formed or unproved Lean code, but it can produce false positives when a generated proof type\-checks for a statement that differs from the informal theorem[Liu et al\. \(2025a\)](https://arxiv.org/html/2608.29270#bib.bib43);[Ammanamanchi et al\. \(2026\)](https://arxiv.org/html/2608.29270#bib.bib57)\.

#### Reference\-based metrics\.

Several metrics evaluate generated statements against a reference formalization\. BLEU\([Azerbayev et al\., 2023](https://arxiv.org/html/2608.29270#bib.bib33);[Papineni et al\., 2002](https://arxiv.org/html/2608.29270#bib.bib30)\)measures lexical overlap with the reference theorem, TransTED\([Liu et al\., 2026b](https://arxiv.org/html/2608.29270#bib.bib44)\)compares structural similarity to the reference theorem, and FormalAlign\([Lu et al\., 2025a](https://arxiv.org/html/2608.29270#bib.bib55)\)and LLM\-as\-judge\([Guo et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib29)\)score the generated statement against the informal statement\. Because these lexical, structural, and model\-based scores are not implication checks, they can produce both false positives and false negatives\. BEq and BEq\+\([Liu et al\., 2025a](https://arxiv.org/html/2608.29270#bib.bib43);[Poiroux et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib1)\)use Lean tactics to prove equivalence with the reference statement, but they create false negatives by rejecting correct statements whose formulations differ from the fixed reference \([Table4](https://arxiv.org/html/2608.29270#S5.T4)\)\.

#### Expert judgments\.

Manual judgment by mathematicians familiar with Lean remains reliable, but it does not scale to large or repeated evaluations\([Wu et al\., 2022](https://arxiv.org/html/2608.29270#bib.bib37);[Fang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib41);[Ying et al\., 2024](https://arxiv.org/html/2608.29270#bib.bib39)\)\.

#### Test\-based metrics\.

Testing Accuracy\([Kim et al\., 2026](https://arxiv.org/html/2608.29270#bib.bib32)\)treats the dependent successor theorems as test cases, accepting a generated theorem when all of them compile\. This approach can produce false positives, since passing all successor theorem tests does not guarantee semantic alignment with the intended informal statement\.

#### Our distinction\.

SA\-Passaddresses both false positives and false negatives in semantic alignment by evaluating generated statements against a complete set of auxiliary theorems\.SA\-Passverifies generated statement with a complete set of both forward and backward implication checks, obtaining98\.8%98\.8\\%binary agreement with expert judgments \([Table4](https://arxiv.org/html/2608.29270#S5.T4)\)\.

## 3SA\-Pass: Semantic Alignment Pass

### 3\.1Task and Shadow Theorems

###### Definition 1\(Full autoformalization task\)\.

Given an informal theorem statement and its proof, the full autoformalization task is to generate a formal statementT^\\widehat\{T\}together with a machine\-checkable proof ofT^\\widehat\{T\}\. LetTTdenote the intended formal statement\. The semantic alignment objective isT^⇔T\\widehat\{T\}\\Leftrightarrow T\.

###### Definition 2\(Shadow theorem\)\.

For an intended formal statementTT, a shadow theorem consists of an auxiliary formal statementSSand a machine\-checkable proof ofSS\. Its forward checker theorem states thatTTimpliesSS:

### 3\.2Complete Shadow Sets

###### Definition 3\(Complete shadow set\)\.

LetTTbe the intended formal statement, and let𝒮=\{S1,…,Sn\}\\mathcal\{S\}=\\\{S\_\{1\},\\ldots,S\_\{n\}\\\}be a finite set of shadow statements\. The set𝒮\\mathcal\{S\}is*complete*if the shadows jointly characterizeTT, i\.e\., the backward checker theorem states

S1∧⋯∧Sn⇒T\.S\_\{1\}\\wedge\\cdots\\wedge S\_\{n\}\\Rightarrow T\.Together with the forward checker theoremsT⇒SiT\\Rightarrow S\_\{i\}, this givesS1∧⋯∧Sn⇔TS\_\{1\}\\wedge\\cdots\\wedge S\_\{n\}\\Leftrightarrow T\.

The completeness of a shadow set is verified in Lean by compiling checker theorems in both directions\. For each shadowSiS\_\{i\}, we compile a forward checker theorem establishingT⇒Si\.T\\Rightarrow S\_\{i\}\.A candidate shadow is accepted only if its forward checker compiles\. We then compile the backward checker theoremS1∧⋯∧Sn⇒T\.S\_\{1\}\\wedge\\cdots\\wedge S\_\{n\}\\Rightarrow T\.The backward checker theorem compiles only when the shadow statements jointly implyTT, which is precisely the completeness condition illustrated in[Figure2](https://arxiv.org/html/2608.29270#S3.F2)\.

The annotation process of complete shadow sets and corresponding checker theorems can be mostly automated \([Section4\.1](https://arxiv.org/html/2608.29270#S4.SS1)\)\.

The following example shows common ways to build complete shadow sets\. Additional checker patterns appear in[AppendixK](https://arxiv.org/html/2608.29270#A11)\.

TTS1S\_\{1\}S2S\_\{2\}⋯\\cdotsSnS\_\{n\}𝒮\\mathcal\{S\}T⇒S1T\\Rightarrow S\_\{1\}T⇒S2T\\Rightarrow S\_\{2\}T⇒SnT\\Rightarrow S\_\{n\}⋀iSi⇒T\\bigwedge\_\{i\}S\_\{i\}\\Rightarrow TFigure 2:A complete shadow set\. Each shadow statementSiS\_\{i\}follows from the intended formal statementTT\. The set is complete when the shadows jointly implyTT\.![Refer to caption](https://arxiv.org/html/2608.29270v1/shadow_pipeline.png)Figure 3:Evaluation procedure forSA\-PassandSA\-Passsofton oneShadowBenchproblem\.###### Example 1\(Bundled conclusions\)\.

SupposeA,B1,…,BnA,B\_\{1\},\\ldots,B\_\{n\}are predicates and the intended formal statement has the form

A⇒B1∧⋯∧Bn\.A\\Rightarrow B\_\{1\}\\wedge\\cdots\\wedge B\_\{n\}\.For eachii, define a shadow theorem

Si:A⇒Bi\.S\_\{i\}:A\\Rightarrow B\_\{i\}\.Then𝒮\\mathcal\{S\}is complete, because the individual components can be assembled back into the bundled conclusion\.

[SectionsK\.1](https://arxiv.org/html/2608.29270#A11.SS1)and[K\.2](https://arxiv.org/html/2608.29270#A11.SS2)show the corresponding Lean checkers\.

### 3\.3SA\-PassScoring

###### Definition 4\(Passing condition\)\.

For a problem whose intended formal statement isTT, a generated formal theorem with statementT^\\widehat\{T\}passes if and only if its declaration and proof type\-check in Lean and it passes the forward checks

T^⇒S1,T^⇒S2,…,T^⇒Sn\\widehat\{T\}\\Rightarrow S\_\{1\},\\quad\\widehat\{T\}\\Rightarrow S\_\{2\},\\quad\\ldots,\\quad\\widehat\{T\}\\Rightarrow S\_\{n\}and the backward check

S1∧⋯∧Sn⇒T^,S\_\{1\}\\wedge\\cdots\\wedge S\_\{n\}\\Rightarrow\\widehat\{T\},where𝒮=\{S1,…,Sn\}\\mathcal\{S\}=\\\{S\_\{1\},\\ldots,S\_\{n\}\\\}is a complete shadow set forTT\.

During evaluation, we append the forward and backward checkers to the generated Lean code, and compile the resulting file\.

Because𝒮\\mathcal\{S\}is complete, passing all forward checks establishesT^⇒S1∧⋯∧Sn⇒T\\widehat\{T\}\\Rightarrow S\_\{1\}\\wedge\\cdots\\wedge S\_\{n\}\\Rightarrow T\. Passing the backward check certifiesT⇒S1∧⋯∧Sn⇒T^T\\Rightarrow S\_\{1\}\\wedge\\cdots\\wedge S\_\{n\}\\Rightarrow\\widehat\{T\}, and it rejects generated formal statements that add constraints not required by the intended formal statement\. For example, if the generated formal statement has the formT^=T∧R\\widehat\{T\}=T\\wedge Rfor an arbitrary extra requirementRR, thenT^⇒T\\widehat\{T\}\\Rightarrow TbutT⇏T^T\\nRightarrow\\widehat\{T\}\. Together, the forward and backward checks establishT^⇔T\\widehat\{T\}\\Leftrightarrow T\.

The passing condition in[Definition4](https://arxiv.org/html/2608.29270#Thmdefinition4)induces the following binary semantic\-alignment metric\.

###### Definition 5\(SA\-Pass\)\.

For a generated formal theorem with statementT^\\widehat\{T\}and a complete shadow set𝒮=\{S1,…,Sn\}\\mathcal\{S\}=\\\{S\_\{1\},\\ldots,S\_\{n\}\\\}, define

SA\-Pass​\(T^,𝒮\)=\{1,if​T^​compiles,T^⇒Si​for all​i,and​⋀i=1nSi⇒T^;0,otherwise\.\\text\{\{SA\-Pass\} \}\(\\widehat\{T\},\\mathcal\{S\}\)=\\begin\{cases\}1,&\\begin\{array\}\[\]\{l\}\\text\{if \}\\widehat\{T\}\\text\{ compiles, \}\\\\ \\widehat\{T\}\\Rightarrow S\_\{i\}\\text\{ for all \}i,\\\\ \\text\{and \}\\bigwedge\_\{i=1\}^\{n\}S\_\{i\}\\Rightarrow\\widehat\{T\};\\end\{array\}\\\\ 0,&\\text\{otherwise\.\}\\end\{cases\}

Since𝒮\\mathcal\{S\}is complete for the intended formal statementTT,SA\-Pass​\(T^,𝒮\)=1\\text\{\{SA\-Pass\} \}\(\\widehat\{T\},\\mathcal\{S\}\)\{=\}1certifiesT^⇔T\\widehat\{T\}\\Leftrightarrow T\.

###### Definition 6\(SA\-Passsoft\)\.

LetT^\\widehat\{T\}be the statement of a generated formal theorem, and let𝒮=\{S1,…,Sn\}\\mathcal\{S\}=\\\{S\_\{1\},\\ldots,S\_\{n\}\\\}be a complete shadow set\. If the generated theorem does not type\-check in Lean, setSA\-Passsoft​\(T^,𝒮\)=0\\text\{\{SA\-Pass\}$\{\}\_\{\\mathrm\{soft\}\}$ \}\(\\widehat\{T\},\\mathcal\{S\}\)\{=\}0\. Otherwise, itsSA\-Passsoftscore is

SA\-Passsoft\(T^,𝒮\):=12⋅\|\{i:T^⇒Si\}\|\|𝒮\|﹈forward checks\+12⋅𝟏\{⋀i=1nSi⇒T^\}﹈backward check\.\\text\{\{SA\-Pass\}$\{\}\_\{\\mathrm\{soft\}\}$ \}\(\\widehat\{T\},\\mathcal\{S\}\):=\\frac\{1\}\{2\}\\cdot\\underbracket\{\\frac\{\|\\\{i:\\widehat\{T\}\\Rightarrow S\_\{i\}\\\}\|\}\{\|\\mathcal\{S\}\|\}\}\_\{\\text\{forward checks\}\}\\\\ \+\\frac\{1\}\{2\}\\cdot\\underbracket\{\\mathbf\{1\}\\\{\\bigwedge\_\{i=1\}^\{n\}S\_\{i\}\\Rightarrow\\widehat\{T\}\\\}\}\_\{\\text\{backward check\}\}\.\(1\)Here𝟏​\{ϕ\}\\mathbf\{1\}\\\{\\phi\\\}equals11if the corresponding checker theorem type\-checks in Lean, and00otherwise\.

A generated statement may become weaker than the intended theorem by adding assumptions, or stronger by omitting them\.SA\-Passsoftassigns partial credit in such cases by averaging the fraction of successful forward checks and the backward check indicator\. By construction,SA\-Passsoft​\(T^,𝒮\)=1⇔SA\-Pass​\(T^,𝒮\)=1\.\\text\{\{SA\-Pass\}$\{\}\_\{\\mathrm\{soft\}\}$ \}\(\\widehat\{T\},\\mathcal\{S\}\)=1\\Leftrightarrow\\text\{\{SA\-Pass\} \}\(\\widehat\{T\},\\mathcal\{S\}\)=1\.

[Figure3](https://arxiv.org/html/2608.29270#S3.F3)summarizes the evaluation procedure\.

## 4ShadowBench

To evaluate full autoformalization systems withSA\-Pass, we constructShadowBench, a Lean 4 benchmark equipped with checker theorems for semantic alignment evaluation\. Its checker construction is LLM\-assisted and compiler\-verified, while the resulting benchmark offers broad mathematical coverage and remains challenging for current systems\.

#### LLM\-assisted checker construction\.

Qwen3\-235B proposes candidate shadow sets and their checker theorems, Lean verifies shadow set completeness, and experts review the results and guide revisions when needed\. The checker construction takes about1010minutes per problem on average, where for85%85\\%of problems the initial LLM\-generated shadow set is already complete \([Section4\.1](https://arxiv.org/html/2608.29270#S4.SS1)\)\.

#### Coverage\.

ShadowBenchcontains 178 problems ranging from postgraduate\- to research\-level across eight mathematical areas and three difficulty levels \([Table1](https://arxiv.org/html/2608.29270#S4.T1)\)\. L1 and L2 contain postgraduate\-level problems, separated by reference Lean length as a proxy for formalization complexity, with L2 containing longer formalizations\. L3 contains research\-level problems\.

AreaL1L2L3Totalgeometry\(Geo\)186024topology\(Top\)169025algebra\(Alg\)194326analysis\(Anl\)1410428algebraic\-geometry\(AG\)216422combinatorics\(Cmb\)86014number\-theory\(NT\)170219probability\(Prob\)191020Total1135213178

Table 1:Number of problems per area and difficulty level inShadowBench\. One topology problem was withdrawn after an error was found in its reference statement\.
#### Difficulty\.

ShadowBenchremains challenging for current systems\. Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent, the strongest system we evaluate underSA\-Pass, achieves a61\.8%61\.8\\%compile rate but scores only18\.3%18\.3\\%onSA\-Passsoftand11\.2%11\.2\\%onSA\-Pass\([Table3](https://arxiv.org/html/2608.29270#S5.T3)\)\.

### 4\.1Benchmark Construction

The curation interface for entering informal statements, reference Lean code, metadata, and checker blocks is shown in Appendix \([Figures8](https://arxiv.org/html/2608.29270#A8.F8),[9](https://arxiv.org/html/2608.29270#A8.F9)and[10](https://arxiv.org/html/2608.29270#A8.F10)\)\. Five mathematicians, spanning graduate students, postdoctoral researchers, and faculty, performed semantic review and guided revisions throughout the construction process\.

#### Informal theorem\.

Annotators first collect source problems from textbooks, lecture notes, and research repositories, summarized in[Table8](https://arxiv.org/html/2608.29270#A1.T8)\. When only a Lean formalization is available, Qwen3\-235B drafts the informal theorem\. We exclude problems whose solutions are dominated by theorem retrieval, since such cases test library search more than full autoformalization\.

#### Reference formalization\.

For each informal theorem, we construct a reference Lean formalization, with Qwen3\-235B providing a draft when only the informal theorem is available\. Annotators edit the code until the theorem type\-checks in Lean, verify that its formal statement matches the informal theorem, and use LeanSearch333[https://leansearch\.net/](https://leansearch.net/)to correct minor errors such as hallucinated theorem names\.

#### Checker theorems\.

Given the reference formalization, Qwen3\-235B proposes a candidate shadow set and its checker theorems \([Figure15](https://arxiv.org/html/2608.29270#A9.F15)\), and Lean verifies the set’s completeness by compiling all forward and backward checkers \([Section3\.2](https://arxiv.org/html/2608.29270#S3.SS2)\)\. The initial draft is complete for85%85\\%of problems\. For the remaining15%15\\%, an expert guides the model to revise or add shadows until all checkers compile\. For77\.1%77\.1\\%of checker proofs,exactalone suffices because the goal follows directly from existing library facts or the statement structure\. Including LLM drafting, checker construction averages about1010minutes per problem\.[Table2](https://arxiv.org/html/2608.29270#S4.T2)summarizes the number of forward and backward checker theorems per problem\.

While each checker is constructed using the reference formalization, valid solver outputs may use different binder styles, declaration names, or field notation\. To reduce false negatives, we diversify the checkers during benchmark construction to cover common differences in binder style and field notation\. At evaluation time, rule\-based rewriting first addresses any remaining declaration\-name mismatches\. If rule\-based rewriting fails, Qwen3\-235B attempts to generate an adapter proof that establishes equivalence between the solver declaration and the corresponding reference declaration, allowing the checker to run in Lean\.

TypeCountMeanMinMaxForward5132\.88113Backward1931\.08112Total7063\.97125

Table 2:Statistics of forward and backward checker theorems inShadowBench, counted over its 178 problems\.

### 4\.2Benchmark Release

We provide the informal theorems and their formalization rules through a hosted portal such as CodaBench,444[https://www\.codabench\.org/](https://www.codabench.org/)while keeping the shadow and checker theorems hidden to prevent direct optimization for the checks\. A version\-pinned evaluator runs the hidden checkers and reports theSA\-PassandSA\-Passsoftscores\.

## 5Experiment

### 5\.1Experimental Setup

#### Evaluation metrics\.

The main results in[Table3](https://arxiv.org/html/2608.29270#S5.T3)use three metrics\.Compile rate[Azerbayev et al\. \(2023\)](https://arxiv.org/html/2608.29270#bib.bib33)is the fraction of outputs whose finaltheoremblock type\-checks in the pinned Lean 4 and Mathlib environment\.555v4\.29\.0SA\-Pass\([Definition5](https://arxiv.org/html/2608.29270#Thmdefinition5)\) is11if the generated theorem type\-checks and all forward and backward checks pass, and00otherwise\.SA\-Passsoft\([Definition6](https://arxiv.org/html/2608.29270#Thmdefinition6)\) averages the forward\-check pass rate and the backward\-check indicator\.

To analyze agreement with expert judgments \([Tables4](https://arxiv.org/html/2608.29270#S5.T4)and[6](https://arxiv.org/html/2608.29270#S6.T6)\), we include three additional metrics\.BLEU\([Azerbayev et al\., 2023](https://arxiv.org/html/2608.29270#bib.bib33);[Papineni et al\., 2002](https://arxiv.org/html/2608.29270#bib.bib30)\)measures lexicalnn\-gram overlap between the generated theorem block and the reference Lean theorem\.BEq\+\([Poiroux et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib1)\)uses Lean tactics to prove both directions of implication between the generated and reference statements\.LLM\-as\-judge\([Guo et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib29)\)uses Gemini Pro 3\.1, Claude Opus 4\.7, and GPT\-5\.4\. We queried each judge three times and took the majority over all nine votes, where the total API cost was approximately $480\.

L1L2L3Average\(n=113\)\(n=52\)\(n=13\)\(n=178\)MethodCompileSA\-PasssoftSA\-PassCompileSA\-PasssoftSA\-PassCompileSA\-PasssoftSA\-PassCompileSA\-PasssoftSA\-PassAgentic methodsClaude Code \(Opus 4\.6\)6\.21\.80\.01\.91\.00\.00\.00\.00\.04\.51\.40\.0\+ Numina55\.816\.88\.836\.517\.311\.515\.40\.00\.047\.215\.79\.0Claude Code \(Opus 4\.8\)24\.84\.92\.713\.56\.73\.87\.70\.00\.020\.25\.12\.8\+ Numina61\.113\.36\.271\.231\.723\.130\.87\.77\.761\.818\.311\.2Claude Code \(Qwen3 235B\)4\.41\.30\.95\.80\.00\.07\.70\.00\.05\.10\.80\.6\+ Numina8\.81\.30\.93\.80\.00\.00\.00\.00\.06\.70\.80\.6Codex \(GPT\-5\.4\)20\.44\.42\.711\.51\.91\.97\.70\.00\.016\.93\.42\.2\+ Numina61\.915\.98\.848\.121\.213\.530\.87\.77\.755\.616\.910\.1Closed\-source LLMsClaude Opus 4\.61\.80\.00\.00\.00\.00\.00\.00\.00\.01\.10\.00\.0Claude Sonnet 4\.60\.90\.00\.00\.00\.00\.00\.00\.00\.00\.60\.00\.0Claude Haiku 4\.50\.90\.40\.00\.00\.00\.00\.00\.00\.00\.60\.30\.0GPT\-5\.41\.80\.40\.05\.80\.00\.07\.70\.00\.03\.40\.30\.0GPT\-5\.4 mini8\.80\.40\.03\.80\.00\.030\.80\.00\.08\.90\.30\.0GPT\-5\.4 nano6\.10\.00\.05\.80\.00\.015\.40\.00\.06\.70\.00\.0Gemini 3\.1 Pro0\.90\.00\.00\.00\.00\.015\.40\.00\.01\.70\.00\.0Gemini 2\.5 Flash0\.90\.40\.00\.00\.00\.00\.00\.00\.00\.60\.30\.0Open\-source LLMsGPT\-OSS\-120B0\.90\.40\.00\.00\.00\.00\.00\.00\.00\.60\.30\.0GPT\-OSS\-20B4\.40\.40\.01\.90\.00\.00\.00\.00\.03\.40\.30\.0DeepSeek R1 05280\.90\.00\.00\.00\.00\.00\.00\.00\.00\.60\.00\.0DeepSeek V3\.20\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.0Qwen3 235B0\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.0Qwen3\-coder0\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.0Llama3\.1 70b0\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.0Llama3\.1 8b0\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.0Lean\-specialized methodsKimina 7B→\\to8B0\.00\.00\.01\.90\.00\.00\.00\.00\.00\.50\.00\.0Goedel 8B→\\to32B0\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.0Goedel 8B→\\to8B0\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.00\.0

Table 3:Per\-difficulty pass rates \(%\) onShadowBench\.*Compile*is the standalone Lean compile rate\.SA\-Passsoftmeasures the fraction of forward and backward checkers that pass\.SA\-Passrequires all forward and backward checkers to pass\.
#### Methods\.

The main experimental results in[Table3](https://arxiv.org/html/2608.29270#S5.T3)cover four method groups\. Foragentic methods, we run Claude Code with Claude Opus 4\.8\([Anthropic, 2026b](https://arxiv.org/html/2608.29270#bib.bib15)\), Claude Opus 4\.6\([Anthropic, 2026a](https://arxiv.org/html/2608.29270#bib.bib16)\), or Qwen3\-235B\([Yang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib27)\), and Codex with GPT\-5\.4\([OpenAI, 2026a](https://arxiv.org/html/2608.29270#bib.bib19)\)\. Each configuration is evaluated with and without Numina\-Lean\-Agent\([Liu et al\., 2026a](https://arxiv.org/html/2608.29270#bib.bib54)\), which provides search and compilation tools during proof construction \([Table10](https://arxiv.org/html/2608.29270#A2.T10)\)\. Forclosed\-source LLMs, we use Claude Haiku 4\.5, Claude Sonnet 4\.6, and Claude Opus 4\.6\([Anthropic, 2025](https://arxiv.org/html/2608.29270#bib.bib18);[Anthropic, 2026c](https://arxiv.org/html/2608.29270#bib.bib17);[Anthropic, 2026a](https://arxiv.org/html/2608.29270#bib.bib16)\), Gemini Flash 2\.5 and Gemini Pro 3\.1\([Google DeepMind, 2025](https://arxiv.org/html/2608.29270#bib.bib22);[Google DeepMind, 2026](https://arxiv.org/html/2608.29270#bib.bib21)\), and GPT\-5\.4 nano, GPT\-5\.4 mini, and GPT\-5\.4\([OpenAI, 2026a](https://arxiv.org/html/2608.29270#bib.bib19);[OpenAI, 2026b](https://arxiv.org/html/2608.29270#bib.bib20)\)\. Foropen\-source LLMs, we run GPT\-OSS\-20B and GPT\-OSS\-120B\([Agarwal et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib23)\), DeepSeek V3\.2 and DeepSeek R1 0528\([DeepSeek\-AI, 2025](https://arxiv.org/html/2608.29270#bib.bib25);[Guo et al\., 2025a](https://arxiv.org/html/2608.29270#bib.bib24)\), qwen3\-coder and Qwen3\-235B\([Yang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib27)\), and Llama 3\.1 8B and 70B\([Grattafiori et al\., 2024](https://arxiv.org/html/2608.29270#bib.bib28)\)\. For theLean\-specialized methods, we use two\-stage formalizer\-to\-prover configurations: Kimina 7B→\\to8B\([Wang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib52);[Numina and Kimi Team, 2025](https://arxiv.org/html/2608.29270#bib.bib53)\), Goedel 8B→\\to8B, and Goedel 8B→\\to32B\([Lin et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib26)\)\. Further model and configuration details are provided in[SectionB\.2](https://arxiv.org/html/2608.29270#A2.SS2)\.

#### Method Configurations\.

Agentic methods use the default configuration of each agent, with prompts shown in[AppendicesI](https://arxiv.org/html/2608.29270#A9.SS0.SSS0.Px2)and[I](https://arxiv.org/html/2608.29270#A9.SS0.SSS0.Px3)\. Closed\-source and open\-source LLMs use zero\-shot prompting withmax\_tokens=8192\{=\}8192, temperature0\.60\.6, andtop\_p=0\.95\{=\}0\.95\. Lean\-specialized methods usemax\_tokens=2048\{=\}2048for the formalizer andmax\_tokens=16384\{=\}16384for the prover, both with temperature0\.60\.6andtop\_p=0\.95\{=\}0\.95\.

### 5\.2Results onShadowBench

[Table3](https://arxiv.org/html/2608.29270#S5.T3)reports compile rate,SA\-Passsoft, andSA\-Passacross all evaluated methods and difficulty levels\.

#### Compilation substantially overestimates semantic alignment onShadowBench\.

The strongest system underSA\-Pass, Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent, reaches a61\.8%61\.8\\%compile rate but only18\.3%18\.3\\%SA\-Passsoftand11\.2%11\.2\\%SA\-Pass\. Thus, even the relaxed score remains43\.543\.5points below compile rate, while the gap to full semantic alignment is50\.650\.6points\. This discrepancy primarily reflects false positives from compile rate, which achieves a precision of only 0\.178 in our expert analysis \([Section6\.1](https://arxiv.org/html/2608.29270#S6.SS1)\), compared with 1\.000 forSA\-Pass\.

#### Numina\-Lean\-Agent improves compilability more than semantic alignment\.

Employing a concurrent agentic method Numina\-Lean\-Agent raises the compile rate of Claude Code \(Opus 4\.8\) from20\.2%20\.2\\%to61\.8%61\.8\\%, a gain of41\.641\.6points\. Over the same comparison,SA\-Passsoftincreases from5\.1%5\.1\\%to18\.3%18\.3\\%andSA\-Passfrom2\.8%2\.8\\%to11\.2%11\.2\\%, gains of13\.213\.2and8\.48\.4points, respectively\. For Codex, the corresponding gains are38\.738\.7points in compile rate,13\.513\.5points inSA\-Passsoft, and7\.97\.9points inSA\-Pass\. The same qualitative pattern holds for the other agentic configurations\. These results indicate that search and compiler feedback are substantially more effective at helping agents produce type\-correct Lean theorem–proof pairs than at ensuring that the generated statements express the intended mathematics\.

MetricPrecisionRecallF1AgreementCompile0\.1781\.0000\.3020\.178BLEU0\.2340\.6740\.3470\.550LLM\-as\-judge0\.2350\.0930\.1330\.785BEq\+0\.4000\.1860\.2540\.806SA\-Passsoft0\.4140\.9530\.5770\.752SA\-Pass1\.0000\.9300\.9640\.988Table 4:Binary agreement of automatic metrics with expert judgment, averaged measurement over all six agentic configurations onShadowBench\. Per\-configuration results are in[AppendixD](https://arxiv.org/html/2608.29270#A4)\. The best value per column is bold, and the second best is underlined\.
#### Semantic alignment onShadowBenchremains largely unsolved\.

Closed\-source LLMs, open\-source LLMs, and Lean\-specialized methods all score0\.0%0\.0\\%onSA\-Pass, and none exceeds0\.3%0\.3\\%onSA\-Passsoft\. Even among agentic methods, the best scores are only11\.2%11\.2\\%onSA\-Passand18\.3%18\.3\\%onSA\-Passsoft\. Performance is particularly limited on L3, where the bestSA\-Passscores7\.7%7\.7\\%\. For comparison,[Section6\.2](https://arxiv.org/html/2608.29270#S6.SS2)finds that compile rate andSA\-Passdiffer by only2\.12\.1points on average and at most7\.87\.8points across the 16 non\-agentic models evaluated on ProofNet\. This contrast suggests that the longer and more compositional targets inShadowBenchexpose semantic failures that are less visible on shorter, mostly single\-conclusion formalizations\.

## 6Analysis

### 6\.1Agreement with Expert Judgment

The large gap between compile rate andSA\-Passin[Table3](https://arxiv.org/html/2608.29270#S5.T3)admits two possible explanations: compilation may accept semantically misaligned formalizations, orSA\-Passmay reject valid alternative formulations\. We distinguish these explanations by comparing each automatic metric with expert judgments\.

We collect expert judgments for compile\-passed generations onShadowBench, where compilation and semantic alignment can disagree\. Two mathematics experts independently assess whether each generated theorem is semantically aligned with the source problem and resolve disagreements through discussion\. We analyze six configurations with sufficient compile\-passed outputs: Claude Code \(Opus 4\.6\), Claude Code \(Qwen3\-235B\), and Codex \(GPT\-5\.4\), each with and without Numina\-Lean\-Agent\. Against the resulting binary judgments, we measure precision, recall, F1, and agreement for compile rate, BLEU, BEq\+, LLM\-as\-judge,SA\-Passsoft, andSA\-Pass\. For the non\-binary metrics, we use thresholds of00forSA\-Passsoftand0\.10\.1for BLEU, as determined in[AppendixE](https://arxiv.org/html/2608.29270#A5)\. Agreement measures the proportion of an automatic metric’s binary decisions that match expert judgments\.

[Table4](https://arxiv.org/html/2608.29270#S5.T4)shows thatSA\-Passachieves the highest F1 \(0\.9640\.964\) and agreement \(0\.9880\.988\)\. Compile rate treats compilation success as semantically aligned, yielding1\.0001\.000recall but only0\.1780\.178precision due to false positives\. BEq\+ applies Lean’s built\-in equivalence check, achieving higher precision than Compile rate \(0\.4000\.400vs\.0\.1780\.178\) but substantially lower recall \(0\.1860\.186\)\. Its precision remains limited because the check covers only the final theorem statement, ignoring the auxiliary declarations required for a complete formalization of the informal theorem\. In contrast,SA\-Passachieves1\.0001\.000precision and0\.9300\.930recall\. Its few false negatives stem from namespace mismatches that the LLM fallback fails to resolve \([AppendixD](https://arxiv.org/html/2608.29270#A4.SS0.SSS0.Px1)\)\.

Taken together, these results indicate that the large gap between Compile rate andSA\-Passin[Table3](https://arxiv.org/html/2608.29270#S5.T3)primarily reflects false positives from compilation rather than false negatives fromSA\-Pass\.

ModelCompileSA\-PasssoftSA\-PassClosed\-source LLMsClaude Opus 4\.696\.592\.990\.6Claude Sonnet 4\.685\.985\.185\.1Claude Haiku 4\.596\.595\.395\.3GPT 5\.494\.993\.793\.7GPT 5\.4 Mini95\.394\.194\.1GPT 5\.4 Nano77\.676\.576\.5Gemini 3\.1 Pro35\.734\.934\.9Gemini 2\.5 Flash82\.476\.176\.1Open\-source LLMsGPT\-OSS\-120B60\.860\.860\.8GPT\-OSS\-20B60\.460\.460\.4DeepSeek R1 052825\.525\.525\.5DeepSeek V3\.264\.364\.364\.3Qwen3 235B91\.091\.091\.0Qwen3\-coder89\.889\.889\.8Llama 3\.1 70B32\.925\.125\.1Llama 3\.1 8B35\.328\.228\.2Table 5:Non\-agentic pass rates \(%\) on the Lean 4 version of ProofNet, using automatically generated shadow sets\.
### 6\.2SA\-Passon ProofNet

MetricPrecisionRecallF1AgreementCompile0\.8001\.0000\.8890\.800BLEU0\.8001\.0000\.8890\.800LLM\-as\-judge0\.8650\.8890\.8770\.800BEq\+0\.8870\.6530\.7520\.656SA\-Passsoft1\.0001\.0001\.0001\.000SA\-Pass1\.0001\.0001\.0001\.000Table 6:Binary agreement of automatic metrics with expert judgment for Llama 3\.1 8B outputs on ProofNet\. The best value per column is bold, and the second best is underlined\.To test whetherSA\-Passtransfers beyondShadowBench, we apply it to the Lean 4 version of ProofNet\([Azerbayev et al\., 2023](https://arxiv.org/html/2608.29270#bib.bib33)\), an undergraduate\-level benchmark with shorter formalizations\.666We exclude the 31% of problems with known faulty reference formalizations\([Poiroux et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib1)\)\.We construct a complete shadow set and checker theorems for each problem using the same LLM\-assisted pipeline as forShadowBench\([Section4\.1](https://arxiv.org/html/2608.29270#S4.SS1)\)\. All initial drafts pass the Lean completeness checks, so no expert revision is required\.

We first compare the resulting metrics with expert judgments on Llama 3\.1 8B outputs, which include both positive and negative expert labels\. As shown in[Table6](https://arxiv.org/html/2608.29270#S6.T6),SA\-PassandSA\-Passsoftboth match every expert judgment, while compile rate reaches an F1 of0\.8890\.889\. This result provides evidence that the shadow checks remain reliable when applied to ProofNet\.

[Table5](https://arxiv.org/html/2608.29270#S6.T5)shows that compile rate andSA\-Passare much closer on ProofNet than onShadowBench\. Across the 16 models, the gap is2\.12\.1points on average and at most7\.87\.8points\. The smaller gap is consistent with the shorter and less compositional targets in ProofNet\. Reference statements inShadowBenchare about1\.6×1\.6\\timeslonger by line count, and its reference solutions contain4\.54\.5auxiliary declarations per problem on average, compared with none in ProofNet \([Table9](https://arxiv.org/html/2608.29270#A1.T9)\)\. Most ProofNet targets also have a single conclusion, so their shadow sets typically require only one or two short checks\. Compile rate is therefore a closer proxy for semantic alignment on ProofNet, whereasShadowBenchexposes failures that are less visible in shorter formalizations\.

L1 \(n=113\)L2 \(n=52\)L3 \(n=13\)Average \(n=178\)MethodFwdFwdallBwdSA\-PassFwdFwdallBwdSA\-PassFwdFwdallBwdSA\-PassFwdFwdallBwdSA\-PassClaude Code \(Opus 4\.6\)0\.90\.92\.70\.01\.91\.90\.00\.00\.00\.00\.00\.01\.11\.11\.70\.0\+ Numina15\.015\.018\.68\.817\.317\.317\.311\.50\.00\.00\.00\.014\.614\.616\.99\.0Claude Code \(Opus 4\.8\)4\.44\.45\.32\.75\.85\.87\.73\.80\.00\.00\.00\.04\.54\.55\.62\.8\+ Numina9\.79\.716\.86\.225\.025\.038\.523\.17\.77\.77\.77\.714\.014\.022\.511\.2Claude Code \(Qwen3 235B\)0\.90\.91\.80\.90\.00\.00\.00\.00\.00\.00\.00\.00\.60\.61\.10\.6\+ Numina0\.90\.91\.80\.90\.00\.00\.00\.00\.00\.00\.00\.00\.60\.61\.10\.6Codex \(GPT\-5\.4\)3\.53\.55\.32\.71\.91\.91\.91\.90\.00\.00\.00\.02\.82\.83\.92\.2\+ Numina17\.717\.714\.28\.819\.219\.223\.113\.57\.77\.77\.77\.717\.417\.416\.310\.1

Table 7:Per\-difficulty checker metrics \(%\) for agentic systems onShadowBench\. Fwd and Bwd average the per\-problem fractions of passed forward and backward checkers, Fwdallis the fraction of problems passing every forward checker\.
### 6\.3Forward and Backward Checker Analysis

The forward and backward checks used bySA\-Passdetect different forms of semantic mismatch\. A successful forward check certifies that the generated statement implies a required consequence of the intended theorem, while a successful backward check certifies that the intended theorem implies the generated statement\. Passing the backward checks but not all forward checks can arise from omitted conclusions or added assumptions \([SectionJ\.4](https://arxiv.org/html/2608.29270#A10.SS4)\)\. Conversely, passing all forward checks but failing the backward checks can arise from added conclusions or omitted assumptions\. When both directions fail, neither implication is certified \([SectionJ\.5](https://arxiv.org/html/2608.29270#A10.SS5)\)\.

[Table7](https://arxiv.org/html/2608.29270#S6.T7)shows that the two implication directions can differ substantially even whenSA\-Passis low\. Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent reaches aSA\-Passscore of11\.2%11\.2\\%, with a14\.0%14\.0\\%all forward pass rate but22\.5%22\.5\\%average backward pass rate\. Among its 110 compile\-passed outputs, 20 pass both directions, 20 pass only the backward direction, 5 pass only the forward direction, and 65 pass neither\.

## 7Conclusion

We introducedSA\-Pass, an automatic metric that evaluates semantic alignment between generated formal statements and informal theorem statements\. For each problem,SA\-Passuses a set of auxiliary formal statements, called shadows, whose conjunction is equivalent to the intended theorem statement, and checks in Lean whether the generated statement implies each shadow and is implied by their conjunction\. We instantiatedSA\-PassinShadowBench, a Lean 4 full autoformalization benchmark of 178 postgraduate\- to research\-level problems spanning eight mathematical areas\. OnShadowBench, Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent reaches61\.8%61\.8\\%compile rate,18\.3%18\.3\\%SA\-Passsoft, and11\.2%11\.2\\%SA\-Pass, showing that compile success alone can overstate semantic alignment\. Across six agentic configurations,SA\-Passachieves98\.8%98\.8\\%binary agreement with expert judgments\.

## Limitations

ShadowBenchcovers 178 postgraduate\- to research\-level problems across eight mathematical areas, and future versions can extend this coverage to more domains and proof styles\.SA\-Passrequires one\-time construction of shadow statements and checker proofs for each benchmark problem\.

## Potential Risks

The main risk is benchmark leakage\. If checker artifacts are exposed, systems can optimize for the checks rather than the informal theorem\. To reduce this risk, public problem inputs are separated from the checking artifacts used for evaluation\. We give the full release and evaluation protocol in[Section4\.2](https://arxiv.org/html/2608.29270#S4.SS2)\.

## Acknowledgments

This work was supported by the National Research Foundation of Korea \(NRF\) grant funded by the Korea government \(MSIT\) \(No\. RS\-2025\-00520280\), Institute of Information & communications Technology Planning & Evaluation \(IITP\) grant funded by the Korea government\(MSIT\) \[NO\.RS\-2021\-II211343, Artificial Intelligence Graduate School Program \(Seoul National University\)\], Electronics and Telecommunications Research Institute \(ETRI\) grant funded by ICT R&D program of MSIT/IITP \(2022\-0\-00995, Automated reliable source code generation from natural language descriptions\)\. We thank Soonho Kong for supporting our experiments with Claude and Claude Code on Amazon Web Services\.

## References

- 1000\+ Theorems contributors1000\+ Theorems: euler’s quadrilateral theorem\.Note:[https://1000\-plus\.github\.io/all](https://1000-plus.github.io/all)Entry “Euler’s quadrilateral theorem”; accessed 2026\-05\-26Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.9.2.1.1)\.
- Agarwalet al\.\(2025\)S\. Agarwal, L\. Ahmad, J\. Ai, S\. Altman, A\. Applebaum, E\. Arbus, R\. K\. Arora, Y\. Bai, B\. Baker, H\. Bao,et al\.Gpt\-oss\-120b & gpt\-oss\-20b model card\.arXiv preprint arXiv:2508\.10925\.External Links:[Link](https://arxiv.org/pdf/2508.10925)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.5.2),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Agrawalet al\.\(2004\)M\. Agrawal, N\. Kayal, and N\. SaxenaPRIMES is in p\.Annals of mathematics,pp\. 781–793\.Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.10.2.1.1)\.
- Aigner and Ziegler \(1999\)M\. Aigner and G\. M\. ZieglerProofs from the book\.Berlin\. Germany1\(2\),pp\. 7\.Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.11.2.1.1)\.
- Ammanamanchiet al\.\(2026\)P\. S\. Ammanamanchi, S\. Bhat, and S\. BidermanFaults in our formal benchmarking: dataset defects and evaluation failures in Lean theorem proving\.InForty\-third International Conference on Machine Learning,External Links:[Link](https://openreview.net/forum?id=bHYAWawd4A)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p2.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px1.p1.1)\.
- Anthropic \(2025\)AnthropicSystem Card: Claude Haiku 4\.5\.External Links:[Link](https://assets.anthropic.com/m/99128ddd009bdcb/original/Claude-Haiku-4-5-System-Card.pdf)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.2.2),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Anthropic \(2026a\)AnthropicSystem Card: Claude Opus 4\.6\.Claude Opus 4\.6 Model Card\.External Links:[Link](https://www-cdn.anthropic.com/14e4fb01875d2a69f646fa5e574dea2b1c0ff7b5.pdf)Cited by:[Table 10](https://arxiv.org/html/2608.29270#A2.T10.2.1.2.2),[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.2.2),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Anthropic \(2026b\)AnthropicSystem Card: Claude Opus 4\.8\.Claude Opus 4\.8 Model Card\.External Links:[Link](https://www-cdn.anthropic.com/0b4915911bb0d19eca5b5ee635c80fef830a37ea.pdf)Cited by:[Table 10](https://arxiv.org/html/2608.29270#A2.T10.2.1.3.2),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Anthropic \(2026c\)AnthropicSystem Card: Claude Sonnet 4\.6\.Claude Sonnet 4\.6 Model Card\.External Links:[Link](https://www-cdn.anthropic.com/78073f739564e986ff3e28522761a7a0b4484f84.pdf)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.2.2),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Azerbayevet al\.\(2023\)Z\. Azerbayev, B\. Piotrowski, H\. Schoelkopf, E\. W\. Ayers, D\. Radev, and J\. AvigadProofNet: autoformalizing and formally proving undergraduate\-level mathematics\.arXiv preprint arXiv:2302\.12433\.External Links:[Link](https://arxiv.org/abs/2302.12433)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p5.1),[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px1.p1.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px2.p1.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px1.p1.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px1.p2.1),[§6\.2](https://arxiv.org/html/2608.29270#S6.SS2.p1.1)\.
- Boyd and Vandenberghe \(2004\)S\. Boyd and L\. VandenbergheConvex optimization\.Cambridge university press\.Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.4.2.1.1)\.
- Chenet al\.\(2026\)G\. Chen, J\. Wu, X\. Chen, W\. X\. Zhao, R\. Song, C\. Li, K\. Fan, D\. Liu, and M\. LiaoReForm: reflective autoformalization with prospective bounded sequence optimization\.InInternational Conference on Learning Representations,Note:PosterExternal Links:[Link](https://openreview.net/forum?id=KfxRzCmRSX)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Chenet al\.\(2021\)M\. Chen, J\. Tworek, H\. Jun, Q\. Yuan, H\. P\. d\. O\. Pinto, J\. Kaplan, H\. Edwards, Y\. Burda, N\. Joseph, G\. Brockman, A\. Ray, R\. Puri, G\. Krueger, M\. Petrov, H\. Khlaaf, G\. Sastry, P\. Mishkin, B\. Chan, S\. Gray, N\. Ryder, M\. Pavlov, A\. Power, L\. Kaiser, M\. Bavarian, C\. Winter, P\. Tillet, F\. P\. Such, D\. Cummings, M\. Plappert, F\. Chantzis, E\. Barnes, A\. Herbert\-Voss, W\. H\. Guss, A\. Nichol, A\. Paino, N\. Tezak, J\. Tang, I\. Babuschkin, S\. Balaji, S\. Jain, W\. Saunders, C\. Hesse, A\. N\. Carr, J\. Leike, J\. Achiam, V\. Misra, E\. Morikawa, A\. Radford, M\. Knight, M\. Brundage, M\. Murati, K\. Mayer, P\. Welinder, B\. McGrew, D\. Amodei, S\. McCandlish, I\. Sutskever, and W\. ZarembaEvaluating large language models trained on code\.arXiv preprint arXiv:2107\.03374\.External Links:[Link](https://arxiv.org/abs/2107.03374)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p3.1)\.
- Coxet al\.\(2008\)D\.A\. Cox, J\. Little, and D\. O’SheaIdeals, varieties, and algorithms: an introduction to computational algebraic geometry and commutative algebra\.Undergraduate Texts in Mathematics,Springer New York\.External Links:ISBN 9780387514857,LCCN 89021569,[Link](https://books.google.co.kr/books?id=qs9fAQAACAAJ)Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.6.2.1.1)\.
- DeepSeek\-AI \(2025\)DeepSeek\-AIDeepSeek\-V3\.2: pushing the frontier of open large language models\.arXiv preprint arXiv:2512\.02556\.External Links:[Link](https://arxiv.org/abs/2512.02556)Cited by:[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Dieudonne and Grothendieck \(1971\)J\. A\. Dieudonne and A\. GrothendieckÉléments de géométrie algébrique\.Vol\.166,Springer Berlin Heidelberg New York\.Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.5.2.1.1)\.
- Fanget al\.\(2025\)Y\. Fang, S\. Huang, X\. Yu, H\. Huang, Z\. Zhang, W\. Deng, F\. Wei, F\. Sun, Q\. Zhang, and Z\. JinNL2Lean: translating natural language into Lean 4 through multi\-aspect reinforcement learning\.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\. 31148–31158\.External Links:[Document](https://dx.doi.org/10.18653/v1/2025.emnlp-main.1586),[Link](https://aclanthology.org/2025.emnlp-main.1586/)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p2.1),[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px3.p1.1)\.
- Gaoet al\.\(2025\)G\. Gao, Y\. Wang, J\. Jiang, Q\. Gao, Z\. Qin, T\. Xu, and B\. DongHerald: a natural language annotated Lean 4 dataset\.InInternational Conference on Learning Representations,Note:PosterExternal Links:[Link](https://openreview.net/forum?id=Se6MgCtRhz)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Google DeepMind \(2025\)Google DeepMindGemini 2\.5 Flash Model Card\.External Links:[Link](https://storage.googleapis.com/deepmind-media/Model-Cards/Gemini-2-5-Flash-Model-Card.pdf)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.3.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Google DeepMind \(2026\)Google DeepMindGemini 3\.1 Pro Model Card\.Gemini 3\.1 Pro Model Card\.External Links:[Link](https://storage.googleapis.com/deepmind-media/Model-Cards/Gemini-3-1-Pro-Model-Card.pdf)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.3.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Grattafioriet al\.\(2024\)A\. Grattafiori, A\. Dubey, A\. Jauhri, A\. Pandey, A\. Kadian, A\. Al\-Dahle, A\. Letman, A\. Mathur, A\. Schelten, A\. Vaughan,et al\.The llama 3 herd of models\.arXiv preprint arXiv:2407\.21783\.Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.8.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Guoet al\.\(2025a\)D\. Guo, D\. Yang, H\. Zhang, J\. Song, P\. Wang, Q\. Zhu, R\. Xu, R\. Zhang, S\. Ma, X\. Bi,et al\.DeepSeek\-R1 incentivizes reasoning in LLMs through reinforcement learning\.Nature645,pp\. 633–638\.External Links:[Document](https://dx.doi.org/10.1038/s41586-025-09422-z),[Link](https://www.nature.com/articles/s41586-025-09422-z)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.6.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Guoet al\.\(2025b\)Q\. Guo, J\. Wang, J\. Zhang, D\. Kong, X\. Huang, X\. Xi, W\. Wang, J\. Wang, X\. Cai, S\. Zhang, and W\. YeAutoformalizer with tool feedback\.arXiv preprint arXiv:2510\.06857\.Cited by:[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px2.p1.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px1.p2.1)\.
- Janaet al\.\(2026\)P\. Jana, K\. Kale, A\. E\. Tanriverdi, C\. Song, S\. Vishwanath, and V\. GaneshProofBridge: auto\-formalization of natural language proofs in Lean via joint embeddings\.InInternational Conference on Learning Representations,Note:PosterExternal Links:[Link](https://openreview.net/forum?id=U2jxHXuOX9)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Kimet al\.\(2026\)J\. Kim, H\. Han, and S\. HwangBenchmarking testing in automated theorem proving\.InProceedings of the 64th Annual Meeting of the Association for Computational Linguistics \(Volume 6: Industry Track\),San Diego, California, USA,pp\. 2241–2260\.External Links:[Document](https://dx.doi.org/10.18653/v1/2026.acl-industry.150),[Link](https://aclanthology.org/2026.acl-industry.150/)Cited by:[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px4.p1.1)\.
- Kwonet al\.\(2023\)W\. Kwon, Z\. Li, S\. Zhuang, Y\. Sheng, L\. Zheng, C\. H\. Yu, J\. E\. Gonzalez, H\. Zhang, and I\. StoicaEfficient memory management for large language model serving with PagedAttention\.InProceedings of the ACM SIGOPS 29th Symposium on Operating Systems Principles,Cited by:[§B\.1](https://arxiv.org/html/2608.29270#A2.SS1.p1.1)\.
- Lee \(2003\)J\. M\. LeeSmooth manifolds\.InIntroduction to smooth manifolds,pp\. 1–29\.Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.7.2.1.1)\.
- Linet al\.\(2025a\)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\.InConference on Language Modeling,External Links:[Link](https://openreview.net/forum?id=x2y9i2HDjD)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Linet al\.\(2025b\)Y\. Lin, S\. Tang, B\. Lyu, Z\. Yang, J\. Chung, H\. Zhao, L\. Jiang, Y\. Geng, J\. Ge, J\. Sun, J\. Wu, J\. Gesi, X\. Lu, D\. Acuna, K\. Yang, H\. Lin, Y\. Choi, D\. Chen, S\. Arora, and C\. JinGoedel\-Prover\-V2: scaling formal theorem proving with scaffolded data synthesis and self\-correction\.arXiv preprint arXiv:2508\.03613\.External Links:[Link](https://arxiv.org/pdf/2508.03613)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.10.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Liuet al\.\(2026a\)J\. Liu, Z\. Zhou, Z\. Zhu, M\. Dos Santos, W\. He, J\. Liu, R\. Wang, Y\. Xie, J\. Zhao, Q\. Wang, L\. Zhi, J\. Li, and W\. LiNumina\-Lean\-Agent: an open and general agentic reasoning system for formal mathematics\.arXiv preprint arXiv:2601\.14027\.External Links:[Link](https://arxiv.org/abs/2601.14027)Cited by:[§B\.1](https://arxiv.org/html/2608.29270#A2.SS1.p1.1),[§1](https://arxiv.org/html/2608.29270#S1.p6.1),[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Liuet al\.\(2025a\)Q\. Liu, X\. Zheng, X\. Lu, Q\. Cao, and J\. YanRethinking and improving autoformalization: towards a faithful metric and a dependency retrieval\-based approach\.InInternational Conference on Learning Representations,Note:SpotlightExternal Links:[Link](https://openreview.net/forum?id=hUb2At2DsQ)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p6.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px1.p1.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px2.p1.1)\.
- Liuet al\.\(2025b\)X\. Liu, K\. Bao, J\. Zhang, Y\. Liu, Y\. Chen, Y\. Liu, Y\. Jiao, and T\. LuoATLAS: autoformalizing theorems through lifting, augmentation, and synthesis of data\.InAdvances in Neural Information Processing Systems,External Links:[Link](https://openreview.net/forum?id=MlJyAvQaxp)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Liuet al\.\(2026b\)X\. Liu, T\. Zhu, Z\. Dong, Y\. Liu, Q\. Guo, Z\. Liu, Y\. Chen, and T\. LuoASSESS: a semantic and structural evaluation framework for statement similarity\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=avwNGWtiHF)Cited by:[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px2.p1.1)\.
- Luet al\.\(2025a\)J\. Lu, Y\. Wan, Y\. Huang, J\. Xiong, Z\. Liu, and Z\. GuoFormalAlign: automated alignment evaluation for autoformalization\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=B5RrIFMqbe)Cited by:[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px2.p1.1)\.
- Luet al\.\(2024\)J\. Lu, Y\. Wan, Z\. Liu, Y\. Huang, J\. Xiong, C\. Liu, J\. Shen, H\. Jin, J\. Zhang, H\. Wang, Z\. Yang, J\. Tang, and Z\. GuoProcess\-driven autoformalization in Lean 4\.arXiv preprint arXiv:2406\.01940\.External Links:[Link](https://arxiv.org/abs/2406.01940)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Luet al\.\(2025b\)W\. Lu, L\. Du, S\. Li, K\. Weng, H\. Sun, H\. Liu, M\. Yu, T\. Zhang, and G\. YuAutomated formalization via conceptual retrieval\-augmented LLMs\.arXiv preprint arXiv:2508\.06931\.External Links:[Link](https://arxiv.org/abs/2508.06931)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Murphyet al\.\(2024\)L\. Murphy, K\. Yang, J\. Sun, Z\. Li, A\. Anandkumar, and X\. SiAutoformalizing Euclidean geometry\.InProceedings of the 41st International Conference on Machine Learning,Vol\.235,pp\. 36847–36893\.External Links:[Link](https://proceedings.mlr.press/v235/murphy24a.html)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Numina and Kimi Team \(2025\)Numina and Kimi TeamKimina\-Prover: applying test\-time RL search on large formal reasoning models\.External Links:[Link](https://huggingface.co/blog/AI-MO/kimina-prover)Cited by:[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- OpenAI \(2026a\)OpenAIGPT\-5\.4 Thinking System Card\.External Links:[Link](https://deploymentsafety.openai.com/gpt-5-4-thinking/gpt-5-4-thinking.pdf)Cited by:[Table 10](https://arxiv.org/html/2608.29270#A2.T10.2.1.5.2),[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.4.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- OpenAI \(2026b\)OpenAIIntroducing GPT\-5\.4 mini and nano\.External Links:[Link](https://openai.com/index/introducing-gpt-5-4-mini-and-nano/)Cited by:[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.p1.1)\.
- Ospanovet al\.\(2025\)A\. Ospanov, F\. Farnia, and R\. YousefzadehminiF2F\-Lean revisited: reviewing limitations and charting a path forward\.InAdvances in Neural Information Processing Systems,Note:PosterExternal Links:[Link](https://openreview.net/forum?id=KtaHv0YUyh)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p2.1)\.
- Papineniet al\.\(2002\)K\. Papineni, S\. Roukos, T\. Ward, and W\. ZhuBLEU: a method for automatic evaluation of machine translation\.InProceedings of the 40th Annual Meeting of the Association for Computational Linguistics,pp\. 311–318\.External Links:[Document](https://dx.doi.org/10.3115/1073083.1073135)Cited by:[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px2.p1.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px1.p2.1)\.
- Poirouxet al\.\(2025a\)A\. Poiroux, A\. Bosselut, and V\. KunčakRLMEval: evaluating research\-level neural theorem proving\.InFindings of the Association for Computational Linguistics: EMNLP 2025,C\. Christodoulopoulos, T\. Chakraborty, C\. Rose, and V\. Peng \(Eds\.\),Suzhou, China,pp\. 10946–10957\.External Links:[Document](https://dx.doi.org/10.18653/v1/2025.findings-emnlp.581),[Link](https://aclanthology.org/2025.findings-emnlp.581/)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Poirouxet al\.\(2025b\)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:[§1](https://arxiv.org/html/2608.29270#S1.p6.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px2.p1.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px1.p2.1),[footnote 6](https://arxiv.org/html/2608.29270#footnote6)\.
- Shapiro \(2024\)J\. ShapiroFunctional analysis: princeton university mat520 lecture notes\.Princeton University\.Note:[https://web\.math\.princeton\.edu/~js129/PDFs/teaching/MAT520\_fall\_2023/MAT520\_Lecture\_Notes\.pdf](https://web.math.princeton.edu/~js129/PDFs/teaching/MAT520_fall_2023/MAT520_Lecture_Notes.pdf)Created August 18, 2023; last typeset September 5, 2024; accessed May 26, 2026Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.2.2.1.1)\.
- Stacks project authors \(2026\)T\. Stacks project authorsThe stacks project\.Note:[https://stacks\.math\.columbia\.edu](https://stacks.math.columbia.edu/)Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.13.2.1.1)\.
- Stein and Shakarchi \(2009\)E\. M\. Stein and R\. ShakarchiReal analysis: measure theory, integration, and hilbert spaces\.Princeton University Press\.Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.12.2.1.1)\.
- The mathlib Community \(2020\)The mathlib CommunityThe Lean Mathematical Library\.InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,CPP 2020,New Orleans, LA, USA\.External Links:[Document](https://dx.doi.org/10.1145/3372885.3373824),[Link](https://doi.org/10.1145/3372885.3373824)Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.8.2.1.1)\.
- Wanget al\.\(2025\)H\. Wang, M\. Unsal, X\. Lin, M\. Baksys, J\. Liu, M\. Dos Santos, F\. Sung, M\. Vinyes, Z\. Ying, Z\. Zhu, J\. Lu, H\. de Saxcé, B\. Bailey, C\. Song, C\. Xiao, D\. Zhang, E\. Zhang, F\. Pu, H\. Zhu, J\. Liu, J\. Bayer, J\. Michel, L\. Yu, L\. Dreyfus\-Schmidt, L\. Tunstall, L\. Pagani, M\. Machado, P\. Bourigault, R\. Wang, S\. Polu, T\. Barroyer, W\. Li, Y\. Niu, Y\. Fleureau, Y\. Hu, Z\. Yu, Z\. Wang, Z\. Yang, Z\. Liu, and J\. LiKimina\-Prover preview: towards large formal reasoning models with reinforcement learning\.arXiv preprint arXiv:2504\.11354\.External Links:[Link](https://arxiv.org/abs/2504.11354)Cited by:[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.9.2),[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.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\.InAdvances in Neural Information Processing Systems,External Links:[Link](https://arxiv.org/abs/2205.12615)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p2.1),[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px3.p1.1)\.
- Wunsch \(2005\)A\. D\. WunschComplex variables with applications\.Pearson Education India\.Cited by:[Table 8](https://arxiv.org/html/2608.29270#A1.T8.2.3.2.1.1)\.
- Xieet al\.\(2025\)J\. Xie, C\. Liu, Y\. Yuan, S\. Li, Z\. Xiao, and M\. ZhangFMC: formalization of natural language mathematical competition problems\.In2nd AI for Math Workshop at ICML 2025,External Links:[Link](https://icml.cc/virtual/2025/52460)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Xinet al\.\(2024\)H\. Xin, D\. Guo, Z\. Shao, Z\. Z\. Ren, Q\. Zhu, B\. Liu, C\. Ruan, W\. Li, and X\. LiangDeepSeek\-Prover: advancing theorem proving in LLMs through large\-scale synthetic data\.arXiv preprint arXiv:2405\.14333\.External Links:[Link](https://arxiv.org/abs/2405.14333)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Yanget al\.\(2025\)A\. Yang, A\. Li, B\. Yang, B\. Zhang, B\. Hui, B\. Zheng, B\. Yu, C\. Gao, C\. Huang, C\. Lv, C\. Zheng, D\. Liu, F\. Zhou, F\. Huang, F\. Hu, H\. Ge, H\. Wei, H\. Lin, J\. Tang, J\. Yang, J\. Tu, J\. Zhang, J\. Yang, J\. Yang, J\. Zhou, J\. Zhou, J\. Lin, K\. Dang, K\. Bao, K\. Yang, L\. Yu, L\. Deng, M\. Li, M\. Xue, M\. Li, P\. Zhang, P\. Wang, Q\. Zhu, R\. Men, R\. Gao, S\. Liu, S\. Luo, T\. Li, T\. Tang, W\. Yin, X\. Ren, X\. Wang, X\. Zhang, X\. Ren, Y\. Fan, Y\. Su, Y\. Zhang, Y\. Zhang, Y\. Wan, Y\. Liu, Z\. Wang, Z\. Cui, Z\. Zhang, Z\. Zhou, and Z\. QiuQwen3 technical report\.arXiv preprint arXiv:2505\.09388\.Cited by:[Table 10](https://arxiv.org/html/2608.29270#A2.T10.2.1.4.2),[Table 11](https://arxiv.org/html/2608.29270#A2.T11.2.1.7.1),[§5\.1](https://arxiv.org/html/2608.29270#S5.SS1.SSS0.Px2.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\.InAdvances in Neural Information Processing Systems,External Links:[Link](https://openreview.net/forum?id=g7OX2sOJtn)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.
- Yinget al\.\(2024\)H\. Ying, Z\. Wu, Y\. Geng, J\. Wang, D\. Lin, and K\. ChenLean Workbook: a large\-scale Lean problem set formalized from natural language math problems\.InAdvances in Neural Information Processing Systems,Note:Datasets and Benchmarks Track PosterExternal Links:[Link](https://openreview.net/forum?id=Vcw3vzjHDb)Cited by:[§1](https://arxiv.org/html/2608.29270#S1.p2.1),[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1),[§2\.2](https://arxiv.org/html/2608.29270#S2.SS2.SSS0.Px3.p1.1)\.
- Zhenget al\.\(2022\)K\. Zheng, J\. M\. Han, and S\. PoluminiF2F: a cross\-system benchmark for formal Olympiad\-level mathematics\.InInternational Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=9ZPegFuFTFv)Cited by:[§2\.1](https://arxiv.org/html/2608.29270#S2.SS1.p1.1)\.

## Appendix ADataset Details

SourceReferenceInformalFormalAnalysis problem\([Shapiro, 2024](https://arxiv.org/html/2608.29270#bib.bib4)\)OXComplex Variables with Applications\([Wunsch, 2005](https://arxiv.org/html/2608.29270#bib.bib11)\)OXConvex Optimization\([Boyd and Vandenberghe, 2004](https://arxiv.org/html/2608.29270#bib.bib5)\)OXElements de geometrie algebrique \(EGA\)\([Dieudonne and Grothendieck, 1971](https://arxiv.org/html/2608.29270#bib.bib7)\)OXIdeals, Varieties, and Algorithms \(4th ed\.\)\([Cox et al\., 2008](https://arxiv.org/html/2608.29270#bib.bib6)\)OXIntroduction to Smooth Manifolds\([Lee, 2003](https://arxiv.org/html/2608.29270#bib.bib8)\)OXMathlib 4\([The mathlib Community, 2020](https://arxiv.org/html/2608.29270#bib.bib3)\)XOMissing theorems from Wiedijk 1000\+\([1000\+ Theorems contributors, 2026](https://arxiv.org/html/2608.29270#bib.bib14)\)OXPRIMES is in P\([Agrawal et al\., 2004](https://arxiv.org/html/2608.29270#bib.bib12)\)OXProofs from THE BOOK\([Aigner and Ziegler, 1999](https://arxiv.org/html/2608.29270#bib.bib13)\)OXReal Analysis: Measure Theory, Integration, and Hilbert Spaces\([Stein and Shakarchi, 2009](https://arxiv.org/html/2608.29270#bib.bib10)\)OXThe Stacks Project\([Stacks project authors, 2026](https://arxiv.org/html/2608.29270#bib.bib9)\)△\\triangle△\\triangleTable 8:List of reference sources used to constructShadowBench\.*Informal*and*Formal*mark the statement type available before annotation\. A triangle denotes mixed availability across problems\.DatasetShadowBenchProofNetnn178371TargetstatementLines5\.13\.2Chars226149ReferenceproofLines71\.63\.4Chars3242157Aux\. decl\.4\.50\.0Table 9:Statistics of the reference statement and proof for bothShadowBenchand ProofNet \(Lean 4\)\.### A\.1Problem Sources

[Table8](https://arxiv.org/html/2608.29270#A1.T8)lists the sources used to constructShadowBench\. Annotators collect problems from textbooks, lecture notes, research papers, and Lean 4 library material\. The Informal and Formal columns mark the statement type available in each source before annotation\. When a source provides only one side, Qwen3\-235B drafts the other, as described in[Section4\.1](https://arxiv.org/html/2608.29270#S4.SS1)\.

### A\.2Dataset Statistics

[Table9](https://arxiv.org/html/2608.29270#A1.T9)compares reference Lean statistics ofShadowBenchwith the Lean 4 version of ProofNet\. Target statements inShadowBenchare about1\.6×1\.6\\timeslonger by line count than those in ProofNet\. The larger difference lies in the reference proofs\. A reference proof inShadowBenchaverages7272lines and4\.54\.5auxiliary declarations, while ProofNet averages about3\.43\.4lines and none of auxiliary declarations\.[Table2](https://arxiv.org/html/2608.29270#S4.T2)reports the number of checker theorems per problem\.

## Appendix BExperiment Details

### B\.1Generation Setup

Closed\-source models and general\-purpose open\-source models are accessed through OpenRouter\. Lean\-specialized models are self\-hosted with vLLM[Kwon et al\. \(2023\)](https://arxiv.org/html/2608.29270#bib.bib2)\. These models are executed on two NVIDIA Titan RTX \(24GB\) for model sizes up to 8B, on two NVIDIA RTX 6000 PRO Ada Generation \(48GB\) for the 32B model, and on eight NVIDIA RTX 6000 PRO Black Edition \(96GB\) for the 235B model\. All non\-agentic runs use zero\-shot prompting with temperature0\.60\.6\. For each non\-agentic problem run, we generate a single completion\. For the agentic setting, each harness is evaluated with and without Numina\-Lean\-Agent[Liu et al\. \(2026a\)](https://arxiv.org/html/2608.29270#bib.bib54)\.

### B\.2Model Details

Base systemBackboneThinkingClaude CodeClaude Opus 4\.6\([Anthropic, 2026a](https://arxiv.org/html/2608.29270#bib.bib16)\)MediumClaude CodeClaude Opus 4\.8\([Anthropic, 2026b](https://arxiv.org/html/2608.29270#bib.bib15)\)MediumClaude CodeQwen3 235B\([Yang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib27)\)\-CodexGPT\-5\.4\([OpenAI, 2026a](https://arxiv.org/html/2608.29270#bib.bib19)\)Medium

Table 10:Configuration for agentic harnesses\.SettingFamilyModelsClosed\-sourceClaude\([Anthropic, 2025](https://arxiv.org/html/2608.29270#bib.bib18);[Anthropic, 2026c](https://arxiv.org/html/2608.29270#bib.bib17);[Anthropic, 2026a](https://arxiv.org/html/2608.29270#bib.bib16)\)Claude Haiku 4\.5, Claude Sonnet 4\.6, Claude Opus 4\.6Gemini\([Google DeepMind, 2025](https://arxiv.org/html/2608.29270#bib.bib22);[Google DeepMind, 2026](https://arxiv.org/html/2608.29270#bib.bib21)\)Gemini Flash 2\.5, Gemini Pro 3\.1GPT\([OpenAI, 2026a](https://arxiv.org/html/2608.29270#bib.bib19)\)GPT\-5\.4 nano, GPT\-5\.4 mini, GPT\-5\.4Open\-source generalGPT\-OSS\([Agarwal et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib23)\)GPT\-OSS\-20B, GPT\-OSS\-120BDeepSeek\([Guo et al\., 2025a](https://arxiv.org/html/2608.29270#bib.bib24)\)DeepSeek V3\.2, DeepSeek R1 0528Qwen\([Yang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib27)\)qwen3\-coder, Qwen3 235BLlama\([Grattafiori et al\., 2024](https://arxiv.org/html/2608.29270#bib.bib28)\)Llama 3\.1 8B, Llama 3\.1 70BOpen\-source Lean\-specializedKimina\([Wang et al\., 2025](https://arxiv.org/html/2608.29270#bib.bib52)\)Kimina 7B→\\to8BGoedel\([Lin et al\., 2025b](https://arxiv.org/html/2608.29270#bib.bib26)\)Goedel 8B→\\to8B, Goedel 8B→\\to32B

Table 11:Non\-agentic model configurations evaluated in our experiments\.We evaluate 19 non\-agentic model configurations across 9 model families, as listed in[Table11](https://arxiv.org/html/2608.29270#A2.T11)\. Parameter counts for closed\-source models are not publicly available\. General\-purpose open\-source models are evaluated directly, while Lean\-specialized rows use the two\-stage formalization\-to\-proving setup shown in[Table11](https://arxiv.org/html/2608.29270#A2.T11)\. The four agentic settings are Claude Code with Claude Opus 4\.6, or Claude Opus 4\.8, Claude Code with Qwen3 235B, and Codex with GPT\-5\.4\. Each setting is evaluated both with and without Numina\-Lean\-Agent, as listed in[Table10](https://arxiv.org/html/2608.29270#A2.T10)\.

### B\.3Per\-Metric Rates

L1L2L3Average\(n=113\)\(n=52\)\(n=13\)\(n=178\)ModelBEq\+BLEUJudgeBEq\+BLEUJudgeBEq\+BLEUJudgeBEq\+BLEUJudgeAgentic methodsClaude Code \(Opus 4\.6\)1\.86\.64\.40\.01\.61\.90\.00\.80\.01\.14\.73\.4\+ Numina12\.418\.98\.015\.413\.81\.97\.74\.50\.012\.916\.45\.6Claude Code \(Qwen3 235B\)0\.011\.60\.00\.07\.50\.00\.01\.20\.00\.09\.60\.0\+ Numina0\.09\.60\.00\.07\.40\.00\.02\.80\.00\.08\.50\.0Codex \(GPT\-5\.4\)1\.812\.45\.30\.010\.21\.97\.73\.80\.01\.711\.13\.9\+ Numina9\.715\.65\.37\.711\.81\.97\.72\.70\.09\.013\.53\.9Closed\-source LLMsGPT\-5\.42\.715\.11\.80\.012\.70\.07\.712\.80\.02\.214\.21\.1GPT\-5\.4 mini2\.711\.80\.00\.011\.51\.97\.712\.50\.02\.211\.80\.6GPT\-5\.4 nano0\.910\.50\.90\.08\.30\.00\.06\.60\.00\.69\.60\.6Gemini 3\.1 Pro4\.413\.85\.33\.811\.70\.07\.714\.40\.04\.513\.23\.4Gemini 2\.5 Flash3\.517\.71\.85\.813\.80\.015\.413\.40\.05\.116\.21\.1Claude Opus 4\.66\.219\.81\.81\.918\.01\.97\.714\.70\.05\.118\.91\.7Claude Sonnet 4\.65\.316\.82\.73\.813\.80\.015\.412\.70\.05\.615\.61\.7Claude Haiku 4\.52\.716\.10\.01\.914\.00\.015\.412\.60\.03\.415\.20\.0Open\-source LLMsGPT\-OSS\-120B1\.813\.92\.71\.913\.10\.07\.714\.20\.02\.213\.71\.7GPT\-OSS\-20B0\.95\.72\.71\.96\.70\.00\.08\.20\.01\.16\.21\.7DeepSeek R1 05280\.03\.80\.90\.02\.80\.00\.02\.90\.00\.03\.50\.6DeepSeek V3\.23\.516\.20\.00\.011\.90\.015\.411\.60\.03\.414\.60\.0Qwen3 235B−\-15\.3−\-−\-8\.7−\-−\-2\.4−\-−\-12\.4−\-qwen3\-coder0\.916\.40\.01\.910\.80\.015\.47\.00\.02\.214\.10\.0llama3\.1 70b0\.010\.20\.01\.98\.40\.07\.76\.60\.01\.19\.40\.0llama3\.1 8b0\.07\.60\.00\.06\.10\.07\.74\.90\.00\.67\.00\.0Lean\-specialized methodsKimina 7B→\\to8B0\.05\.90\.00\.05\.40\.00\.09\.60\.00\.06\.00\.0Goedel 8B→\\to32B0\.06\.60\.00\.06\.00\.00\.01\.70\.00\.06\.10\.0Goedel 8B→\\to8B0\.06\.10\.01\.98\.90\.07\.714\.60\.01\.17\.50\.0

Table 12:Per\-difficulty automatic metric results \(%\) onShadowBench\. BEq\+ and Judge are pass rates\. BLEU is a token\-level similarity score\. The Average columns are task\-weighted over 178 problems\.This section expands[Section6\.1](https://arxiv.org/html/2608.29270#S6.SS1)\.[Table12](https://arxiv.org/html/2608.29270#A2.T12)reports BEq\+, BLEU, and LLM\-as\-judge by difficulty\. The judge prompt is in[SectionI\.1](https://arxiv.org/html/2608.29270#A9.SS1)and the cost profile in[SectionC\.3](https://arxiv.org/html/2608.29270#A3.SS3)\.

## Appendix CCost and Compute

\\codeboxmax\_tokensBucket819216384SubtotalClosed \(API\)$23\.10$30\.46$53\.56Open \(via OpenRouter\)$3\.79$4\.70$8\.49Open \(self\-hosted\)$0\.00$0\.00$0\.00Total$26\.89$35\.16$62\.05Table 13:Non\-agentic generation cost across 33 runs and 178 prompts per run, taken from per\-call sidecar logs\.This section reports the compute and API budget used for the experiments\. Measured costs come from per\-call sidecar logs with\\codeboxprompt\_tokens,\\codeboxcompletion\_tokens, and OpenRouter\-quoted\\codeboxcost\_usd\. Estimated costs use observed prompt and completion lengths with provider pricing\. Self\-hosted Lean\-specialized models and Qwen3 235B were served on local GPUs, so we report wall\-clock time rather than cost\.

### C\.1Non\-Agentic Generation

[Table13](https://arxiv.org/html/2608.29270#A3.T13)aggregates per\-call sidecar logs across the 33 non\-agentic runs\. Closed\-source rows are billed by the model provider\. Open\-source API rows are billed through OpenRouter\. Open\-source self\-hosted rows are local vLLM deployments and have zero API cost\.

### C\.2Agentic Generation

ExperimentN tasksWall\-clock \(h\)Avg/task \(min\)Est\. cost \(USD\)Claude Code \(Opus 4\.6\)17820\.56\.9$310\+\+Numina178101\.234\.1$1,500Claude Code \(Opus 4\.8\)17820\.46\.9$310\+\+Numina17851\.817\.5$780Codex \(GPT\-5\.4\)1782\.80\.9$200\+\+Numina17821\.17\.1$330Claude Code \(Qwen3 235B\)178––local GPU\+\+Numina178––local GPUTotal217\.8$3,430Table 14:Estimated API cost of agentic methods over the 178 problems ofShadowBench\.The agentic runs use Claude Code and Codex, each with and without Numina\-Lean\-Agent\. Early experiments used subscription access, while later runs incurred paid API charges\. For consistent accounting,[Table14](https://arxiv.org/html/2608.29270#A3.T14)reports the estimated cost if all API\-capable agentic runs were billed through API\. We estimate cost from per\-task wall\-clock time and provider token throughput\. The table reports wall\-clock time and estimated API cost for the 178\-problem run\. Claude Code with Numina\-Lean\-Agent is the most costly API\-billed setting at 34\.1 minutes per problem\. Claude Code with Qwen3 235B uses the local vLLM server, so it has no API charge in this table\.

### C\.3LLM\-as\-Judge

ModelCallsCostanthropic/claude\-opus\-4\.79,207$324google/gemini\-3\.1\-pro\-preview9,207$58openai/gpt\-5\.49,207$98Total judge spend27,621$480Table 15:Cost of LLM\-as\-judge\.We score every cached generation with a three\-judge majority vote \(3 samples per judge, temperature 0\.5\)\. The three judges areanthropic/claude\-opus\-4\.7,google/gemini\-3\.1\-pro\-preview, andopenai/gpt\-5\.4, accessed via OpenRouter\. At three samples per judge, each candidate triggers nine completions\.

### C\.4Total

Adding the three components above, the API spend for the experiments reported in the main body is approximately $3,970 \($62 NA\+\+$3,430 agentic\+\+$480 judge\)\. Self\-hosted local GPU runs are not included in this API total\.

## Appendix DPer\-Configuration Agreement with Expert Judgment

MetricPrecisionRecallF1AgreementCompile0\.2141\.0000\.3530\.214BLEU0\.2650\.7220\.3880\.512LLM\-as\-judge0\.3750\.1670\.2310\.762BEq\+0\.3640\.2220\.2760\.750SA\-Passsoft0\.4000\.8890\.5520\.690SA\-Pass1\.0000\.8890\.9410\.976Table 16:Binary agreement of automatic metrics with expert judgment for outputs from Claude Code \(Opus 4\.6\) with Numina\-Lean\-Agent onShadowBench\. The best value per column is bold, and the second best is underlined\.MetricPrecisionRecallF1AgreementCompile0\.000––0\.000BLEU0\.000––0\.250LLM\-as\-judge0\.000––0\.750BEq\+–––1\.000SA\-Passsoft0\.000––0\.375SA\-Pass–––1\.000Table 17:Binary agreement of automatic metrics with expert judgment for outputs from Claude Code \(Opus 4\.6\) onShadowBench\. The best value per column is bold, and the second best is underlined\.MetricPrecisionRecallF1AgreementCompile0\.1921\.0000\.3220\.192BLEU0\.2860\.8420\.4270\.566LLM\-as\-judge0\.1430\.0530\.0770\.758BEq\+0\.4440\.2110\.2860\.798SA\-Passsoft0\.4521\.0000\.6230\.768SA\-Pass1\.0000\.9470\.9730\.990Table 18:Binary agreement of automatic metrics with expert judgment for outputs from Codex \(GPT\-5\.4\) with Numina\-Lean\-Agent onShadowBench\. The best value per column is bold, and the second best is underlined\.MetricPrecisionRecallF1AgreementCompile0\.1331\.0000\.2350\.133BLEU0\.0000\.0000\.0000\.567LLM\-as\-judge–0\.000–0\.867BEq\+–0\.000–0\.867SA\-Passsoft0\.5001\.0000\.6670\.867SA\-Pass1\.0001\.0001\.0001\.000Table 19:Binary agreement of automatic metrics with expert judgment for outputs from Codex \(GPT\-5\.4\) onShadowBench\. The best value per column is bold, and the second best is underlined\.MetricPrecisionRecallF1AgreementCompile0\.0831\.0000\.1540\.083BLEU0\.0000\.0000\.0000\.583LLM\-as\-judge–0\.000–0\.917BEq\+–0\.000–0\.917SA\-Passsoft0\.5001\.0000\.6670\.917SA\-Pass1\.0001\.0001\.0001\.000Table 20:Binary agreement of automatic metrics with expert judgment for outputs from Claude Code \(Qwen3 235B\) with Numina\-Lean\-Agent onShadowBench\. The best value per column is bold, and the second best is underlined\.MetricPrecisionRecallF1AgreementCompile0\.1111\.0000\.2000\.111BLEU–0\.000–0\.889LLM\-as\-judge–0\.000–0\.889BEq\+–0\.000–0\.889SA\-Passsoft0\.5001\.0000\.6670\.889SA\-Pass1\.0001\.0001\.0001\.000Table 21:Binary agreement of automatic metrics with expert judgment for outputs from Claude Code \(Qwen3 235B\) onShadowBench\. The best value per column is bold, and the second best is underlined\.For expert judgment, two mathematics experts independently evaluate whether each generated theorem is semantically aligned with the source problem\. The evaluation is finalized once both annotators reach consensus\. The disagreements are resolved through discussion\.

[Table4](https://arxiv.org/html/2608.29270#S5.T4)in the main text pools all six agentic configurations\.[Tables16](https://arxiv.org/html/2608.29270#A4.T16),[17](https://arxiv.org/html/2608.29270#A4.T17),[19](https://arxiv.org/html/2608.29270#A4.T19),[18](https://arxiv.org/html/2608.29270#A4.T18),[21](https://arxiv.org/html/2608.29270#A4.T21)and[20](https://arxiv.org/html/2608.29270#A4.T20)report them individually\. Across every configuration,SA\-Passachieves a Precision of1\.01\.0against expert judgment, with Recall of1\.01\.0except on two of the three Numina configurations, where it is0\.8890\.889and0\.9470\.947\. Claude Code \(Opus 4\.6\) without Numina\-Lean\-Agent produced only incorrect outputs, so Recall and F1 are undefined for it and Agreement is reported instead\.

#### False Negatives ofSA\-Pass\.

SA\-Passmisses three of the outputs the experts judged aligned\. All three state the intended theorem correctly but name their auxiliary declarations differently from the reference\. Two rename or omit them, and the other one declares the expected name as a theorem where the reference declares a definition\. The LLM matching step of checker adaptation \([Section4\.1](https://arxiv.org/html/2608.29270#S4.SS1)\) did not resolve these cases, so every forward check for those problems fails\.

## Appendix EThreshold Sensitivity

The relaxed scoreSA\-Passsoftis the fraction of passing shadow checks, and is thus non\-binary\. To test whether the choice of threshold affects agreement with expert judgment, we sweep a thresholdttand count a statement as positive when its passing fraction exceedstt\([Figure4](https://arxiv.org/html/2608.29270#A5.F4)\)\. F1 is flat belowt=0\.5t=0\.5, at0\.5520\.552for Claude Code \(Opus 4\.6\) with Numina\-Lean\-Agent and0\.6230\.623for Codex with Numina\-Lean\-Agent, and rises to0\.9410\.941and0\.9730\.973att=0\.5t=0\.5\. A passing fraction above one half requires both directions to pass, soSA\-Passsoftcoincides withSA\-Passfrom that point on\. We therefore reportSA\-Passsoftwitht=0t=0, the setting most distinct fromSA\-Pass\.

For BLEU, F1 peaks at a low cutoff and then falls \([Figure5](https://arxiv.org/html/2608.29270#A5.F5)\)\. Claude Code \(Opus 4\.6\) with Numina\-Lean\-Agent peaks at0\.4360\.436with a cutoff of0\.050\.05, and Codex with Numina\-Lean\-Agent at0\.4270\.427with a cutoff of0\.10\.1\. We report BLEU at a cutoff of0\.10\.1, which maximizes the mean F1 over the two configurations that have expert\-labelled positives, so BLEU is scored at its most favorable setting\. No cutoff brings BLEU near the agreementSA\-Passreaches\.

Figure 4:F1 ofSA\-Passsoftagainst expert judgment across the binarization thresholdtt\.Figure 5:F1 of BLEU against expert judgment across the cutofftt\.
## Appendix FRank Correlation with Expert Judgment

Metricρ\\rho\(↑\\uparrow\)τ\\tau\(↑\\uparrow\)Compile0\.990\.97BLEU0\.900\.79LLM\-as\-judge0\.720\.52BEq\+0\.760\.57SA\-Passsoft0\.820\.71SA\-Pass1\.001\.00Table 22:Spearmanρ\\rhoand Kendallτ\\taubetween the ranking of the six agentic systems by each automatic metric and by expert judgment, over the 178 problems\. The best value per column is in bold\.We measure whether each automatic metric ranks whole systems in the same order as a human expert\. Two human experts label every candidate Lean statement asokorreject\. We evaluate six agentic systems: Claude Code and Codex, each run directly and with Numina\-Lean\-Agent, and Qwen3 235B run directly and with Numina\-Lean\-Agent\. For each system, we aggregate every score over all 178 tasks and rank the systems by the expert pass rate\.[Table22](https://arxiv.org/html/2608.29270#A6.T22)reports Spearmanρ\\rhoand Kendallτ\\taubetween the ranking of the six systems induced by each metric and the expert ranking\.

SA\-Passrecovers the expert ranking exactly \(ρ=τ=1\.00\\rho=\\tau=1\.00\), and compile rate is next atρ=0\.99\\rho=0\.99, ahead of BLEU \(0\.900\.90\),SA\-Passsoft\(0\.820\.82\), BEq\+ \(0\.760\.76\), and LLM\-as\-judge \(0\.720\.72\)\. With six systems whose compile rates range from4\.5%4\.5\\%to55\.6%55\.6\\%, the system\-level ranking is a coarse test, and the per\-task agreement in[Table4](https://arxiv.org/html/2608.29270#S5.T4)separates the metrics further\.

## Appendix GPublic Challenge Track

![Refer to caption](https://arxiv.org/html/2608.29270v1/figures/codabench_track4.png)Figure 6:CodaBench page ofShadowBenchas Track 4 of the ICML 2026 AI4Math Challenge\.We released an early 126\-problem version ofShadowBenchas Track 4 of the ICML 2026 AI4Math Challenge\.[Figure6](https://arxiv.org/html/2608.29270#A7.F6)shows the CodaBench competition page that hosted the 126\-problem snapshot ofShadowBenchas Track 4 of the ICML 2026 AI4Math Challenge\. As we described in[Section4\.2](https://arxiv.org/html/2608.29270#S4.SS2), informal theorems and formalization rules are accessible to the public, while the checker theorems for evaluation remain hidden\. About 117 teams registered, but only twenty\-seven teams actually participated\.

The participants’ results show similar trends to our experiments\. TheSA\-Passsoftdistribution is skewed, where the median is8\.1%8\.1\\%, and the average is11\.1%11\.1\\%, while the compile rate averages61\.6%61\.6\\%\. That is, there is about a5\.5×5\.5\\timesgap between the compile rate andSA\-Passsoft, underlining that the compile rate causes false positives in formalizations\. In many of these low\-scoring cases, the submission replaces the target with a trivial statement closed by\\codeboxtrivial, which compiles but cannot be used by another theorem or declaration\. Such submissions give the compile rate many false positives\. They can even induce a ranking error, where the top five by compile rate share no member with the top five bySA\-Passsoft\. Compilation and BEq\+ produce rankings that differ substantially fromSA\-Passsoft\([Figure7](https://arxiv.org/html/2608.29270#A7.F7)\), with the compile rate agreeing at onlyρ=0\.41\\rho=0\.41and BEq\+ passing12\.4%12\.4\\%\. This result over many independent participants is consistent with the metric\-validity gap we measure against expert judgment in[Section6\.1](https://arxiv.org/html/2608.29270#S6.SS1)\.

The best submissions use agentic pipelines that decompose each goal into auxiliary lemmas, and we observe the same trend in our experiments, where Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent achieves the best result\. We examine two factors, agentic behavior and decomposition\. We label a submission as agentic when it runs more than three turns, and we measure decomposition by the number of declarations, such as lemma, def, or theorem\. The verified score correlates with the number of declarations at Spearman’sρ\\rhoof0\.590\.59and with the number of turns at0\.560\.56, emphasizing thatShadowBenchrequires multi\-turn solving through decomposition\.59\.7%59\.7\\%of submissions add at least one auxiliary lemma or definition \(3\.63\.6on average\), which is close to the4\.54\.5in the reference proofs \([Table9](https://arxiv.org/html/2608.29270#A1.T9)\)\.[Table23](https://arxiv.org/html/2608.29270#A7.T23)lists the top ten participants and their submission profiles\.

\(a\)Mean pass rate under compilation, BEq\+, andSA\-Passsoft\.\(b\)Per participant, the recomputed metric pass rate againstSA\-Passsoft\.
Figure 7:Metric disagreement on the public challenge\. In \([7\(a\)](https://arxiv.org/html/2608.29270#A7.F7.sf1)\), compilation accepts5\.5×5\.5\\timesas many outputs on average compared toSA\-Passsoft\. In \([7\(b\)](https://arxiv.org/html/2608.29270#A7.F7.sf2)\), points for compilation lie far from the diagonal, combining a high compile rate with a lowSA\-Passsoftscore, which indicates over\-acceptance\.RankSA\-Passsoft%Compile %No Sorry %Length \(Char\)AuxiliaryMultiple declaration %130\.968\.899\.23,0455\.3892\.0230\.175\.299\.22,9525\.4290\.4327\.952\.096\.85,1339\.5858\.2427\.880\.099\.22,3654\.4075\.2527\.477\.699\.22,8995\.7188\.0624\.763\.295\.24,1136\.5670\.8720\.975\.294\.49692\.4368\.9812\.579\.2100\.02,5672\.6947\.6911\.469\.6100\.02,4343\.5345\.21010\.866\.491\.18,0526\.8978\.8Table 23:Top ten teams on theShadowBenchpublic challenge track, anonymized and ranked bySA\-Passsoft\. Compile is the fraction of the 126 problems whose submitted solution compiles standalone\. No Sorry counts the number of problems solved without sorry\. Length indicates the average length of submission in characters\. Auxiliary is the average number of auxiliary declaration per each problem solution beyond single canonical solution\. Multiple declaration counts the number of solutions that used more than one declaration\. The medianSA\-Passsoftacross all 27 participants is8\.1%8\.1\\%\.
## Appendix HAnnotation Interface

The 178 problems were annotated through a custom browser\-based tool\. The tool exposes three views, each captured below\.[Figure8](https://arxiv.org/html/2608.29270#A8.F8)is the main page, which shows the number of problems annotated for each area and level\. Selecting a problem opens the detail page in[Figure9](https://arxiv.org/html/2608.29270#A8.F9)\. The detail view renders the natural language statement and proof, and exposes metadata such as area, level, paper of origin, subfields, and type tags\. This page also shows whether the problem is valid by compiling with the reference Lean code through the same Docker image used at evaluation time\. To submit the new problem, curators fill out the form in[Figure10](https://arxiv.org/html/2608.29270#A8.F10)\. This page accepts paired natural language text and Lean code, optional auxiliary imports, reference code that the examinee must complete, and hidden shadow checks used to evaluate semantic correctness\.

![Refer to caption](https://arxiv.org/html/2608.29270v1/figures/annotation_main.png)Figure 8:Data annotation landing page\. The left panel summarises area by level coverage\. The right panel ranks contributors by the number of problems they have annotated\. Selecting a row in the left panel opens the problem detail in[Figure9](https://arxiv.org/html/2608.29270#A8.F9)\.![Refer to caption](https://arxiv.org/html/2608.29270v1/figures/annotation_example.png)Figure 9:Problem detail view \(algebra/L3/alg\_grob\_L3\_001\)\. Header buttons surface the underlyingmeta\.jsonandgold\.lean, and the “Compile” / “Compile target” actions rerun the Lean type checker through the evaluation Docker image\. The body renders the LaTeX natural language statement and proof\.![Refer to caption](https://arxiv.org/html/2608.29270v1/figures/annotation_write.png)Figure 10:Submission form for a new problem\. The form pairs natural language text \(Math / NL text\) with Lean code, accepts optional auxiliary lemma imports, and separates the public target code from an optional hidden checker block used for semantic evaluation\.
## Appendix IPrompt Templates

Every prompt used in this paper is reproduced below verbatim, one per figure\. Placeholders of the form\{\{ … \}\}are filled per problem by the serving pipeline\. Raw text sources live underprompts/andscripts/judge\_prompt\.pyin the code repository\. The structured environments here mirror thesystem,user, andmodelroles in the API call\.

#### Non\-agentic prompt\.

We use the prompt shown in[Figure11](https://arxiv.org/html/2608.29270#A9.F11)for non\-agentic models\.

#### Agentic baseline\.

[Figure12](https://arxiv.org/html/2608.29270#A9.F12)shows the direct agentic prompt used without Numina\-Lean\-Agent\. The Claude Code rows invoke this prompt through the standard Claude Code CLI on the target Lean file\. Codex uses the same task instruction in its own wrapper\.

#### Agentic setting \(Numina\-Lean\-Agent\)\.

[Figure13](https://arxiv.org/html/2608.29270#A9.F13)is used for the\+ Numinarows of[Table3](https://arxiv.org/html/2608.29270#S5.T3)\. Numina\-Lean\-Agent runs the coordinator prompt below, which instructs the agent to select one targetsorryper session, sketch incrementally, and verify vialean\_diagnostic\_messages\.

### I\.1LLM\-as\-Judge Prompt

The judge prompt drives the Judge column in[Table12](https://arxiv.org/html/2608.29270#A2.T12)\. For each candidate the builder fills\{\{ informal\_block \}\}with the problem’s NL statement \(and NL proof, when the ablation condition provides one\),\{\{ formal\_ref \}\}with the reference Lean 4 statement withsorry, and\{\{ candidate \}\}with the model’s generated Lean 4 theorem plus its proof\.

The response parser accepts bare JSON, fenced JSON, and a permissive regex fallback\. Verdicts are normalised to \{correct,incorrect,uncertain\}\. All three are recorded per vote, then reduced by majority\.

System PromptYou are a helpful assistant that can interact multiple times with a computer shell to solve programming tasks\. However, for this specific interaction, you are acting as an expert Lean 4 mathematician tasked with implementing a formal Lean 4 declaration \(theorem or definition\) based on the provided context\.Your response must contain exactly ONE lean code block\.Include a THOUGHT section before your code where you explain your reasoning process\. Format your response as shown in<format\_example\>\.<format\_example\></format\_example\>Failure to follow these rules will cause your response to be rejected\.

User Prompt<task\_description\> Your task is to provide the full formal Lean 4 code for the specific declaration named\{\{ target\_code\_name \}\}\. The declaration is part of a larger code sequence, and you must implement it to fit seamlessly into the provided context\.The Code Context is provided below\.•Header: Imports and open namespaces\.•Code Before: Code appearing before the target\.•Target Code Name: The name of the definition or theorem you need to implement\.•Natural Language Description: A description of the target code in natural language\.•Code After: Code appearing after the target\.Header:Code Before:Target Code Name:Natural Language Description:Code After:<instructions\> \# Task Instructions \#\# Overview You are an expert Lean 4 mathematician\. You must provide the complete and correct Lean 4 implementation for\{\{ target\_code\_name \}\}\.•If it is a theorem, provide the statement and the full proof \(do not usesorry\)\.•If it is a definition, provide the full definition\.•Pay close attention toCode BeforeandCode Afterto infer the correct type signatures, variable names, and logical dependencies\.•Ensure your code compiles and integrates correctly with the surrounding context\.\#\# Output Coding Rules 1\. ATHOUGHTsection where you explain your reasoning:•Analyze theCode BeforeandCode Afterto deduce the purpose and signature of\{\{ target\_code\_name \}\}\.•Plan the implementation\.2\. A single lean code block with your implementation\.Format your responses like this:<format\_example\> [⬇](data:text/plain;base64,SSB3aWxsIGltcGxlbWVudCBcdGV4dHR0e2Zvb30gYXMgYSBkZWZpbml0aW9uIHRha2luZyB0d28gTmF0cyBhbmQgcmV0dXJuaW5nIHRoZWlyIHN1bS4=)Iwillimplement\\texttt\{foo\}asadefinitiontakingtwoNatsandreturningtheirsum\.</format\_example\>CRITICAL REQUIREMENTS:•Your response SHOULD include a THOUGHT section\.•Your response MUST include EXACTLY ONE lean block\.•This block MUST contain the COMPLETELY NEW implementation for\{\{ target\_code\_name \}\}\.•Do NOT repeat theHeaderorCode BeforeorCode After\. Only output the code for\{\{ target\_code\_name \}\}\.</instructions\>

AI Response

Figure 11:Prompt template for autoformalizing to Lean 4 code\.
User PromptComplete the target Lean theorem file, making it sorry\-free and ensuring it compiles without errors\.Use the toollean\_diagnostic\_messagesto verify the file\. Errors mean “severity 1” in the response\.IMPORTANT:•Do NOT write a detailed full proof plan upfront\. Instead, write a one or two sentence high\-level idea, then implement one step at a time, checkinglean\_goalafter each step to plan the next\.•Verify the file again after each update usinglean\_diagnostic\_messages\.•You may add helper lemmas, but do not create new axioms\.Tips:•Usesimpfirst, thensimp?to get minimal simp lemmas\.•Usenative\_decidefor computational results\.•Use\#evalto evaluate expressions\.•Usenorm\_castfor type conversions\.•Useapply?to find applicable lemmas\.•Ifdecidetimes out, do NOT simply increasemaxHeartbeats\. Instead, write a symbolic proof using mathematical reasoning and lemmas from Mathlib\.At the end of your response, include:where\{reason\}is:•LIMIT: stopped due to limits or there are still sorries/errors\.•COMPLETE: the file is sorry\-free AND compiles without errors\.IMPORTANT:Uselean\_diagnostic\_messagesto verify, do not uselake build\.

Figure 12:Prompt template for the direct agentic baseline without the retrieval harness\.
User PromptPlease analyze all sorries in the file and choose ONLY ONE that you believe is most approachable or strategically important to work on\.\# Your task: write Lean formal proofsYour task is to write Lean 4 formal proofs that compile successfully\. Replacesorrywith executable Lean code \(tactics, term\-mode proofs, etc\.\) that passes the Lean compiler\. Choose ONLY ONE target lemma/sorry for this entire session, focus on it and try your best to complete it\.\# \[Critical prohibition\] no natural language proofs1\.ZERO TOLERANCE FOR NARRATIVE COMMENTS\. You are forbidden from using comments \(/\- …\-/or\-\-\) to write mathematical derivations, proof plans, or natural\-language explanations\.2\.STRICT COMMENT LENGTH LIMIT\. No single comment block may exceed 42 lines\.3\.CODE IS THE EXPLANATION\. If a logic step is complex enough to need an explanation, extract it into a new helper lemma\.4\.CONSTRAINT COMMENT\. Prohibit sequences of 5 or more consecutive comment blocks unless interleaved with valid Lean code\.\# Session focus rulesAt session start:1\.Identify all remaining sorries or failed proofs\.2\.Select EXACTLY ONE target that is most approachable and strategically important\.3\.Announce:"TARGET FOR THIS SESSION: \[lemma\_name\] at line \[line\_number\]"\.During session: only work on your selected target and any new helper lemmas you create for it\.End session with ONE of:•SELECTED\_TARGET\_COMPLETE: target fully proven\.•COMPLETE: all sorries in folder proven\.•LIMIT: stopped due to token/time/error limits\.\# Incremental planningDo NOT write a detailed upfront plan\. Instead:1\.Abstract sketch: a one or two sentence high\-level idea\.2\.One step at a time\. After each step, uselean\_goalandlean\_diagnostic\_messages\.3\.Re\-plan from the actual proof state, not from your initial sketch\.\# Tools•lean\_diagnostic\_messages,lean\_goal,lean\_leandex,gemini\_informal\_prover,create\_formal\_sketch,discussion\_partner\.•Do NOT uselake buildorlean\_build\. Always uselean\_diagnostic\_messages\.\# End formatAt the very end of the response include exactly one line:

Figure 13:Prompt template for the Numina\-Lean\-Agent harness used with Claude Code, Codex, and Qwen3 235B\.
System PromptYou are an expert in Lean 4 and Mathlib\. Decide whether a candidate Lean 4 statement\+proof semantically establishes the INTENDED mathematical theorem shown alongside it\.Return ONE JSON object and nothing else:[⬇](data:text/plain;base64,ICJyZWFzb24iOiAgIjwxLTMgc2VudGVuY2VzPiJ9)"reason":"<1\-3sentences\>"\}•"correct": \(a\) the candidate’s stated theorem is mathematically equivalent to the intended claim, AND \(b\) its proof actually justifies that claim\.•"incorrect": statement weaker/stronger/wrong OR proof unsound, circular, or relies on a broken auxiliary\.•"uncertain": artifact truncated or unreadable\.

User Prompt\# Intended problem \(informal\)\# Intended formal statement \(reference Lean 4, proof body issorry\)\# Candidate \(Lean 4, statement \+ attempted proof\)Return your JSON verdict now\.

AI Response[⬇](data:text/plain;base64,ICJyZWFzb24iOiAgInt7IHJlYXNvbiB9fSJ9)"reason":"\{\{reason\}\}"\}

Figure 14:Prompt template for the LLM\-as\-judge proof correctness evaluator\.
\#\#Task

Thenatural\-languagetextbelowstatesamathematicalresult\.Itcontains

severaldistinctsub\-claims\(e\.g\.conjunctions,consequences,specialisations,

unfoldeddefinitions,orotherpropertiesimpliedbythemainstatement\)\.

Step1—identifythesub\-claimspresentintheNLtext\.

Step2—foreachtargetdeclarationlistedbelow,writeoneLean

examplepersub\-claimthatPROVESthatsub\-claimfollowsfromthesolver’s

declaration\.Thecheckerisappendedafterthesolver’soutput,sothe

solver’sdeclarationnameisalreadyinscope\.

\#\#Rulesforeverygeneratedcheckeritem

\-ItmustbeaSTRICTsub\-statementofthecorrespondingtargetitem:a

projection\(\.1/\.2/\.mp/\.mpr\),aspecialisation\(∀instantiatedataconcrete

value\),anunfolded/simp\-normalform,aniffdirection,oradirect

consequencethatthesolvermusthaveactuallyproved\.

\-Itmustreferenceandusethetargetdeclarationnameinitsproof\.

\-ItmustNOTrestatethefulltargetdeclarationandproveitbyexact/simpa

usingthetargetdeclaration\.Thatisjustcopyingthetheorem,notahidden

checker\.

\-ItmustNOTcopyfromgold\.leanproofs\.Youaregivenonlytargetdeclaration

headersandtextmatches;generatesmallshadowsfromthosedeclarations\.

\-Itmustcontainnosorry,admit,axiom,constant,namespace,orend\.

\-Preferanonymoustop\-level‘example‘declarations\.Donotintroducenamed

declarationsunlessneeded\.

\-Useexplicitbinders;donotassumevariablesthatarenotinscope\.The

declaration’sparametersareONLYwhatappearsinitssignaturebeforethe

‘:‘\(thereturntype\)\.Nothingafter‘:=‘isaparameter\.

\-An‘↔‘\(Iff\)propositionisNOTafunctionandcannotbeappliedto

arguments\.Neverwrite‘exact\(iff\_lemmaarg1arg2\)‘or‘simpausing

\(iff\_lemmaarg1arg2\)‘\.Use‘\.mp‘,‘\.mpr‘,‘\.1‘,or‘\.2‘toaccess

itsdirections:‘exact\(iff\_lemmaarg1arg2\)\.mp‘\.

\-Forconjunctionconclusions,generateoneshadowperconjunctusing‘\.1‘,

‘\.2‘,‘\.2\.1‘,etc\.Donotaddhelper\-onlyorcompleteness\-certificateitems:

everycheckerdeclarationisscoredindependentlyandmustusethetarget

declarationinitsproofbody\.

\-Foriffconclusions,generate‘\.mp‘and‘\.mpr‘shadows\.Donotadda

completenesscertificate\.

\#\#Proofrobustnessrequirement

Solversmaydeclarethesametheoremwithadifferentbinderstyle\(makingsome

argumentsimplicit,reorderingtype\-classparameters,etc\.\)whilebeing

mathematicallycorrect\.Tomaximisecompatibility,everycheckeritemMUSTuse

a‘first\|…\|…‘tacticblockwiththefollowingthreealternativesinorder:

1\.Directprojectionusingthegoldargumentlist:

‘exact\(TARGETARGS\)\.PROJECTION‘

2\.Let\-boundvariant\(separateselaboration,helpswithuniverse/instanceissues\):

‘exact\(let\_hc:=TARGETARGS;\_hc\.PROJECTION\)‘

3\.Argument\-agnosticfallback—letsLean’sunifierdeterminehowtoapplythe

solver’sdeclarationregardlessofhowthesolverdeclareditsbinders:

‘suffices\_hc:FULL\_CONCLUSIONbyexact\_hc\.PROJECTION;applyTARGET<;\>assumption‘

Exampleforaconjunctionconjunct\(‘\.1‘of‘foo\(n:ℕ\)\(h:n\>0\):An∧Bn‘\):

“‘lean

example\(n:ℕ\)\(h:n\>0\):

An:=by

first

\|exact\(foonh\)\.1

\|exact\(let\_hc:=foonh;\_hc\.1\)

\|\(suffices\_hc:An∧Bnbyexact\_hc\.1;applyfoo<;\>assumption\)

“‘

Exampleforaniffforwarddirection\(‘bar\(x:α\):Px↔Qx‘\):

“‘lean

example\(x:α\):

Px→Qx:=by

first

\|exact\(barx\)\.mp

\|exact\(barx\)\.1

\|exact\(let\_hc:=barx;\_hc\.mp\)

\|\(suffices\_hc:Px↔Qxbyexact\_hc\.mp;applybar<;\>assumption\)

“‘

Fornon\-structuralsub\-claims\(specialisations,unfoldings,consequences\),applythe

samepattern:leadwiththenatural‘exact‘,followwitha‘let‘\-boundvariant,and

closewiththe‘applyTARGET<;\>assumption‘fallbackwrappedin‘suffices‘\.

\#\#Problem

Problemid:\{problem\_id\}

Targetdeclarations\(musteachappearinatleastonechecker\):\{target\_names\}

Targetsource:\{target\_source\_label\}

Targetitems:

\{targetitems\}

\#\#Formalizationrules

\{formalizationrules\}

\#\#Natural\-languagetext\(sourceofsub\-claims\)

\{natural\-languagetext\}

\#\#Outputformat

Ifmultiplecheckerdeclarationsarealternativeversionsofthesametargetsubstatement,

givethemidenticaltarget/substatementmetadata;theirLeandoc\-commentlabelswillbe

normalizedtoShadow1\-1,Shadow1\-2,etc\.DistinctsubstatementsremainShadow1,

Shadow2,etc\.

ReturnONLYvalidJSON—nomarkdown,noprose,noextrakeys:

\{

"checker\_code":"<completeLeancodeblocktoappendaftersolveroutput\>",

"items":\[

\{

"target\_index":1,

"target\_name":"foo",

"checker\_names":\["hidden\_foo\_part1"\],

"method":"projection/specialisation/unfolding/iff\_direction/consequence",

"substatement":"one\-linedescriptionofthesub\-claim"

\}

\],

"rationale":"one\-linesummary"

\}

Figure 15:Prompt for generating forward checker theorems, i\.e\. strict sub\-statements \(shadows\)SiS\_\{i\}withT⇒SiT\\Rightarrow S\_\{i\}, from the reference formal statement\. Deterministic shadows are emitted first and this prompt fills the remaining cases\.
Goldtarget‘\{target\_name\}‘hasconclusion:

\{conclusion\}

Youaregiventhesesub\-statementsashypotheses:

\{shadowhypotheses\}

WriteasingleLean4‘example‘thattakesexactlythosehypothesesandprovesthegoldconclusion:

example\{binderprefix\}

\{shadowhypotheses\}:

\{conclusion\}:=by

<proof\>

Rules:

\-UseONLYthegivenhypothesesh\_bc\_i\(donotreferencetheoriginaltargetoranysolvertheorem\)\.

\-Prefer‘exact⟨…⟩‘forconjunctions,‘⟨\.mp,\.mpr⟩‘styleforiff,or‘constructor‘/‘refine‘/‘tauto‘\.

\-OutputONLYtheLeancodeblock,noprose\.

Figure 16:Prompt for the backward sufficiency certificate⋀iSi⇒T\\bigwedge\_\{i\}S\_\{i\}\\Rightarrow T, used as a fallback when the certificate cannot be produced structurally\.

## Appendix JShadow Check Case Studies

These case studies instantiate the forward checks of[Section3\.2](https://arxiv.org/html/2608.29270#S3.SS2)on real statements\. In the first case \([SectionJ\.1](https://arxiv.org/html/2608.29270#A10.SS1)\), the intended statementTTsays a finite morphism is projective, that is, finite⇒\\Rightarrowprojective\. Its shadows \([Equation3](https://arxiv.org/html/2608.29270#A10.E3)\) are affine \(S1S\_\{1\}\) andHasProjectiveEmbedding\(S2S\_\{2\}\), so the forward checksT⇒SiT\\Rightarrow S\_\{i\}are finite⇒\\Rightarrowaffine and finite⇒HasProjectiveEmbedding\\Rightarrow\\texttt\{HasProjectiveEmbedding\}, written as the two Lean examples that follow\. The separation condition \([Equation5](https://arxiv.org/html/2608.29270#A10.E5)\) keeps the two shadows distinct, so passing the forward checks is not vacuous\. This non\-triviality is what a complete shadow set requires, and the backward checkS1∧⋯∧Sn⇒TS\_\{1\}\\wedge\\cdots\\wedge S\_\{n\}\\Rightarrow Tis the completeness half it protects\. Each later case names its own targetTTand the shadowsSiS\_\{i\}that must follow from it\.

This appendix walks through eight case studies that illustrate how these shadow checks apply to real mathematical statements\. The first case is worked out in detail\. The others are sketched\.

### J\.1Algebraic Geometry: Finite Morphisms Are Projective

Consider the textbook theorem that finite morphisms are projective\. Let

A\\displaystyle A=finite morphism,\\displaystyle=\\text\{finite morphism\},\(2\)B\\displaystyle B=projective morphism\\displaystyle=\\text\{projective morphism\}
WriteHasProjectiveEmbedding​\(f\)\\texttt\{HasProjectiveEmbedding\}\(f\)for the property thatXXadmits a closedSS\-immersion intoℙSn\\mathbb\{P\}^\{n\}\_\{S\}for somen≥0n\\geq 0\(whereSSis the target offf\)\. Natural shadows are

A′\\displaystyle A^\{\\prime\}=affine morphism,\\displaystyle=\\text\{affine morphism\},\(3\)B′\\displaystyle B^\{\\prime\}=HasProjectiveEmbedding\\displaystyle=\\texttt\{HasProjectiveEmbedding\}The forward checks rely on the implications

finite\\displaystyle\\text\{finite\}⇒affine,\\displaystyle\\Rightarrow\\text\{affine\},\(4\)projective\\displaystyle\\text\{projective\}⇒HasProjectiveEmbedding\.\\displaystyle\\Rightarrow\\texttt\{HasProjectiveEmbedding\}\.
The second holds because a projective morphismf:X→Sf:X\\to Sfactors as a closedSS\-immersionX↪ℙSnX\\hookrightarrow\\mathbb\{P\}^\{n\}\_\{S\}followed by the projection, soXXadmits the required closedSS\-immersion by construction\. The separation condition holds because an affine morphism need not have propertyHasProjectiveEmbedding: a closedSS\-subscheme ofℙSn\\mathbb\{P\}^\{n\}\_\{S\}is proper overSS, but affine morphisms need not be proper\. Over a fieldkk, the structure morphism

𝔸k1→Spec⁡k\\mathbb\{A\}^\{1\}\_\{k\}\\to\\operatorname\{Spec\}kis affine, but𝔸k1\\mathbb\{A\}^\{1\}\_\{k\}admits no closed immersion into anyℙkn\\mathbb\{P\}^\{n\}\_\{k\}, since any such subscheme would be proper\. Thus

A′⇏B′\.\\displaystyle A^\{\\prime\}\\nRightarrow B^\{\\prime\}\.\(5\)
The public task asks the solver to define finite and projective morphisms and prove that finite implies projective\. The hidden checker contains the forward\-check one\-liners:

example\{X Y : Scheme\}\{f : X⟶\\longrightarrowY\}\(hf : IsFinite f\) :IsAffineHom f := bysimpa using IsFinite\.isAffine hf

and the check for the second shadow, discharged by applying the solver’s theorem

example\{X S : Scheme\}\{f : X⟶\\longrightarrowS\}\(hf : IsFinite f\) :HasProjectiveEmbedding f := bysimpa \[HasProjectiveEmbedding\]using finite\_implies\_projective hf

If the first check fails, the LLM fallback attempts to proveIsFinite⇒\\RightarrowIsAffineHomfrom the solver’s definition\. The second check is not subject to fallback, since it must be discharged through the solver’s theorem\.

### J\.2Projective Products and Hidden Properness

A related theorem is that the fiber product of two projective schemes over a base is projective, classically via the Segre embedding\. The public theorem may be:

X→S​projective,Y→S​projective\\displaystyle X\\to S\\text\{ projective\},Y\\to S\\text\{ projective\}\(6\)⇒X×SY→S​projective\\displaystyle\\Rightarrow X\\times\_\{S\}Y\\to S\\text\{ projective\}
A hidden forward check can ask whether the product morphism has propertyHasProjectiveEmbedding, i\.e\., whetherX×SYX\\times\_\{S\}Yadmits a closedSS\-immersion into someℙSn\\mathbb\{P\}^\{n\}\_\{S\}\. This tests that the product theorem returns projectivity in a usable form and that the solver’s definition of projectivity connects to the trustedHasProjectiveEmbeddingpredicate\. Here the targetTTis the projectivity of the product morphism, and the shadowS1S\_\{1\}is the property that the product hasHasProjectiveEmbedding, so the forward checkT⇒S1T\\Rightarrow S\_\{1\}asks the product to admit a closedSS\-immersion into someℙSn\\mathbb\{P\}^\{n\}\_\{S\}\.

### J\.3Compiled False Positive: Projective as Proper

Claude Opus 4\.6 and Claude Sonnet 4\.6 both produced the following definition for an algebraic\-geometry problem about projective morphisms\. The submission compiles, but it defines projectivity as properness:

class IsProjective\{S X : Scheme\}\(f : X⟶\\longrightarrowS\) : Prop whereisProper : IsProper f

With this definition, the generated theorem is immediate:

import Mathlibnamespace ABMnamespace algebraic\_geometrynamespace L3namespace alg\_sche\_L3\_003open CategoryTheory AlgebraicGeometryclass IsProjective\{S X : Scheme\}\(f : X⟶\\longrightarrowS\) :Prop whereisProper : IsProper fopen CategoryTheory\.Limitstheorem projective\_isProper\{S X : Scheme\}\(f : X⟶\\longrightarrowS\) \[IsProjective f\] :IsProper f :=IsProjective\.isProperend alg\_sche\_L3\_003end L3end algebraic\_geometryend ABM

Compile rate marks this candidate as correct because the theorem block type\-checks\.SA\-Passrejects it: the hidden shadow checks require the generated notion of projectivity to support the intended algebraic\-geometric content, not only the weaker properness property\. Here the shadowSSis againHasProjectiveEmbedding, and the forward checkT^⇒S\\widehat\{T\}\\Rightarrow Sfails, because the generated statement proves only properness, which does not implyHasProjectiveEmbedding\.

### J\.4Compiled Weakening: Complex Structure Dropped

The forward check verifies the weakened statements\. Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent produced the following statement for a Fourier analysis problem, whose intended lemma is a Gaussian truncation limit used toward Fourier inversion\. The intended statement is complex valued:

\-\- Intended statement \(abridged\)variable \{E : Type\*\}\[NormedAddCommGroup E\]\[NormedSpaceℂ\\mathbb\{C\}E\] \{f : V→\\toE\}lemma tendsto\_integral\_cexp\_sq\_smul\(hf : Integrable f\) :Tendsto\(fun c :ℝ\\mathbb\{R\}=\>∫\\intv : V,cexp \(\- c\-1\*∥\\\|v∥\\\|ˆ2\)∙\\bulletf v\)atTop \(nhds \(∫\\intv : V, f v\)\)

The generated output compiles with a correct proof of a real\-valued variant\. It replacescexpand theℂ\\mathbb\{C\}module structure onEEwithReal\.expand anℝ\\mathbb\{R\}module structure, and generalizes the volume measure to an arbitrary measure:

\-\- Submission \(abridged\)\{E : Type\*\} \[NormedAddCommGroup E\]\[NormedSpaceℝ\\mathbb\{R\}E\] \{f : V→\\toE\}\{μ\\mu: Measure V\}lemma tendsto\_integral\_cexp\_sq\_smul\(hf : Integrable fμ\\mu\) :Tendsto\(fun c :ℝ\\mathbb\{R\}=\>∫\\intv,Real\.exp\(\- c\-1\*∥\\\|v∥\\\|ˆ2\)∙\\bulletf v∂\\partialμ\\mu\)atTop \(nhds \(∫\\intv, f v∂\\partialμ\\mu\)\)

The backward check passes, since the shadows derived from the complex statement imply the real variant\. The forward check fails, since the real variant does not recover the complex shadow\. Compile rate considers this generation as correct, andSA\-Passrejects it as a weakening\.

### J\.5Compiled False Positive: Conclusion Assumed as a Hypothesis

A compiling submission can also prove a different statement\. Claude Code \(Opus 4\.8\) with Numina\-Lean\-Agent produced the following statement for Brahmagupta’s formula \(geo\_gen\_L2\_007\)\. The intended theorem computes the area of a cyclic quadrilateral, stated as the measure of the convex hull of the four vertices:

\-\- Intended statement \(abridged\)theorem brahmagupta\_formula\{A B C D : EuclideanSpaceℝ\\mathbb\{R\}\(Fin 2\)\}\(h\_cyclic : Concyclic\(\{A, B, C, D\} : Set \_\)\)\(h\_convex :\(openSegmentℝ\\mathbb\{R\}A C∩\\capopenSegmentℝ\\mathbb\{R\}B D\)\.Nonempty\):let s := \(dist A B \+ dist B C\+ dist C D \+ dist D A\) / 2let K := \(volume \(convexHullℝ\\mathbb\{R\}\(\{A, B, C, D\} : Set \_\)\)\)\.toRealK = sqrt \(\(s \- dist A B\)\* \(s \- dist B C\)\* \(s \- dist C D\)\* \(s \- dist D A\)\)

The submission compiles with a correct proof of a different statement\. It receives the valueKKas a hypothesis that already encodes the triangle decomposition of the area, and replaces concyclicity of the four points with an angle condition:

\-\- Submission \(abridged\)theorem brahmagupta\_formula\(A B C D : P\) \(a b c d s K :ℝ\\mathbb\{R\}\)\(ha : a = dist A B\)\(hb : b = dist B C\)\(hc : c = dist C D\)\(hd : d = dist D A\)\(hs : s = \(a \+ b \+ c \+ d\) / 2\)\(hcyclic :EuclideanGeometry\.angle D A B\+ EuclideanGeometry\.angleB C D =π\\pi\)\(harea : K = 1 / 2 \* a \* d\* Real\.sin\(EuclideanGeometry\.angleD A B\)\+ 1 / 2 \* b \* c\* Real\.sin\(EuclideanGeometry\.angleB C D\)\)\(hK : 0≤\\leqK\) :K = Real\.sqrt \(\(s \- a\) \* \(s \- b\)\* \(s \- c\) \* \(s \- d\)\)

The resulting statement is an identity about the assumed valueKK, not a statement about the area\. Both check directions fail, since the submission neither implies nor is implied by the shadows of the intended theorem\. Compile rate counts this submission as correct, andSA\-Passrejects it\.

### J\.6Backup Declarations on ProofNet

The larger models often attach a backup declaration to a long proof attempt\. Claude Opus 4\.6 produced the following output for Herstein Exercise 2\.1\.18 on ProofNet, which asks for an elementa≠1a\\neq 1witha=a−1a=a^\{\-1\}in a group of even order\. The generated statement matches the intended one, and the output carries a second declaration that ends insorry:

\-\- Claude Opus 4\.6 \(abridged\)theorem exercise\_2\_1\_18\{G : Type\*\} \[Group G\]\[Fintype G\] \(hG2 : Even \(card G\)\) :∃\\exists\(a : G\), a≠\\neq1∧\\landa = a\-1:= byhave h :∃\\existsa : G, a≠\\neq1∧\\landa \* a = 1:= by\.\.\. \-\- long proof attempttheorem exercise\_2\_1\_18’\{G : Type\*\} \[Group G\]\[Fintype G\] \(hG2 : Even \(card G\)\) :∃\\exists\(a : G\), a≠\\neq1∧\\landa = a\-1:= bysorry

The evaluation takes the last theorem block as the candidate \([Section5\.1](https://arxiv.org/html/2608.29270#S5.SS1)\), which here is the backup declaration, so the output is rejected\. Claude Haiku 4\.5 emits a single declaration with the same statement for this problem and passes\.

### J\.7Flat Morphisms and Openness

For flat morphisms, a classical theorem states that a flat morphism locally of finite presentation is open\. A benchmark can use

A\\displaystyle A=flat and locally of finite presentation,\\displaystyle=\\text\{flat and locally of finite presentation\},\(7\)B\\displaystyle B=open map\.\\displaystyle=\\text\{open map\}\.
Possible shadows include generalizing maps and universally open morphisms, depending on the available benchmark environment\. Here the targetTTisA⇒BA\\Rightarrow B, and the shadowsSiS\_\{i\}are properties such as being a generalizing map or a universally open morphism thatBBshould entail, so each forward checkT⇒SiT\\Rightarrow S\_\{i\}tests one consequence of openness\. Here the separation condition must be checked carefully: if the chosen shadow ofAAalready implies the chosen shadow ofBBin that environment, then the item is vulnerable to collapse\. The framework forces the benchmark designer to make this relationship explicit before releasing the task\.

### J\.8Homotopy and Homology

In algebraic topology, many one step facts are already explicit in mature libraries: path homotopy is an equivalence relation, path homotopy respects concatenation, homotopy equivalences compose, and so on\. Such facts should not be visible target theorems if the goal is to evaluate autoformalization beyond retrieval\.

The shadow based evaluation suggests using derived tasks instead\. For instance, a public theorem may ask for a bundled threefold product statement for homotopy equivalences, while hidden checks specialize it to product with an identity factor\. In homology, a public theorem may bundle the degree zero homology computation of totally disconnected spaces with positive degree vanishing, while hidden checks specialize to concrete degrees\. Here each public targetTTis a bundled statement, and the shadowsSiS\_\{i\}are its specializations, so the forward checksT⇒SiT\\Rightarrow S\_\{i\}project the bundle onto one component in the bundled\-conclusion pattern of[Section3\.2](https://arxiv.org/html/2608.29270#S3.SS2)\. These tasks are not merely lookups of named declarations\. They require composing library facts into reusable results\.

## Appendix KComplete Shadow Set Checker Patterns

### K\.1Bundled Conclusions

For a bundled theorem, the hidden checker can compile each projection\.

\-\- Expected submission:\-\- theorem main : A \-\> B1 /\\ B2 /\\ B3example \(hA : A\) : B1 := byexact \(main hA\)\.1example \(hA : A\) : B2 := byexact \(main hA\)\.2\.1example \(hA : A\) : B3 := byexact \(main hA\)\.2\.2

### K\.2Equality as Two Inequalities

For equality\-valued theorems, the hidden checker can compile both inequality consequences\.

\-\- Expected submission:\-\- theorem main \(hA : A\) : f B = f Cexample \(hA : A\) : f B <= f C := byexact le\_of\_eq \(main hA\)example \(hA : A\) : f C <= f B := byexact ge\_of\_eq \(main hA\)

The exact lemmas depend on the proof assistant and ordered structure\. The benchmark uses the idiomatic library lemmas for converting equality into the two inequality directions\.

### K\.3Saddle\-Point Derivatives

This example on the next page shows a complete shadow set for a theorem whose conclusion is a pair of first\-order conditions\. The intended conclusion isD​x=0∧D​z=0Dx=0\\wedge Dz=0\. The hidden checker splits it into two shadows and then checks that the two shadows recover the full conclusion\.

/\-\- Shadow 1: the derivative of the \`x\`\-section vanishes\. \-/example\{n m :ℕ\\mathbb\{N\}\}\{f : \(Fin n→\\toℝ\\mathbb\{R\}\)×\\times\(Fin m→\\toℝ\\mathbb\{R\}\)→\\toℝ\\mathbb\{R\}\}\{x0 : Fin n→\\toℝ\\mathbb\{R\}\} \{z0 : Fin m→\\toℝ\\mathbb\{R\}\}\{Dx : \(Fin n→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\}\{Dz : \(Fin m→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\}\(hs :∀\\forallx z, f \(x0, z\)≤\\leqf \(x0, z0\)∧\\landf \(x0, z0\)≤\\leqf \(x, z0\)\)\(hx : HasFDerivAt \(fun x =\> f \(x, z0\)\) Dx x0\)\(hz : HasFDerivAt \(fun z =\> f \(x0, z\)\) Dz z0\) :Dx = 0 := byexact \(saddle\_sections\_hasFDerivAt\_eq\_zero hs hx hz\)\.1/\-\- Shadow 2: the derivative of the \`z\`\-section vanishes\. \-/example\{n m :ℕ\\mathbb\{N\}\}\{f : \(Fin n→\\toℝ\\mathbb\{R\}\)×\\times\(Fin m→\\toℝ\\mathbb\{R\}\)→\\toℝ\\mathbb\{R\}\}\{x0 : Fin n→\\toℝ\\mathbb\{R\}\} \{z0 : Fin m→\\toℝ\\mathbb\{R\}\}\{Dx : \(Fin n→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\}\{Dz : \(Fin m→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\}\(hs :∀\\forallx z, f \(x0, z\)≤\\leqf \(x0, z0\)∧\\landf \(x0, z0\)≤\\leqf \(x, z0\)\)\(hx : HasFDerivAt \(fun x =\> f \(x, z0\)\) Dx x0\)\(hz : HasFDerivAt \(fun z =\> f \(x0, z\)\) Dz z0\) :Dz = 0 := byexact \(saddle\_sections\_hasFDerivAt\_eq\_zero hs hx hz\)\.2/\-\- Completeness certificate: Shadow 1∧\\landShadow 2⇒\\RightarrowDx = 0∧\\landDz = 0\. \-/example\(hDx :∀\\forall\{n m :ℕ\\mathbb\{N\}\}\{f : \(Fin n→\\toℝ\\mathbb\{R\}\)×\\times\(Fin m→\\toℝ\\mathbb\{R\}\)→\\toℝ\\mathbb\{R\}\}\{x0 : Fin n→\\toℝ\\mathbb\{R\}\} \{z0 : Fin m→\\toℝ\\mathbb\{R\}\}\{Dx : \(Fin n→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\}\{Dz : \(Fin m→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\},\(∀\\forallx z, f \(x0, z\)≤\\leqf \(x0, z0\)∧\\landf \(x0, z0\)≤\\leqf \(x, z0\)\)→\\toHasFDerivAt \(fun x =\> f \(x, z0\)\) Dx x0→\\toHasFDerivAt \(fun z =\> f \(x0, z\)\) Dz z0→\\toDx = 0\)\(hDz :∀\\forall\{n m :ℕ\\mathbb\{N\}\}\{f : \(Fin n→\\toℝ\\mathbb\{R\}\)×\\times\(Fin m→\\toℝ\\mathbb\{R\}\)→\\toℝ\\mathbb\{R\}\}\{x0 : Fin n→\\toℝ\\mathbb\{R\}\} \{z0 : Fin m→\\toℝ\\mathbb\{R\}\}\{Dx : \(Fin n→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\}\{Dz : \(Fin m→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\},\(∀\\forallx z, f \(x0, z\)≤\\leqf \(x0, z0\)∧\\landf \(x0, z0\)≤\\leqf \(x, z0\)\)→\\toHasFDerivAt \(fun x =\> f \(x, z0\)\) Dx x0→\\toHasFDerivAt \(fun z =\> f \(x0, z\)\) Dz z0→\\toDz = 0\) :∀\\forall\{n m :ℕ\\mathbb\{N\}\}\{f : \(Fin n→\\toℝ\\mathbb\{R\}\)×\\times\(Fin m→\\toℝ\\mathbb\{R\}\)→\\toℝ\\mathbb\{R\}\}\{x0 : Fin n→\\toℝ\\mathbb\{R\}\} \{z0 : Fin m→\\toℝ\\mathbb\{R\}\}\{Dx : \(Fin n→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\}\{Dz : \(Fin m→\\toℝ\\mathbb\{R\}\)→\\toL\[ℝ\\mathbb\{R\}\]ℝ\\mathbb\{R\}\},\(∀\\forallx z, f \(x0, z\)≤\\leqf \(x0, z0\)∧\\landf \(x0, z0\)≤\\leqf \(x, z0\)\)→\\toHasFDerivAt \(fun x =\> f \(x, z0\)\) Dx x0→\\toHasFDerivAt \(fun z =\> f \(x0, z\)\) Dz z0→\\toDx = 0∧\\landDz = 0 := byintro n m f x0 z0 Dx Dz hs hx hzexact⟨\\langlehDx hs hx hz, hDz hs hx hz⟩\\rangle

## Appendix LAuthor Contact Information

We list the contact information for all authors below\.

- •Hojae Han, Electronics and Telecommunications Research Institute\.hojae\.han@etri\.re\.kr
- •Jongyoon Kim, Interdisciplinary Program in Artificial Intelligence, Seoul National University\.john\.jongyoon\.kim@snu\.ac\.kr
- •Sanghyuk Park, Department of Mathematical Sciences, Seoul National University\.202123018@snu\.ac\.kr
- •Dongwook Cheon, Department of Mathematical Sciences, Seoul National University\.dongwook0826@snu\.ac\.kr
- •Myungjae Jeon, Department of Mathematics, University of Maryland, College Park\.mjjeon@umd\.edu
- •Sunjong Choi, Department of Mathematical Sciences, Seoul National University\.sunjc@snu\.ac\.kr
- •Soonho Kong, Amazon Web Services\.soonho@amazon\.com
- •Wonseok Heo, Department of Computer Science and Engineering, Seoul National University\.hws0728jik@snu\.ac\.kr
- •Seung\-won Hwang, Department of Computer Science and Engineering, Seoul National University\.seungwonh@snu\.ac\.kr
- •Donghoon Hyeon, Department of Mathematical Sciences, Seoul National University\.dhyeon@snu\.ac\.kr