Pith. sign in

REVIEW 4 major objections 5 minor 5 cited by

Aria is claimed to be the first agent that can auto-formalize research-level conjectures in Lean by synthesizing new definitions, reaching 42.9% on homological conjectures where all baselines score 0%.

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 · deepseek-v4-flash

2026-08-04 11:28 UTC pith:CJBKL6XI

load-bearing objection A genuinely new GoT-based definition synthesis pipeline with a plausible but under-verified semantic checker; the Conjectures result is credible, the comparative margins are not yet established. the 4 major comments →

arxiv 2510.04520 v2 pith:CJBKL6XI submitted 2025-10-06 cs.AI

Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph

Hanyu Wang , Ruohan Xie , Yutong Wang , Guoxiong Gao , Xintao Yu , Bin Dong This is my paper
classification cs.AI
keywords auto-formalizationLeanMathlibdependency graphretrieval-augmented generationsemantic checkingconjecture formalizationgraph-of-thought
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 claims that auto-formalizing research-level mathematical statements, long a bottleneck for automated mathematics, can be solved by an agent that decomposes a statement into a dependency graph of concepts, grounds known concepts in the Lean math library, synthesizes missing definitions bottom-up with compiler feedback, and verifies semantic fidelity with a term-grounded checker. On a dataset of homological conjectures, this agent reaches 42.9% final accuracy while every baseline scores 0%, and it surpasses prior systems on ProofNet, FATE-H, and FATE-X. A sympathetic reader would take the central contribution to be the demonstrated capability to autonomously create the novel definitions that conjecture-level statements require. If the claim holds, future theorem provers would gain a supply of correctly typed conjecture statements to attack, removing a key obstacle to automated mathematical discovery.

Core claim

The paper's central claim is that Aria is the first agent capable of autonomously synthesizing the complex novel definitions required to formalize high-difficulty mathematical statements such as conjectures. Concretely, on a set of 14 real homological conjectures, Aria achieves 42.9% final accuracy — passing both compilation and the paper's semantic checker — while all baseline models score 0%; on ProofNet it reaches 68.5% final accuracy with a 91.6% compilation rate, and on FATE-X it outscores the best baseline 44.0% to 24.0%. The authors attribute this to the two-phase Graph-of-Thought pipeline and to AriaScorer's term-level grounding, which lets the checker detect semantic mismatches that

What carries the argument

The load-bearing mechanism is a two-phase Graph-of-Thought planner. In the decomposition phase, the agent recursively expands an informal statement into a dependency graph of concept nodes, using a retrieval engine to ground each node in the current Lean math library; ungrounded nodes become internal nodes marked for synthesis. In the synthesis phase, the agent builds formal definitions bottom-up, each validated by the Lean compiler in a reflection loop that feeds error messages back to the model. A companion checker, AriaScorer, retrieves the authoritative library definition of every Lean term and passes it to an LLM judge, enabling detection of subtle discrepancies such as reversed paramet

Load-bearing premise

The comparative results rest on the assumption that AriaScorer — whose threshold and validation ground truth were both derived from Aria's own outputs on FATE-X — is a fair, calibration-invariant arbiter when applied to every baseline, even though its calibration on non-Aria outputs is never tested.

What would settle it

Have a human expert re-annotate a random sample of Aria's FATE-X and homological-conjecture formalizations, blind to which system produced them, and compare the expert labels against AriaScorer's True/False decisions; if AriaScorer systematically over-approves Aria's outputs relative to baselines, the headline accuracy gap could shrink or vanish.

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

Share X Bluesky LinkedIn Reddit HN

If this is right

  • Aria's stated success on conjecture-level statements provides a practical path to turning research mathematics into formally stated theorems in Lean, which automated provers can then target.
  • The ablation results imply that the agent's capability depends on all three components — retrieval, decomposition, and reflection — since removing any one collapses performance on the hardest dataset.
  • AriaScorer's term-grounded checking offers a reusable evaluation method for auto-formalization that is less dependent on surface textual similarity.
  • If the conjecture-formalization capability is real, it would enable large-scale creation of formal conjecture statements, potentially accelerating data-generation pipelines for training future theorem-proving systems.
  • The finding that Aria maintains higher final accuracy than a baseline given more than seven times the compute suggests the architecture, not compute per question, is the decisive factor.

