Pith. sign in

REVIEW 2 major objections 2 minor 75 references

Translating proofs to modular pseudo-formal blocks lets LLMs detect errors more reliably than direct assessment.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-30 17:14 UTC pith:QOTC7V2X

load-bearing objection The paper gives a workable middle format for breaking proofs into LLM-checkable natural-language blocks and releases a useful research benchmark, but the claimed gains over direct LLM judging rest on an untested translation step. the 2 major comments →

arxiv 2605.20531 v2 pith:QOTC7V2X submitted 2026-05-19 cs.LO cs.LG

Pseudo-Formalization for Automatic Proof Verification

Slim Barkallah , Luke Bailey , Kaiyue Wen , Mohammed Abouzaid , Tengyu Ma This is my paper
classification cs.LO cs.LG
keywords pseudo-formalizationblock verificationproof verificationLLM evaluationmathematical reasoningerror detectionnatural language proofs
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Pseudo-Formalization, a format that splits a proof into self-contained modules each listing its premises, conclusion, and natural language argument. An LLM converts the original proof into this format, then Block Verification checks the logical validity of each module on its own. This approach targets the difficulty of verifying complex mathematical reasoning produced by AI systems, where full formalization in strict languages remains impractical. Tests across olympiad problems and research-level mathematics show the combined method finds errors with better precision and recall than standard LLM judging. A new benchmark of research proofs is released to aid further development.

Core claim

Pseudo-Formalization decomposes a natural language proof into independent modules that each declare explicit premises and a conclusion while retaining natural language text for the argument, after which Block Verification has an LLM translate the original proof and assess every module separately for correctness.

What carries the argument

Block Verification, the procedure that translates a proof to pseudo-formal modules and then checks each module independently.

Load-bearing premise

The LLM translation from natural language to the pseudo-formal format preserves the original logical structure without adding or omitting errors.

What would settle it

A natural language proof containing a genuine logical error that the translation step either removes or alters so that Block Verification reports the proof as correct.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • PF+BV achieves higher error-finding precision and recall than LLM-as-judge baselines on both olympiad and research-level benchmarks.
  • Proof verification becomes possible for statements that resist complete formalization in languages such as Lean.
  • The released ArxivMathGradingBench supplies a standardized set of research-level proofs for evaluating verification systems.
  • Automated checks during AI training on advanced mathematics can operate at higher reliability without requiring full formal proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The modular format could support iterative human-AI refinement of proofs by allowing reviewers to focus on individual blocks.
  • Similar decomposition might apply to verification tasks outside mathematics, such as checking technical arguments in computer science or physics.
  • Training data consisting of pseudo-formal examples could improve future LLMs at producing verifiable reasoning steps.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 2 minor

Summary. The paper proposes Pseudo-Formalization (PF), a modular natural-language proof format consisting of self-contained blocks each stating premises, conclusion, and proof text. It introduces Block Verification (BV), an algorithm in which an LLM first translates a natural-language proof into PF modules and then verifies each module independently. The central claim is that PF+BV Pareto-dominates standard LLM-as-judge baselines on error-finding precision and recall across two benchmarks (olympiad and research-level mathematics), and the authors release the ArxivMathGradingBench benchmark to support further work.

Significance. If the evaluation results hold after methodological clarification, the work would provide a practical intermediate point between fully formal verification (e.g., Lean) and unstructured LLM judging, potentially easing verification of frontier AI-generated mathematics. The public release of ArxivMathGradingBench is a concrete, reusable contribution that directly benefits the community.

major comments (2)
  1. [Evaluation methodology / abstract claim] The headline Pareto-dominance result on precision and recall (abstract and evaluation section) is load-bearing on the untested assumption that the LLM translation step from natural language to Pseudo-Formal modules neither fabricates nor suppresses errors present in the original proof. No human audit, inter-annotator agreement score, or ablation that isolates translation fidelity from downstream verification accuracy is reported; without such evidence the reported metrics cannot be unambiguously attributed to the modular verification procedure rather than to rephrasing artifacts.
  2. [§3] §3 (Block Verification algorithm): the claim that independent per-module verification is sufficient presupposes that logical errors are strictly localized. The manuscript provides no analysis or counter-example discussion of cross-module dependencies (e.g., an erroneous premise in module i affecting the soundness of module j), which directly affects whether the reported error-finding gains are robust.