Where Pith is reading between the lines

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

  • Aria's success likely hinges on the reasoning strength of the underlying LLM; the paper does not test whether the Graph-of-Thought scaffolding transfers to weaker base models, so the method's generality remains an open question.
  • The dependency-graph decomposition appears conceptually portable to other interactive theorem provers such as Isabelle or Coq, but the paper only evaluates Lean, so cross-system transfer is untested.
  • AriaScorer's design suggests a broader pattern for LLM evaluation: injecting authoritative definitions into prompts can suppress hallucinations in semantic judgments beyond formalization, a direction the paper leaves implicit.
  • Because the evaluation benchmarks are small and domain-specific, the reported 42.9% on conjectures may understate variance; a larger sample of conjectures from diverse fields would be needed to confirm the capability is general.

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

4 major / 5 minor

Summary. The paper introduces Aria, an LLM-based agent for auto-formalizing informal mathematical statements into Lean 4. Aria uses a Graph-of-Thought planner to decompose a statement into a conceptual dependency graph, grounds concepts via LeanSearch/Mathlib retrieval, synthesizes missing definitions bottom-up, and iteratively fixes compilation errors with compiler feedback. The paper also introduces AriaScorer, a semantic checker that decomposes informal/formal statements into subtasks and uses retrieved Lean term definitions to judge semantic fidelity. Experiments report 91.6% compilation / 68.5% final accuracy on ProofNet, 71.0% on FATE-H, 44.0% on FATE-X, and 42.9% on a 14-problem homological-conjecture set, with all baselines scoring 0% on the conjectures. The central capability claim is that Aria is the first agent that can autonomously synthesize the novel definitions needed to formalize research-level conjecture statements.

Significance. If the quantitative claims hold, this is a meaningful advance: statement auto-formalization at conjecture level is widely recognized as a bottleneck, and the paper's combination of dependency-graph decomposition, retrieval, and compiler-in-the-loop synthesis is a plausible and useful architecture. The manuscript has real strengths: compilation success is machine-checked; the Conjectures results are manually verified; the Appendix case studies give concrete, inspectable examples of Aria synthesizing definitions such as IsSystemOfParameters and correctly rejecting a QuaternionAlgebra mismatch; and the ablations isolate the contributions of reflection, GoT, and RAG. The main value of the paper, however, rests on the AriaScorer-based final-accuracy numbers, and those numbers are not yet established as fair and calibration-invariant across all systems being compared.

major comments (4)
  1. [§4.3.1, §4.3.2, Table 2] The central comparative claims—68.5% on ProofNet, 71.0% on FATE-H, 44.0% on FATE-X—are all computed with AriaScorer at α=0.9, but AriaScorer's validation and threshold selection are both performed on the same FATE-X benchmark that is later scored with that threshold. §4.3.1 states that the ground-truth evaluation set is built from "the Aria agent's syntactically correct, auto-formalized outputs" on FATE-X, and §4.3.2 says "we adopt the high-precision setting of α=0.9 in all other experiments." Thus the headline FATE-X number is an in-sample selection result, not a held-out evaluation, and the threshold has never been validated on ProofNet or FATE-H. The reported margins over baselines are therefore not self-contained. The authors should either fix α before evaluation on an independent validation set, or report final accuracies under multiple thresholds together with human verification on
  2. [§4.3.1, §4.3.2, Table 1] AriaScorer is only tested on Aria's own output distribution (69 labeled statements in Table 2). There is no evidence of its precision/recall on outputs produced by Goedel-V2, Gemini-2.5-Pro, Kimina, or Herald. Since AriaScorer's design, term-grounding context, and tuning examples all come from Aria's distribution, it may systematically disagree on baseline outputs—e.g., by being more permissive of Aria's style or more strict with different naming conventions. This is load-bearing for the comparative SOTA claim, not just for the absolute accuracy of Aria. A concrete fix is to build a human-labeled ground-truth set from each baseline's outputs and report AriaScorer's confusion matrix per baseline, or at minimum to have an expert manually verify a random sample of accepted and rejected outputs for every system.
  3. [§3.2.1, Figure 2] The scoring mechanism of AriaScorer is underspecified. The text says subtasks are labeled Perfectly Match, Minor Inconsistency, or Major Inconsistency, then "aggregated via a fuzzy integral into a final score between 0 and 1," with an unspecified decay for accumulating minor inconsistencies; Figure 2 mentions "Sugeno" without giving the integral or the decay function. Because the threshold α=0.9 is applied to this score and all final accuracies depend on that threshold, the missing functional form prevents independent reproduction of the checker. The authors should provide the exact aggregation formula, the number of subtasks, and the procedure for mapping labels to scores.
  4. [§4.1.1, §4.3.1] The FATE-H and FATE-X benchmarks are cited to a blog post from the authors' own group rather than a versioned, citable dataset. The paper does not report the number of problems, the exact problem set, the selection criteria, or a release URL. Since two of the four benchmarks and the only AriaScorer validation set come from this resource, the manuscript should include full dataset specifications, versioning, and access information, or the claims should be restricted to the released subsets.