minor comments (2)
  1. [Abstract] The abstract refers to “two benchmarks” but names only ArxivMathGradingBench; explicitly identifying the olympiad benchmark (name, size, source) would improve readability.
  2. [§2] Notation for the Pseudo-Formal module components (premises, conclusion, proof text) is introduced informally; a small table or diagram in §2 would make the format easier to compare with existing semi-formal representations.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive and detailed comments. We address each major comment below and indicate the revisions we will make.

read point-by-point responses

  1. Referee: [Evaluation methodology / abstract claim] The headline Pareto-dominance result on precision and recall (abstract and evaluation section) is load-bearing on the untested assumption that the LLM translation step from natural language to Pseudo-Formal modules neither fabricates nor suppresses errors present in the original proof. No human audit, inter-annotator agreement score, or ablation that isolates translation fidelity from downstream verification accuracy is reported; without such evidence the reported metrics cannot be unambiguously attributed to the modular verification procedure rather than to rephrasing artifacts.

    Authors: We agree that the manuscript does not contain a direct human audit or ablation isolating the translation step, and that this leaves open the possibility that some measured gains could stem from rephrasing effects. The current evaluation reports end-to-end performance of the full PF+BV pipeline against baselines, which remains the practically relevant comparison. In the revision we will add a new subsection reporting a human audit on a random sample of 50 translated modules per benchmark, including inter-annotator agreement, to quantify any fabrication or suppression of errors during translation. revision: yes

  2. Referee: [§3] §3 (Block Verification algorithm): the claim that independent per-module verification is sufficient presupposes that logical errors are strictly localized. The manuscript provides no analysis or counter-example discussion of cross-module dependencies (e.g., an erroneous premise in module i affecting the soundness of module j), which directly affects whether the reported error-finding gains are robust.

    Authors: The PF format requires every module to list its premises explicitly and to be self-contained, so that verification checks whether the stated proof text entails the conclusion from precisely those premises. An erroneous premise is therefore detected inside its own module. When the conclusion of module i becomes a premise of module j, its correctness has already been verified in module i. We will expand the description in §3 with an explicit paragraph on this localization property together with a short counter-example discussion of a hypothetical dependency chain. revision: yes

Circularity Check

0 steps flagged

No significant circularity; evaluation uses external benchmarks

full rationale

The paper defines Pseudo-Formalization (PF) and Block Verification (BV) as a method, then evaluates PF+BV on two external benchmarks (olympiad and research-level) against LLM-as-judge baselines, reporting Pareto dominance on precision and recall. No equations, self-citations, or fitted parameters are shown reducing the central claim to an input by construction. The translation step is an unverified modeling assumption rather than a definitional loop or renamed fit. The derivation chain remains independent of the reported metrics.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The approach rests on the unverified assumption that LLM translation to the modular format is faithful; no free parameters or invented physical entities are involved.

axioms (1)
  • domain assumption LLMs can translate natural language proofs into self-contained Pseudo-Formal modules while preserving correctness and logical independence of blocks
    This assumption is required for Block Verification to function as an error-detection method.
invented entities (1)
  • Pseudo-Formal proof module no independent evidence
    purpose: Intermediate representation enabling modular natural language verification
    New concept introduced by the paper to bridge natural language and formal verification.

pith-pipeline@v0.9.1-grok · 5721 in / 1158 out tokens · 39587 ms · 2026-06-30T17:14:37.281837+00:00 · methodology

0 comments
read the original abstract

Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.

Figures

Figures reproduced from arXiv: 2605.20531 by Kaiyue Wen, Luke Bailey, Mohammed Abouzaid, Slim Barkallah, Tengyu Ma.