minor comments (5)
  1. [§4.3.2, Table 2] At α=0 the proposed checker has accuracy 89.9% and F1 93.5%, while at α=0.9 accuracy drops to 82.6% and F1 to 87.5%. The paper should explain the operational cost asymmetry that justifies choosing the lower-accuracy, lower-F1 operating point for 'all other experiments.'
  2. [§4.2, Table 1] The comparison mixes evaluation budgets: Aria uses an average of 17.7 calls per problem, while Goedel-V2 is reported at pass@1/pass@16/.../pass@128. The paper should state whether pass@k means k independent samples per problem and should report Aria's pass@1 or pass@k equivalent to make the efficiency comparison precise.
  3. [§4.3.1] The ground-truth annotation process is described as two independent experts, but no inter-annotator agreement statistic or full annotation set is provided. Inclusion of the labeled data or a confusion count per expert would strengthen confidence in the checker comparison.
  4. [Appendix C, Table 4] Typo: 'cripped' should be 'crippled' in the ablation discussion. Also, the FATE-X without-GoT row is reported as 69.0% compiler and 38.0% final accuracy in the table but as 44.0→38.0 in the text; please reconcile the presentation.
  5. [Abstract, §4.1.2] The paper should clarify whether 'final accuracy' for the Conjectures dataset is computed manually for all models or only for Aria; Table 1 says 'manually verified' but the verification protocol for the baselines is not described.

Circularity Check

1 steps flagged

Headline benchmark numbers are scored by a checker threshold-tuned on Aria's own FATE-X outputs; the conjecture-formalization capability claim itself is manually verified and independent.

specific steps
  1. fitted input called prediction [§4.3.1–§4.3.2, Table 1, Table 2]
    ""The evaluation used the Aria agent's syntactically correct, auto-formalized outputs." (§4.3.1) "While we adopt the high-precision setting of α=0.9 in all other experiments" (§4.3.2) "the stricter Final accuracy (passing both compilation and our AriaScorer semantic check)" (Table 1 caption)."

    AriaScorer is the arbiter of every reported final accuracy. Its threshold α=0.9 was selected on the same FATE-X benchmark where Aria's 44.0% headline is reported, and its validation ground truth was built exclusively from Aria's own FATE-X outputs. Thus the numerical advantages over Goedel-V2/Gemini/Kimina/Herald are measured with a criterion calibrated on the distribution of the system being scored; no calibration or error analysis is reported for baseline outputs. The 42.9% Conjectures result is manually verified and the Appendix A case studies are type-checked, so the core capability claim does not reduce to the checker; only the comparative benchmark numbers are partly self-validated.

full rationale

I walked the derivation chain. The central capability claim—that Aria can synthesize novel definitions for conjecture-level statements—does not reduce to the paper's checker: the Conjectures result (42.9%) is explicitly manually verified (Table 1 note), Appendix A gives type-checked case studies, and the ablations isolate GoT/RAG/Reflection contributions. That part is self-contained and not circular. The problem is the comparative numerical claims on ProofNet/FATE-H/FATE-X. Final accuracy is defined by the paper as passing 'our AriaScorer semantic check' (Table 1 caption), and AriaScorer's threshold α=0.9 was chosen on the FATE-X outputs of Aria itself (§4.3.2), with validation ground truth also drawn from Aria's FATE-X outputs (§4.3.1). The same threshold is then used to score all baselines, with no reported calibration on baseline outputs. So the benchmark margins are partly an in-family evaluation: the measuring instrument was fitted on the distribution of the measured system. I do not call this a full 6+ because the 44.0% number is not forced by construction—outputs still must compile and satisfy the checker—and the strongest capability claim has independent manual/type-checked support. The FATE benchmarks are also from the same research group's blog, which compounds the provenance concern but is not by itself circular. Score 4 reflects partial circularity in the quantitative evaluation, not in the method's derivation.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 3 invented entities

The central claim rests on roughly three hand-set parameters (α threshold, reflection budget, score-decay shape) and five domain assumptions about decomposition completeness, corpus authoritativeness, decomposition fidelity, LLM selection reliability, and the adequacy of `sorry`-statements as evaluation objects. No new physical or mathematical entities are postulated; the novel artifacts are software (Aria, AriaScorer, dependency graph) and synthesized Lean definitions whose main independent evidence is that they type-check and are auditable. The most consequential hidden input is the α=0.9 threshold: the paper's own checker is the metric behind every reported final accuracy, and that threshold was selected on the very benchmark it is then used to score.

free parameters (3)
  • AriaScorer decision threshold α = 0.9
    Tuned on FATE-X (§4.3.2: 'we adopt the high-precision setting of α=0.9 in all other experiments') yet applied to report Aria's own FATE-X final accuracy of 44.0%; all reported final accuracies use this threshold.
  • Reflection attempt budget = 16
    Maximum compiler-feedback refinement iterations per node (§C.1); ablating it drops FATE-X final accuracy from 44% to 14% and Conjectures from 42.9% to 0%, so the headline results depend on this hand-chosen budget.
  • AriaScorer minor-inconsistency decay (unspecified functional form) = not stated
    Score 'decays gradually from 1 with accumulating minor inconsistencies' (§3.2.1) via a Sugeno fuzzy integral; the exact decay shape determines which borderline outputs pass at α=0.9 and is never specified.
axioms (5)
  • domain assumption Any concept, no matter how complex, can be defined solely in terms of its immediate prerequisite concepts.
    §3.1.1, the founding principle of the GoT decomposition; if a concept's prerequisite set is incomplete or the wrong canonical definition is chosen, the synthesized Lean definition silently changes meaning.
  • domain assumption Retrieved Mathlib term information (Herald informal descriptions) is the authoritative semantics of the formal terms.
    §3.2.2: AriaScorer 'queries the curated informalized Mathlib dataset established in Herald' and treats it as ground truth; checker correctness depends on this corpus being current and accurate.
  • domain assumption Subtask decomposition with fuzzy-integral aggregation faithfully measures informal/formal semantic fidelity.
    §3.2.1: AriaScorer inherits LeanScorer's subtask decomposition and aggregation; a statement with a mis-decomposed subtask list can be scored wrongly.
  • domain assumption The LLM reasoner reliably picks the canonical Mathlib candidate from LeanSearch retrieval results.
    §3.1.1: 'the agent employs an LLM as a sophisticated reasoner to analyze the retrieved candidates'; grounding quality (hence compilation success) depends on this selection being correct at every node.
  • domain assumption A type-checked statement with `sorry` is a valid object for semantic comparison.
    All generated outputs end in `sorry` (appendix examples); the compiler verifies only type-correctness, leaving semantic fidelity entirely to AriaScorer or human judgment.