Figure 1
Figure 1. Figure 1: Left: Diagram indicating how Pseudo-Formalization can be used to verify proofs. We translate a natural language proof to Pseudo-Formal representation (Definition 1), and then verify each block (see [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: An example Pseudo-Formalized Proof on IMO 2024 P6. The block verifier correctly assigns Lemma 5.1 score 0 because the proof incorrectly strengthens P2 from Lemma 4.2 “S cannot contain both d and −d” to “all nonzero elements of S have the same sign”. 3.1 Step 1: Translation to Pseudo-Formal The translation LLM receives the natural-language proof Π, and is prompted to produce a Pseudo￾Formal proof Πˆ in the … view at source ↗
Figure 3
Figure 3. Figure 3: Per-proof/paper and per-error metrics on [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Precision-recall on Hard2Verify at the whole-proof label level (positive class: proof contains 1 or more incorrect steps). For each k, the verifier’s per-rollout proof-level verdicts are aggregated with pessimistic-min (the proof is pre￾dicted incorrect iff at least one 1 or more steps over the k rollouts is predicted incorrect). Quantitative Results [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

75 extracted references · 21 canonical work pages · 4 internal anchors

  1. [1]

    Learning to Give Checkable Answers with Prover-Verifier Games.arXiv:2108.12099 [cs.LG],

    Cem Anil, Guodong Zhang, Yuhuai Wu, and Roger Grosse. Learning to give checkable answers with prover-verifier games.arXiv preprint arXiv:2108.12099, 2021

    work page arXiv 2021

  2. [2]

    Towards a Lean proof of Fermat’s Last Theorem.https: //imperialcollegelondon.github.io/FLT/blueprint.pdf, 2024

    Kevin Buzzard and Richard Taylor. Towards a Lean proof of Fermat’s Last Theorem.https: //imperialcollegelondon.github.io/FLT/blueprint.pdf, 2024

    2024

  3. [3]

    Jiaqi Chen, Bang Zhang, Ruotian Ma, Peisong Wang, Xiaodan Liang, Zhaopeng Tu, Xiaolong Li, and Kwan-Yee K. Wong. Spc: Evolving self-play critic via adversarial games for llm reasoning.arXiv preprint arXiv:2504.19162, 2025

    work page arXiv 2025

  4. [4]

    Power-free palindromes and reversed primes: S

    Shashi Chourasiya and Daniel R Johnston. Power-free palindromes and reversed primes: S. chourasiya, dr johnston.Monatshefte für Mathematik, pages 1–17, 2025

    2025

  5. [5]

    Escaping the cognitive well: Efficient competition math with off-the-shelf models,

    Xingyu Dang, Rohit Agarwal, Rodrigo Porto, Anirudh Goyal, Liam H Fowl, and Sanjeev Arora. Escaping the cognitive well: Efficient competition math with off-the-shelf models,

  6. [6]

    URLhttps://arxiv.org/abs/2602.16793

    work page arXiv

  7. [7]

    The lean theorem prover (system description)

    Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). InInternational Conference on Automated Deduction, pages 378–388. Springer, 2015

    2015

  8. [8]

    Finite codimension stability of invariant surfaces.arXiv preprint arXiv:2502.00898, 2025

    Giovanni Forni. Finite codimension stability of invariant surfaces.arXiv preprint arXiv:2502.00898, 2025

    work page arXiv 2025

  9. [9]

    Llm critics help catch bugs in mathematics: Towards a better mathematical verifier with natural language feedback

    Bofei Gao, Zefan Cai, Runxin Xu, Peiyi Wang, Ce Zheng, Runji Lin, Keming Lu, Dayiheng Liu, Chang Zhou, Wen Xiao, Tianyu Liu, and Baobao Chang. Llm critics help catch bugs in mathematics: Towards a better mathematical verifier with natural language feedback. InFindings of the Association for Computational Linguistics: ACL 2025, pages 14588–14604. Associati...

    2025

  10. [10]

    Formal proof – theory and practice.Notices of the American Mathematical Society, 55:1395–1406, 2008

    John Harrison. Formal proof – theory and practice.Notices of the American Mathematical Society, 55:1395–1406, 2008

    2008

  11. [11]

    Context rot: How increasing input tokens impacts llm performance.URL https://research

    Kelly Hong, Anton Troynikov, and Jeff Huber. Context rot: How increasing input tokens impacts llm performance.URL https://research. trychroma. com/context-rot, retrieved October, 20: 2025, 2025

    2025

  12. [12]

    Pessimistic Verification for Open Ended Math Questions

    Yanxing Huang, Zihan Tang, Zejin Lin, Peng Li, and Yang Liu. Pessimistic verification for open ended math questions.arXiv preprint arXiv:2511.21522, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  13. [13]

    arXiv preprint arXiv:2507.15855 , year=

    Yichen Huang and Lin F Yang. Winning gold at imo 2025 with a model-agnostic verification- and-refinement pipeline.arXiv preprint arXiv:2507.15855, 2025

    work page arXiv 2025

  14. [14]

    Prover-Verifier Games improve legibility of LLM outputs.arXiv:2407.13692 [cs.CL],

    Jan Hendrik Kirchner, Yining Chen, Harri Edwards, Jan Leike, Nat McAleese, and Yuri Burda. Prover-verifier games improve legibility of llm outputs.arXiv preprint arXiv:2407.13692, 2024

    work page arXiv 2024

  15. [15]

    PrimeNumberTheoremAnd: A formalization of the prime number theorem and related results in Lean 4

    Alex Kontorovich and Terence Tao. PrimeNumberTheoremAnd: A formalization of the prime number theorem and related results in Lean 4. https://github.com/ AlexKontorovich/PrimeNumberTheoremAnd, 2024

    2024

  16. [16]

    Let’s verify step by step

    Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harri Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let’s verify step by step. In International Conference on Learning Representations, 2024. 12

    2024

  17. [17]

    https://arxiv.org/abs/2502.07640

    Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving.arXiv preprint arXiv:2502.07640, 2025

    work page arXiv 2025

  18. [18]

    Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

    Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.arXiv preprint arXiv:2508.03613, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  19. [19]

    Trust, but verify: A self-verification approach to reinforcement learning with verifiable rewards

    Xiaoyuan Liu, Tian Liang, Zhiwei He, Jiahao Xu, Wenxuan Wang, Pinjia He, Zhaopeng Tu, Haitao Mi, and Dong Yu. Trust, but verify: A self-verification approach to reinforcement learning with verifiable rewards. InProceedings of the 39th Conference on Neural Information Processing Systems (NeurIPS 2025), 2025

    2025

  20. [20]

    Towards robust mathematical reasoning

    Minh-Thang Luong, Dawsen Hwang, Hoang H Nguyen, Golnaz Ghiasi, Yuri Chervonyi, Insuk Seo, Junsu Kim, Garrett Bingham, Jonathan Lee, Swaroop Mishra, et al. Towards robust mathematical reasoning. InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pages 35406–35430, 2025

    2025

  21. [21]

    Scaling generative ver- ifiers for natural language mathematical proof verification and selection.arXiv preprint arXiv:2511.13027, 2025

    Sadegh Mahdavi, Branislav Kisacanin, Shubham Toshniwal, Wei Du, Ivan Moshkov, George Armstrong, Renjie Liao, Christos Thrampoulidis, and Igor Gitman. Scaling generative ver- ifiers for natural language mathematical proof verification and selection.arXiv preprint arXiv:2511.13027, 2025

    work page arXiv 2025

  22. [22]

    arXiv preprint arXiv:2310.07923 , year=

    William Merrill and Ashish Sabharwal. The expressive power of transformers with chain of thought.arXiv preprint arXiv:2310.07923, 2023

    work page arXiv 2023

  23. [23]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. InInternational Conference on Automated Deduction, pages 625–635. Springer, 2021

    2021

  24. [24]

    Springer, 2002

    Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson.Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002

    2002

  25. [25]

    Hard2verify: A step-level verification benchmark for open-ended frontier math.CoRR, abs/2510.13744, 2025

    Shrey Pandit, Austin Xu, Xuan-Phi Nguyen, Yifei Ming, Caiming Xiong, and Shafiq Joty. Hard2verify: A step-level verification benchmark for open-ended frontier math.arXiv preprint arXiv:2510.13744, 2025

    work page arXiv 2025

  26. [26]

    Real algebraic surfaces biholomorphically equivalent but not algebraically equivalent

    Guillaume Rond. Real algebraic surfaces biholomorphically equivalent but not algebraically equivalent.arXiv preprint arXiv:2503.08957, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  27. [27]

    Liquid tensor experiment.Experimental Mathematics, 31(2):349–354, 2022

    Peter Scholze. Liquid tensor experiment.Experimental Mathematics, 31(2):349–354, 2022

    2022

  28. [28]

    Deepseekmath-v2: Towards self-verifiable mathematical reasoning

    Zhihong Shao, Yuxiang Luo, Chengda Lu, ZZ Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, and Xiaokang Zhang. Deepseekmath-v2: Towards self-verifiable mathematical reasoning. arXiv preprint arXiv:2511.22570, 2025

    work page arXiv 2025

  29. [29]

    Heimdall: test-time scaling on the generative verification.arXiv preprint arXiv:2504.10337, 2025

    Wenlei Shi and Xing Jin. Heimdall: test-time scaling on the generative verification.arXiv preprint arXiv:2504.10337, 2025

    work page arXiv 2025

  30. [30]

    A promising path towards autoformalization and general artificial intelli- gence

    Christian Szegedy. A promising path towards autoformalization and general artificial intelli- gence. InInternational Conference on Intelligent Computer Mathematics, pages 3–20. Springer, 2020

    2020

  31. [31]

    From solving to verifying: A unified objective for robust reasoning in llms, 2025

    Xiaoxuan Wang, Bo Liu, Song Jiang, Jingzhou Liu, Jingyuan Qi, Xia Chen, and Baosheng He. From solving to verifying: A unified objective for robust reasoning in llms, 2025. URL https://arxiv.org/abs/2511.15137. 13

    work page arXiv 2025

  32. [32]

    Autoformalization with large language models.Advances in neural information processing systems, 35:32353–32368, 2022

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models.Advances in neural information processing systems, 35:32353–32368, 2022

    2022

  33. [33]

    arXiv preprint arXiv:2503.14337 , year=

    Chenxiao Yang, Nathan Srebro, David McAllester, and Zhiyuan Li. Pencil: Long thoughts with short memory, 2025. URLhttps://arxiv.org/abs/2503.14337

    work page arXiv 2025

  34. [34]

    Recursive models for long-horizon reasoning

    Chenxiao Yang, Nathan Srebro, and Zhiyuan Li. Recursive models for long-horizon reasoning. arXiv preprint arXiv:2603.02112, 2026

    work page internal anchor Pith review arXiv 2026

  35. [35]

    Loca-bench: Benchmarking language agents under controllable and extreme context growth.arXiv preprint arXiv:2602.07962, 2026

    Weihao Zeng, Yuzhen Huang, and Junxian He. Loca-bench: Benchmarking language agents under controllable and extreme context growth.arXiv preprint arXiv:2602.07962, 2026

    work page arXiv 2026

  36. [36]

    arXiv preprint arXiv:2408.15240 , year=

    Lunjun Zhang, Arian Hosseini, Hritik Bansal, Mehran Kazemi, Aviral Kumar, and Rishabh Agarwal. Generative verifiers: Reward modeling as next-token prediction. InProceedings of the International Conference on Learning Representations (ICLR), 2025. URL https://arxiv. org/abs/2408.15240

    work page arXiv 2025

  37. [37]

    Sample, scrutinize and scale: Effective inference-time search by scaling verification.arXiv preprint arXiv:2502.01839, 2025

    Eric Zhao, Pranjal Awasthi, and Sreenivas Gollapudi. Sample, scrutinize and scale: Effective inference-time search by scaling verification.arXiv preprint arXiv:2502.01839, 2025

    work page arXiv 2025

  38. [38]

    Processbench: Identifying process errors in mathematical reasoning

    Chujie Zheng, Zhenru Zhang, Beichen Zhang, Runji Lin, Keming Lu, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. Processbench: Identifying process errors in mathematical reasoning. InThe 63rd Annual Meeting of the Association for Computational Linguistics, 2025

    2025

  39. [39]

    Leanarchitect: Automating blueprint generation for humans and ai, 2026

    Thomas Zhu, Pietro Monticone, Jeremy Avigad, and Sean Welleck. Leanarchitect: Automating blueprint generation for humans and ai, 2026. URL https://arxiv.org/abs/2601. 22554. 14 A Context cost of verification: formal statement and proof Definition 2(Good Pseudo-Formal proof).Agood Pseudo-Formal proofis a Pseudo-Formal proof (Definition 1) with the followin...

    2026

  40. [40]

    The depth of T is D<n

  41. [41]

    Definition 3(Block-wise verification algorithm).Let P= (G , T) be a Pseudo-Formal proof with node set V={v 1,

    The lengths of the conclusion c, the premises, and the proof are bounded above by L. Definition 3(Block-wise verification algorithm).Let P= (G , T) be a Pseudo-Formal proof with node set V={v 1, . . . ,vn}, where each node is written as v= (P v,c v,π v). For a node v∈V , let AncT(v) denote its ancestors in the scope-inheritance forest T, and define its de...

    2026

  42. [42]

    1"> Assumptions / Conditions / Definitions. - ... Statement : ... </PROPOSITION_STATEMENT> <LEMMA_STATEMENT id=

    Lemmas - Do not introduce any deeper hierarchy. - If a deeper tree seems natural, flatten it into a sequential list of lemmas inside the relevant proposition. - The theorem proof may only cite propositions; a proposition proof may only cite its own lemmas and the statements of earlier propositions. - No trivial decompositions: do not decompose the theorem...

  43. [43]

    These are often the parent or ancestor statements of the Assertion, and can be the same as the global theorem

    **Contexts**: A sequence of statements from which the Assertion may or may not inherit definitions, assumptions, or conditions. These are often the parent or ancestor statements of the Assertion, and can be the same as the global theorem. They are provided solely so you can understand the definitions and assumptions of the Assertion. They have NOT been ve...

  44. [44]

    You may assume all established results are correct and use them freely - do NOT re-verify them

    **Established Results **: Statements that have already been verified or can be assumed to be correct. You may assume all established results are correct and use them freely - do NOT re-verify them. The proof of the Assertion can invoke these results as long as the assumptions are properly justified and the definitions are consistent

  45. [45]

    **Assertion**: The specific statement whose proof you must verify

  46. [46]

    verdict":

    **Proposed Proof **: The proof of the Assertion to verify. Instructions: - Verify ONLY the proposed proof of the Assertion. - Read the Assertion carefully and analyze the proof step by step. - Identify any incorrect, unjustified, or logically invalid reasoning. - Pay close attention to potentially confusing or ambiguous interpretations of concepts. - When...

  47. [47]

    Math Problem: The original problem statement. 20

  48. [48]

    Original Solution Steps: The solver’s original solution split into indexed steps, written as: <step>[0] ...</step> <step>[1] ...</step> and so on

  49. [49]

    This rewrite was produced automatically and may contain artifacts that are not present in the original solution

    Rewritten Proof: A structured rewrite of the original solution, decomposed into theorem / proposition / lemma / claim / fact blocks. This rewrite was produced automatically and may contain artifacts that are not present in the original solution

  50. [50]

    These may or may not be genuine errors in the original solution

    Potential Errors: A list of potential errors flagged by automated verification of the rewritten proof. These may or may not be genuine errors in the original solution. Evaluation process:

  51. [51]

    For each flagged issue, decide whether it is a genuine mathematical error in the ORIGINAL solution or a false alarm caused by the rewrite

    Validate each potential error. For each flagged issue, decide whether it is a genuine mathematical error in the ORIGINAL solution or a false alarm caused by the rewrite. Cross-check against the original solution steps. If the original solution contains the missing reasoning, a stronger equivalent argument, or a correct alternative route, do not count the ...

  52. [52]

    The potential errors are useful leads, but your final output must be based on the original solution steps

    Inspect the original steps as needed. The potential errors are useful leads, but your final output must be based on the original solution steps. Check any original steps needed to identify the first genuine incorrect step. If you find that the first incorrect step was not covered by any potential error, report it in <additional_errors>

  53. [53]

    For each original step, determine whether that step is correct or incorrect

    Grade the original steps, not the rewrite. For each original step, determine whether that step is correct or incorrect. - A correct step is one where all mathematical content is correct and logically consistent with the problem and all previous correct steps. - An incorrect step is one that contains a mathematical error, an unjustified load- bearing claim...

  54. [54]

    corrected typos in the proof of Theorem 3

    Identify the first incorrect step. The first incorrect step is the smallest original step index whose content is mathematically incorrect or whose reasoning first depends on an error. If every original step is correct, output -1. Important calibration rules: - The original solution steps are authoritative for the final verdict. - The rewritten proof and p...

    2025

  55. [55]

    Use this to read the paper as a human reader would, with all theorem/lemma/proposition numbers rendered

    The rendered PDF (attached as a file). Use this to read the paper as a human reader would, with all theorem/lemma/proposition numbers rendered

  56. [56]

    Theorem 19

    The raw LaTeX source (included below). Use this to inspect precise notation, equations, and label names if needed. Your task is to identify any mathematical errors in the paper that would require revision before publication. Focus on errors of mathematical substance: incorrect proofs, unjustified steps, false claims, gaps in reasoning, miscomputed quantit...

  57. [57]

    Use it to read the paper as a human would and to identify the rendered numerical or letter labels of every theorem/lemma/proposition/corollary/claim

    The rendered PDF of the paper (attached as a file). Use it to read the paper as a human would and to identify the rendered numerical or letter labels of every theorem/lemma/proposition/corollary/claim

  58. [58]

    Use it to inspect precise notation, equations, and the exact wording of each statement and proof

    The raw LaTeX source of the paper (included below). Use it to inspect precise notation, equations, and the exact wording of each statement and proof. Structure: - The top level of the rewrite is a list of **theorems**. Use one <THEOREM_STATEMENT id="N"> block per top-level result the paper proves. Top-level results are the paper’s flagship theorem(s) plus...

  59. [59]

    Propositions (shared pool, numbered globally across all theorems)

  60. [60]

    N"> may cite any of the propositions; a <PROPOSITION_PROOF id=

    Lemmas (numbered within each proposition) - Do not introduce any deeper hierarchy. If a deeper tree seems natural, flatten it into a sequential list of lemmas inside the relevant proposition. - Each <THEOREM_PROOF id="N"> may cite any of the propositions; a <PROPOSITION_PROOF id="K"> may cite its own lemmas and the statements of earlier propositions. A th...

  61. [61]

    The rendered PDF of the original paper (attached as a file)

  62. [62]

    The raw LaTeX source of the paper (included below -- ground truth -- your rewrite must faithfully represent this)

  63. [63]

    Your previous rewritten paper, which contained faithfulness errors

  64. [64]

    Requirements for the new rewrite: - Fix every issue listed in the Identified Errors

    The specific discrepancies flagged by the checker. Requirements for the new rewrite: - Fix every issue listed in the Identified Errors. For each issue, make sure the new rewrite no longer deviates from the original paper in that way. - Do NOT introduce new discrepancies: do not strengthen/weaken claims, omit steps, add arguments, drift in notation, or mis...

  65. [65]

    **Original Paper (LaTeX) **: The full LaTeX source of the original paper

  66. [66]

    These are provided so you can understand the scope of the Assertion

    **Contexts**: Statements from the rewritten paper that the Assertion inherits definitions or assumptions from (e.g., the enclosing theorem statement, the enclosing proposition statement). These are provided so you can understand the scope of the Assertion

  67. [67]

    You may use them as reference points

    **Established Results **: Statements from the rewritten paper that have already been checked and can be assumed to be faithfully rewritten. You may use them as reference points. 28

  68. [68]

    **Assertion**: The specific rewritten statement whose faithfulness you must verify

  69. [69]

    Your task is to determine whether the Assertion and its Proposed Proof **faithfully represent** the corresponding part of the Original Paper

    **Proposed Proof **: The rewritten proof of the Assertion (may be empty for a top- level theorem statement). Your task is to determine whether the Assertion and its Proposed Proof **faithfully represent** the corresponding part of the Original Paper. Check for:

  70. [70]

    **Strengthened or weakened claims **: Does the Assertion claim more or less than the original paper establishes at the corresponding point?

  71. [71]

    **Omitted content **: Does the Proposed Proof drop a non-trivial argument that appears in the original paper?

  72. [72]

    **Added content **: Does the Proposed Proof introduce new arguments, repairs, or proof ideas not present in the original paper?

  73. [73]

    **Notation drift **: Are variables, functions, or definitions used differently than in the original paper?

  74. [74]

    **Misinterpretation**: Does the Assertion or Proposed Proof misunderstand the original’s reasoning or logical structure?

  75. [75]

    verdict":

    **Scope errors **: Are assumptions incorrectly inherited, dropped, or added compared to the original? Instructions: - Do NOT judge whether the original paper is mathematically correct. Your sole task is faithfulness. - Only flag changes that alter mathematical meaning. Cosmetic rephrasing is fine. - Use the Contexts to understand what the Assertion is all...