invented entities (3)
  • AriaScorer no independent evidence
    purpose: Semantic correctness checker scoring every 'final accuracy' in the paper's headline results.
    Internal validator introduced by this paper; its only external check is the authors' expert-annotated ground-truth set built from Aria's own FATE-X outputs (§4.3.1), and it is used to score both Aria and all baselines rather than being tested on non-Aria output distributions.
  • Conceptual dependency graph (GoT working memory) no independent evidence
    purpose: Drives decomposition and bottom-up synthesis of definitions that are absent from Mathlib.
    Internal data structure of the Aria agent (§3.1.1); there is no isolated evidence of its correctness other than downstream formalization results and the ablation showing that removing it drops Conjectures success from 6/14 to 1/14.
  • Synthesized Mathlib definitions (e.g., IsSystemOfParameters, IsNoetherianLocalRing, IsNil, kleinianSingularityIdeal) independent evidence
    purpose: New Lean definitions created by the agent to formalize concepts missing from Mathlib.
    Unlike the system internals, these outputs have a falsifiable handle: they type-check in Lean and are human-auditable in Appendices A and B against the informal statements; the quaternion-algebra case shows the checker (and readers) can catch when a synthesized statement mismatches the intended meaning.

pith-pipeline@v1.3.0-alltime-deepseek · 20769 in / 24002 out tokens · 180028 ms · 2026-08-04T11:28:05.203969+00:00 · methodology

0 comments
Cite this review

Pith. "Pith review of Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph." pith.science (2026). https://pith.science/paper/CJBKL6XI

@misc{pith2026251004520,
  author       = {Pith},
  title        = {Pith review of: Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CJBKL6XI}},
  note         = {Machine review of arXiv:2510.04520}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Accurate auto-formalization of theorem statements is essential for advancing automated discovery and verification of research-level mathematics, yet remains a major bottleneck for LLMs due to hallucinations, semantic mismatches, and their inability to synthesize new definitions. To tackle these issues, we present Aria (Agent for Retrieval and Iterative Autoformalization), a system for conjecture-level formalization in Lean that emulates human expert reasoning via a two-phase Graph-of-Thought process: recursively decomposing statements into a dependency graph and then constructing formalizations from grounded concepts. To ensure semantic correctness, we introduce AriaScorer, a checker that retrieves definitions from Mathlib for term-level grounding, enabling rigorous and reliable verification. We evaluate Aria on diverse benchmarks. On ProofNet, it achieves 91.6% compilation success rate and 68.5% final accuracy, surpassing previous methods. On FATE-X, a suite of challenging algebra problems from research literature, it outperforms the best baseline with 44.0% vs. 24.0% final accuracy. On a dataset of homological conjectures, Aria reaches 42.9% final accuracy while all other models score 0%.

Figures

Figures reproduced from arXiv: 2510.04520 by Bin Dong, Guoxiong Gao, Hanyu Wang, Ruohan Xie, Xintao Yu, Yutong Wang.

Figure 1
Figure 1. Figure 1: The overall pipeline of Aria system. (A) [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The overall pipeline of AriaScorer: informal statements are decomposed into subtasks, [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Dependency Graph of Koethe’s Conjecture ARIA GENERATED STATEMENT import Mathlib universe u /-- An ideal `I` is a nil ideal if every element of `I` is nilpotent. -/ def IsNil {R : Type u} [Semiring R] (I : Ideal R) : Prop := ∀ x ∈ I, IsNilpotent x /-- If a ring `R` has no non-zero nil two-sided ideals, then it has no non-zero nil one-sided ideals (neither left nor right). -/ theorem no_nil_ideals_implies_no… view at source ↗
Figure 4
Figure 4. Figure 4: Dependency Graph of Existence of Balanced Big Cohen–Macaulay Modules Conjecture [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗

discussion (0)

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

Forward citations

Cited by 5 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. MathAtlas: A Benchmark for Autoformalization in the Wild

    cs.AI 2026-05 accept novelty 8.0

    MathAtlas is the first large-scale benchmark for autoformalizing graduate mathematics, where even strong models reach only 9.8% correctness on theorem statements and drop to 2.6% on the hardest dependency-deep subset.

  2. FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

    cs.CL 2026-07 conditional novelty 7.0

    FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.

  3. Automated Conjecture Resolution with Formal Verification

    cs.LG 2026-04 accept novelty 7.0 full

    Rethlas+Archon automatically construct and Lean-verify a counterexample showing weak quasi-completeness does not imply quasi-completeness for Noetherian local rings.

  4. Automated Conjecture Resolution with Formal Verification

    cs.LG 2026-04 unverdicted novelty 6.0

    An AI framework combining informal reasoning and formal verification resolves an open commutative algebra problem and produces a Lean 4-checked proof with minimal human input.

  5. AI for Mathematics: Progress, Challenges, and Prospects

    math.HO 2026-01 unverdicted novelty 4.0

    AI for math combines task-specific architectures and general foundation models to support research and advance AI reasoning capabilities.

Reference graph

Works this paper leans on

31 extracted references · 14 linked inside Pith · cited by 4 Pith papers

  1. [1]

    Proofnet: Autoformalizing and formally proving undergraduate-level mathematics

    Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W Ayers, Dragomir Radev, and Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. arXiv preprint arXiv:2302.12433, 2023

    Pith/arXiv arXiv 2023

  2. [2]

    The Coq proof assistant reference manual

    Bruno Barras, Samuel Boutin, Cristina Cornes, Judica \"e l Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filli \^a tre, Eduardo Gim \'e nez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, 1999

    1999

  3. [3]

    Seed- Prover : Deep and Broad Reasoning for Automated Theorem Proving , August 2025

    Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zha...

    Pith/arXiv arXiv 2025

  4. [4]

    A semantic search engine for mathlib4, 2024 a

    Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong. A semantic search engine for mathlib4, 2024 a . URL https://arxiv.org/abs/2403.13310

    Pith/arXiv arXiv 2024

  5. [5]

    Herald: A natural language annotated lean 4 dataset

    Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. arXiv preprint arXiv:2410.10878, 2024 b

    Pith/arXiv arXiv 2024

  6. [6]

    Gemini 2.5 pro

    Google DeepMind . Gemini 2.5 pro. https://deepmind.google/technologies/gemini/pro/, 2025

    2025

  7. [7]

    Formarl: Enhancing autoformalization with no labeled data

    Yanxing Huang, Xinling Jin, Sijie Liang, Peng Li, and Yang Liu. Formarl: Enhancing autoformalization with no labeled data. arXiv preprint arXiv:2508.18914, 2025

    Pith/arXiv arXiv 2025

  8. [8]

    Multilingual mathematical autoformalization

    Albert Q Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. arXiv preprint arXiv:2311.03755, 2023

    Pith/arXiv arXiv 2023

  9. [9]

    Introducing fate: A multi-level formal benchmark for frontier algebraic problems

    Jiedong Jiang, Wanyi He, Yuefeng Wang, Guoxiong Gao, Peihao Wu, Bryan Dai, and Bin Dong. Introducing fate: A multi-level formal benchmark for frontier algebraic problems. https://frenzymath.com/blog/fate/, Aug 2025

    2025

  10. [10]

    Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction, 2025. URL ht...

    Pith/arXiv arXiv 2025

  11. [11]

    Rethinking and improving autoformalization: Towards a faithful metric and a dependency retrieval-based approach

    Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: Towards a faithful metric and a dependency retrieval-based approach. In The Thirteenth International Conference on Learning Representations, 2025 a . URL https://openreview.net/forum?id=hUb2At2DsQ

    2025

  12. [12]

    Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data

    Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yuntian Liu, Yu Chen, Yang Jiao, and Tao Luo. Atlas: Autoformalizing theorems through lifting, augmentation, and synthesis of data. arXiv preprint arXiv:2502.05567, 2025 b

    arXiv 2025

  13. [13]

    Process-driven autoformalization in lean 4

    Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. Process-driven autoformalization in lean 4. arXiv preprint arXiv:2406.01940, 2024

    Pith/arXiv arXiv 2024

  14. [14]

    Automated formalization via conceptual retrieval-augmented llms

    Wangyue Lu, Lun Du, Sirui Li, Ke Weng, Haozhe Sun, Hengyu Liu, Minghe Yu, Tiancheng Zhang, and Ge Yu. Automated formalization via conceptual retrieval-augmented llms. arXiv preprint arXiv:2508.06931, 2025

    arXiv 2025

  15. [15]

    The Lean mathematical library

    The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

    2020

  16. [16]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Andr \'e Platzer and Geoff Sutcliffe (eds.), Automated Deduction -- CADE 28, pp.\ 625--635, Cham, 2021. Springer International Publishing. ISBN 978-3-030-79876-5

    2021

  17. [17]

    A new approach towards autoformalization, 2024

    Nilay Patel, Rahul Saha, and Jeffrey Flanigan. A new approach towards autoformalization, 2024. URL https://arxiv.org/abs/2310.07957

    Pith/arXiv arXiv 2024

  18. [18]

    Isabelle : A Generic Theorem Prover

    Lawrence C Paulson. Isabelle : A Generic Theorem Prover . Springer, 1994

    1994

  19. [19]

    Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition

    ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025

    Pith/arXiv arXiv 2025

  20. [20]

    Kimina-prover preview: Towards large formal reasoning models with reinforcement learning

    Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025

    Pith/arXiv arXiv 2025

  21. [21]

    First experiments with neural translation of informal to formal mathematics

    Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In International Conference on Intelligent Computer Mathematics, pp.\ 255--270. Springer, 2018

    2018

  22. [22]

    Homological conjectures in commutative algebra --- Wikipedia , the free encyclopedia

    Wikipedia contributors . Homological conjectures in commutative algebra --- Wikipedia , the free encyclopedia. https://en.wikipedia.org/w/index.php?title=Homological_conjectures_in_commutative_algebra&oldid=1299704292, 2025. [Online; accessed 22-September-2025]

    2025

  23. [23]

    Jiang, Wenda Li, Markus N

    Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models, 2022. URL https://arxiv.org/abs/2205.12615

    Pith/arXiv arXiv 2022

  24. [24]

    StepFun - Formalizer : Unlocking the Autoformalization Potential of LLMs through Knowledge - Reasoning Fusion , August 2025

    Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, and Xing Hu. StepFun - Formalizer : Unlocking the Autoformalization Potential of LLMs through Knowledge - Reasoning Fusion , August 2025. URL http://arxiv.org/abs/2508.04440. arXiv:2508.04440 [cs]

    arXiv 2025

  25. [25]

    Mathesis: Towards formal theorem proving from natural languages

    Yu Xuejun, Jianyuan Zhong, Zijin Feng, Pengyi Zhai, Roozbeh Yousefzadeh, Wei Chong Ng, Haoxiong Liu, Ziyi Shou, Jing Xiong, Yudong Zhou, et al. Mathesis: Towards formal theorem proving from natural languages. arXiv preprint arXiv:2506.07047, 2025

    Pith/arXiv arXiv 2025

  26. [26]

    Lean workbook: A large-scale lean problem set formalized from natural language math problems

    Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. Advances in Neural Information Processing Systems, 37: 0 105848--105863, 2024

    2024

  27. [27]

    Weinberger, and Yuhuai Wu

    Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu. Don't trust: Verify -- grounding llm quantitative reasoning with autoformalization, 2024. URL https://arxiv.org/abs/2403.18120

    Pith/arXiv arXiv 2024

  28. [28]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  29. [29]

    @esa (Ref

    \@ifxundefined[1] #1\@undefined \@firstoftwo \@secondoftwo \@ifnum[1] #1 \@firstoftwo \@secondoftwo \@ifx[1] #1 \@firstoftwo \@secondoftwo [2] @ #1 \@temptokena #2 #1 @ \@temptokena \@ifclassloaded agu2001 natbib The agu2001 class already includes natbib coding, so you should not add it explicitly Type <Return> for now, but then later remove the command n...

  30. [30]

    \@lbibitem[] @bibitem@first@sw\@secondoftwo \@lbibitem[#1]#2 \@extra@b@citeb \@ifundefined br@#2\@extra@b@citeb \@namedef br@#2 \@nameuse br@#2\@extra@b@citeb \@ifundefined b@#2\@extra@b@citeb @num @parse #2 @tmp #1 NAT@b@open@#2 NAT@b@shut@#2 \@ifnum @merge>\@ne @bibitem@first@sw \@firstoftwo \@ifundefined NAT@b*@#2 \@firstoftwo @num @NAT@ctr \@secondoft...

  31. [31]

    UR «T1e ;v̨ܹs3T 1c_֚5kSOe [o #Fd8?I ҇ ݻ+W\ܹSo . _/_V۶m_ 0 ? f P 0@?Sϝ;͛k۶m c5d '

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibsetup #1 @NAT@ctr @ @openbib .11em \@plus.33em \@minus.07em 4000 4000 `\.\@m @bibit...

    arXiv 1976