Pith. sign in

REVIEW 3 major objections 5 minor 120 references

Autoformalization evaluation can move from opaque yes/no scores to four-part diagnostics—verdict, error type, location, and a corrected formal statement—built on a 28-category error taxonomy.

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.5

2026-07-11 15:41 UTC pith:Y54LOZC7

load-bearing objection Solid engineering paper: first fine-grained diagnostic stack for autoformalization, with real ablations and a useful self-refine demo; main caveat is that multi-task numbers largely recover synthetic SCI labels. the 3 major comments →

arxiv 2607.04655 v1 pith:Y54LOZC7 submitted 2026-07-06 cs.CL

FormalRx: Rectify and eXamine Semantic Failures in Autoformalization

Haocheng Wang , Baiyu Huang , Yingjia Wan , Xiao Zhu , Xiaoyang Liu , Yinya Huang , Zhijiang Guo This is my paper
classification cs.CL
keywords autoformalizationsemantic alignmenterror taxonomyLean 4diagnostic evaluationNL-FL pairsformal mathematical reasoningself-refinement
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.

Turning natural-language math into formal Lean statements is only useful if the formalization means the same thing as the original. Existing checks mostly say “aligned” or “not,” or give a single score, so neither people nor training loops learn where or why a translation failed. This paper argues that autoformalization assessment should return actionable diagnostics: whether the pair is aligned, which of 28 error types is present, where in the formal code the problem sits, and a corrected formal statement. It builds that capability around a hierarchical SCI error taxonomy with strict priority rules so each failure gets one label, then trains a single model to emit all four answers at once and releases a matching fine-grained test set. The claim is that evaluation wired this way can drive systematic debugging and iterative improvement of autoformalizers rather than black-box acceptance or rejection.

Core claim

The paper establishes that semantic failures in autoformalization can be decomposed into 28 disjoint, priority-ordered categories (Semantic, Constraint, Implementation), and that a model trained on taxonomy-guided annotated NL–FL pairs can jointly produce alignment verdicts, error categories, localizations, and corrections—substantially outperforming general LLMs and specialized binary metrics on a held-out diagnostic benchmark, and that richer structured feedback improves multi-round formalizer self-refinement more than binary incorrect signals.

What carries the argument

The SCI Error Taxonomy: a hierarchical partition of autoformalization failures into Semantic, Constraint, and Implementation errors (28 categories total) with strict priority ordering and location-based catch-alls so each misalignment is assigned exactly one label; this taxonomy drives both synthetic diagnostic data and the four-task evaluation framework.

Load-bearing premise

That errors deliberately injected into correct formalizations under the taxonomy look enough like the failures real autoformalizers make that training and testing on them transfer outside the synthetic distribution.

What would settle it

Run FormalRx-style full diagnostics (category, location, correction) on a large set of human-annotated, naturally occurring misalignments from independent formalization corpora; if categorization, localization, and correction accuracy collapse relative to the synthetic FormalRx-Test numbers, or if structured feedback no longer beats binary feedback in self-refinement, the central transfer claim fails.

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

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

3 major / 5 minor

Summary. The paper introduces FormalRx, a diagnostic evaluation framework for autoformalization that goes beyond binary alignment scores. At its core is the SCI Error Taxonomy (Semantic, Constraint, Implementation), a 28-category hierarchy with priority ordering for Lean 4 formalization errors. The authors synthesize 56,287 NL–FL pairs via taxonomy-guided error injection from 17,825 aligned seeds, release FormalRx-Test (7,030 samples) with fine-grained labels, and train FormalRx-8B to jointly produce alignment verdict, error category, localization, and correction. On FormalRx-Test the model reports F1 0.88 (verdict) and 0.71 (categorization) and accuracies 0.75 (localization) and 0.73 (correction), outperforming instruct, frontier, and specialized baselines; ablations support taxonomy-guided synthesis, progressive training, and base-model choice. Limited OOD binary evaluation and a self-refinement study with structured feedback are also reported.

Significance. If the diagnostic signals transfer beyond the synthetic distribution, FormalRx would fill a genuine gap: existing autoformalization evaluators (BLEU, typecheck, BEq/GTED, FormalAlign, LeanScorer, LLM judges) give only binary or scalar outputs and no actionable localization or correction. The released taxonomy, FormalRx-Test, and FormalRx-8B weights, together with progressive multi-task training and human validation of LLM synthesis/retag/judges (~84.7% accuracy, substantial κ), are concrete, reusable contributions. The self-refinement experiment (Appendix H) further shows that structured FormalRx feedback improves formalizer Pass@8 more than binary LeanScorer feedback (49% vs 44% accumulated), which is a useful practical signal for iterative autoformalization pipelines.

major comments (3)
  1. The central multi-task claims (Table 3: categorization F1 0.71, localization 0.75, correction 0.73) are measured on FormalRx-Test, a held-out slice of the same Claude-Sonnet-4 taxonomy-guided injection and re-tag pipeline used for training (Section 4.3; Table 14: 52,521 synthetic negatives). Success therefore partly measures recovery of synthetic labels rather than diagnosis of independently labeled natural failures. Human validation is a 200-sample spot-check (98%, Appendix C.2) plus expert checks on LLM stages (Appendix C.1), not an external fine-grained corpus. Limitations §8 and Appendix I acknowledge this; the manuscript should either (a) report fine-grained human annotation on a sample of real autoformalizer outputs (e.g., from ConsistencyCheck/EPLA or a formalizer run) or (b) substantially qualify the claim that FormalRx enables systematic diagnosis of real systems.
  2. Out-of-domain evaluation (Section 6.2, Table 4) is restricted to binary verdict on ConsistencyCheck and EPLA. On these sets FormalRx’s margin over frontier models shrinks or disappears (e.g., GPT-5-mini F1 0.740 vs FormalRx-8B 0.596 on ConsistencyCheck), and the paper itself notes class-prior sensitivity and ground-truth quality issues. Because Tasks 2–4 have no external ground truth, the load-bearing claim that the full diagnostic suite transfers remains under-supported. At minimum, the abstract and conclusion should state clearly that fine-grained superiority is in-distribution, and the OOD section should discuss what would be required for a fair multi-task OOD test.
  3. The self-refinement study (Appendix H) uses FormalRx itself as the verifier that selects and annotates candidates for Goedel-Formalizer refinement. Accumulated Pass@8 gains (49% FormalRx vs 44% LeanScorer) therefore do not independently establish that the taxonomy recovers natural formalizer errors; they show that FormalRx’s own feedback is more useful than binary feedback under FormalRx’s own selection. A cleaner design would hold out a third-party or human verifier for the final Pass@8 measurement, or report agreement between FormalRx labels and human labels on the refined candidates.
minor comments (5)
  1. Table 1 and the abstract claim FormalRx is the first fine-grained diagnostic benchmark; this is fair for the four-task package, but the related-work discussion should more carefully distinguish prior subtask-decomposition judges (LeanScorer, AriaScorer) that already go beyond pure binary verdicts.
  2. Section 5.2 notes the zero-shot vs fine-tuned asymmetry; the main text should flag this earlier (e.g., when introducing Table 3) so readers do not over-read the frontier-model gaps on Tasks 2–4.
  3. Figure 2 and Appendix F.1/F.2: a short decision tree or worked multi-label ambiguity example in the main text would make the priority-ordering rule (S > I > C; nature over location) easier to apply for readers who will use the taxonomy.
  4. Appendix B.2 progressive-training results are strong (correction Acc 0.792 vs joint 0.729); consider promoting a one-sentence summary into the main experimental section so the training-method choice is not buried.
  5. Minor consistency: abstract and intro use both “SciError Taxonomy” and “SCI Error Taxonomy”; pick one spelling. Also fix occasional spacing artifacts (e.g., “AtitscoreisSciErrorTaxonomy”).

Circularity Check

1 steps flagged

No derivation-by-construction circularity; mild evaluation circularity only in that fine-grained metrics recover labels from the same taxonomy-guided synthesis pipeline used for training.

specific steps
  1. other [§4.3 Data Synthesis; Table 14; §6.1 Main Results; Limitations §8; Appendix I]
    "we synthesize misaligned pairs with complete diagnostic annotations based on the SciError Taxonomy... From this dataset, we hold out 7,030 samples as FormalRx-Test... FormalRx-8B achieves F1-scores of 0.88 (verdict) and 0.71 (categorization), along with accuracies of 0.75 (localization) and 0.73 (correction)... This part of the evaluation is also restricted to the verdict task, as no external benchmark provides error-type, localization, or correction labels."

    Fine-grained ground truth for Tasks 2–4 is produced by the same Claude taxonomy-guided injection + re-tag pipeline as the training negatives (52,521 synthetic misalignments). In-domain multi-task superiority therefore partly means recovering that pipeline’s labels on a hold-out split, not independently annotated natural failures. This is not Eq. X = Eq. Y by construction (a weak model can still fail), nor a fitted scalar renamed as prediction; it is mild evaluation circularity about what the fine-grained numbers certify. OOD and self-refinement use external binary/DeepSeek signals and do not close this loop.

full rationale

FormalRx is an empirical ML/systems paper, not a first-principles derivation. The SCI taxonomy is stipulated by design (partition + priority ordering), data are synthesized under that taxonomy, and FormalRx-8B is trained and tested on a hold-out of that process. High categorization/localization/correction scores therefore measure recovery of synthetic diagnostic labels, not a quantity forced by definition or by fitting a parameter that is then renamed as a prediction. Binary OOD verdicts (ConsistencyCheck, EPLA) and DeepSeek-verified self-refinement Pass@8 provide external checks that do not reduce to the training labels. Human spot-checks (200 samples; expert LLM-stage validation) further break pure self-reference. Limitations §8 and Appendix I already state the transfer gap. Under the analyzer’s strict rules this is evaluation-validity risk, not load-bearing circular derivation; score 2 for the mild synthetic-label recovery concern only.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 3 invented entities

The central empirical claims rest on standard ML practice plus two domain assumptions: that taxonomy-guided LLM error injection produces realistic, correctly labeled misalignments, and that the 28-category priority partition is operationally exhaustive for Lean autoformalization. No numerical free parameters are fitted to force the main results; the taxonomy and synthetic pipeline are the paper's invented scaffolding.

axioms (4)
  • domain assumption Taxonomy-guided LLM error injection (Claude-Sonnet-4) produces misalignments whose category, location, and correction labels match real autoformalization failures well enough for training and evaluation.
    Load-bearing for all fine-grained metrics and for claiming diagnostic usefulness beyond synthetic recovery; stated as a limitation in §8 and Appendix I.
  • ad hoc to paper The SCI 28-category hierarchy with priority ordering is pairwise disjoint and collectively exhaustive for Lean 4 autoformalization errors of interest.
    Design principle in §3.1; validated by synthesis saturation and human re-tag agreement, but not proven complete for long-tail or non-Lean systems.
  • domain assumption Compilation success under Lean 4.24.0 isolates semantic misalignment from syntactic invalidity for evaluation purposes.
    Used throughout data filtering (§4.3.2, Appendix E.2); standard in the subfield but excludes non-compiling failures from the diagnostic distribution.
  • standard math Standard supervised fine-tuning / CE loss and LLM-as-judge semantic equivalence for localization and correction are valid evaluation protocols.
    Training objective Eq. (1) and two-stage exact-match + DeepSeek-v3.2 judge (§5.2); human validation of judges in Appendix C.
invented entities (3)
  • SCI Error Taxonomy (28 categories with priority ordering) no independent evidence
    purpose: Partition autoformalization failures into actionable, unique labels for diagnosis and data synthesis.
    Core contribution of §3; independent evidence is limited to internal human agreement and synthesis coverage, not external adoption yet.
  • FormalRx-Test diagnostic benchmark no independent evidence
    purpose: First fine-grained (beyond binary) evaluation set for autoformalization diagnostics.
    Held-out synthetic set of 7,030 samples; released on Hugging Face.
  • FormalRx-8B multi-task diagnostic model no independent evidence
    purpose: Jointly predict verdict, category, location, and correction in one forward pass.
    Trained instantiation of the framework; weights released.

pith-pipeline@v1.1.0-grok45 · 42856 in / 3219 out tokens · 38400 ms · 2026-07-11T15:41:47.040643+00:00 · methodology

0 comments
read the original abstract

The veracious semantic alignment in autoformalization is significant for formal mathematical reasoning. However, existing evaluations provide only opaque binary verdicts or scalar scores, offering no interpretable insight into where or why translations fail. This opacity severely limits both human understanding and automated system improvement. To bridge this gap, we introduce FormalRx, a comprehensive diagnostic evaluation framework that transforms autoformalization assessment from black-box judgments into actionable feedback. At its core is SCI Error Taxonomy, a hierarchical classification scheme decomposing autoformalization errors into 28 distinct categories with strict priority ordering. Building on this taxonomy, FormalRx provides four critical diagnostic capabilities: alignment verdicts, error categorization, error localization, and correction. We instantiate the framework with a diagnostic model FormalRx-8B, trained on 56,287 NL-FL pairs with fine-grained diagnostic annotations, and release FormalRx-Test as the first fine-grained diagnostic benchmark. FormalRx-8B achieves F1-scores of 0.88 (verdict) and 0.71 (categorization), along with accuracies of 0.75 (localization) and 0.73 (correction), substantially outperforming both general-purpose LLMs and specialized baselines. By connecting evaluation with actionable insights, FormalRx enables systematic diagnosis and improvement of autoformalization systems.

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

120 extracted references · 22 linked inside Pith

  1. [1]

    arXiv preprint arXiv:2402.03300 , year=

    DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models , author=. arXiv preprint arXiv:2402.03300 , year=

    Pith/arXiv arXiv

  2. [2]

    Sheng, Guangming and Zhang, Chi and Ye, Zilingfeng and Wu, Xibin and Zhang, Wang and Zhang, Ru and Peng, Yanghua and Lin, Haibin and Wu, Chuan , booktitle=

  3. [3]

    arXiv preprint arXiv:2411.15124 , year=

    T\"ULU 3: Pushing Frontiers in Open Language Model Post-Training , author=. arXiv preprint arXiv:2411.15124 , year=

    Pith/arXiv arXiv

  4. [4]

    CoRR , volume =

    Kang, Feiyang and Kuchnik, Michael and Padthe, Karthik and Vlastelica, Marin and Jia, Ruoxi and Wu, Carole-Jean and Ardalani, Newsha , title =. CoRR , volume =. 2025 , doi =

    2025

  5. [5]

    CoRR , volume =

    Llama Team , title =. CoRR , volume =. 2024 , doi =

    2024

  6. [6]

    CoRR , volume =

    Team OLMo and Walsh, Pete and Soldaini, Luca and Groeneveld, Dirk and Lo, Kyle and Arora, Shane and Bhagia, Akshita and Gu, Yuling and Huang, Shengyi and Jordan, Matt and Lambert, Nathan and others , title =. CoRR , volume =. 2025 , doi =

    2025

  7. [7]

    CoRR , volume =

    Liu, Zihan and Chen, Yang and Shoeybi, Mohammad and Catanzaro, Bryan and Ping, Wei , title =. CoRR , volume =. 2024 , doi =

    2024

  8. [8]

    CoRR , volume =

    Yang, An and Zhang, Beichen and Hui, Binyuan and Gao, Bofei and Yu, Bowen and Li, Chengpeng and Liu, Dayiheng and Tu, Jianhong and Zhou, Jingren and Lin, Junyang and Lu, Keming and Xue, Mingfeng and Lin, Runji and Liu, Tianyu and Ren, Xingzhang and Zhang, Zhenru , title =. CoRR , volume =. 2024 , doi =

    2024

  9. [9]

    CoRR , volume =

    Yu, Qiying and Zhang, Zheng and Zhu, Ruofei and Yuan, Yufeng and Zuo, Xiaochen and Yue, Yu and Fan, Tiantian and Liu, Gaohong and Liu, Lingjun and Liu, Xin and Lin, Haibin and others , title =. CoRR , volume =. 2025 , doi =

    2025

  10. [10]

    CoRR , volume =

    Li, Chloe and Wichers, Nevan and Price, Sara and Marks, Samuel and Kutasov, Jon , title =. CoRR , volume =. 2026 , doi =

    2026

  11. [11]

    Don't Stop Pretraining: Adapt Language Models to Domains and Tasks , booktitle =

    Gururangan, Suchin and Marasovi. Don't Stop Pretraining: Adapt Language Models to Domains and Tasks , booktitle =. 2020 , doi =

    2020

  12. [12]

    and Jeon, Myeongho and Vu, Kim and Lai, Viet and Yang, Eunho , title =

    Le, Thanh-Long V. and Jeon, Myeongho and Vu, Kim and Lai, Viet and Yang, Eunho , title =. CoRR , volume =. 2026 , doi =

    2026

  13. [13]

    CoRR , volume =

    Kotha, Suhas and Liang, Percy , title =. CoRR , volume =. 2026 , doi =

    2026

  14. [14]

    Proceedings of the 13th International Conference on Learning Representations (ICLR) , year =

    Lin, Haohan and Sun, Zhiqing and Welleck, Sean and Yang, Yiming , title =. Proceedings of the 13th International Conference on Learning Representations (ICLR) , year =

  15. [15]

    , title =

    Zelikman, Eric and Wu, Yuhuai and Mu, Jesse and Goodman, Noah D. , title =. Advances in Neural Information Processing Systems (NeurIPS) , year =

  16. [16]

    CoRR , volume =

    Biderman, Dan and Portes, Jacob and Ortiz, Jose Javier Gonzalez and Paul, Mansheej and Greengard, Philip and Jennings, Connor and King, Daniel and Havens, Sam and Chiley, Vitaliy and Frankle, Jonathan and Blakeney, Cody and Cunningham, John Patrick , title =. CoRR , volume =. 2024 , doi =

    2024

  17. [17]

    Synthetic Continued Pretraining , booktitle =

    Yang, Zitong and Band, Neil and Li, Shuangping and Cand. Synthetic Continued Pretraining , booktitle =. 2025 , doi =

    2025

  18. [18]

    CoRR , volume =

    Guo, Yiduo and Fu, Jie and Yang, Yu and Wang, Zicheng and Shi, Lifu and Yang, Diyi and Liu, Yang , title =. CoRR , volume =. 2024 , doi =

    2024

  19. [19]

    CoRR , volume =

    Liu, Bowen and Yang, Wenjing , title =. CoRR , volume =. 2025 , doi =

    2025

  20. [20]

    CoRR , volume =

    Yao, Mingcong and Yang, Hong and Sun, Hai and Tu, Wei , title =. CoRR , volume =. 2025 , doi =

    2025

  21. [21]

    CoRR , volume =

    Yuan, Zheng and Yuan, Hongyi and Li, Chengpeng and Dong, Guanting and Lu, Keming and Tan, Chuanqi and Zhou, Chang and Zhou, Jingren , title =. CoRR , volume =. 2023 , doi =

    2023

  22. [22]

    Proceedings of the National Academy of Sciences , volume=

    Overcoming catastrophic forgetting in neural networks , author=. Proceedings of the National Academy of Sciences , volume=. 2017 , publisher=

    2017

  23. [23]

    Proceedings of the 26th Annual International Conference on Machine Learning (ICML) , pages=

    Curriculum learning , author=. Proceedings of the 26th Annual International Conference on Machine Learning (ICML) , pages=. 2009 , organization=

    2009

  24. [24]

    Advances in Neural Information Processing Systems (NeurIPS) , volume=

    Experience Replay for Continual Learning , author=. Advances in Neural Information Processing Systems (NeurIPS) , volume=. 2019 , publisher=

    2019

  25. [25]

    International Conference on Learning Representations , year=

    Decoupled Weight Decay Regularization , author=. International Conference on Learning Representations , year=

  26. [26]

    Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis , articleno =

    Rajbhandari, Samyam and Rasley, Jeff and Ruwase, Olatunji and He, Yuxiong , title =. Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis , articleno =. 2020 , isbn =

    2020

  27. [27]

    2025 , eprint=

    Qwen3 Technical Report , author=. 2025 , eprint=

    2025

  28. [29]

    The problems of two paradoxes , author=

    High agreement but low kappa: I. The problems of two paradoxes , author=. Journal of clinical epidemiology , volume=. 1990 , publisher=

    1990

  29. [30]

    2018 , publisher=

    Content analysis: An introduction to its methodology , author=. 2018 , publisher=

    2018

  30. [31]

    Fam med , volume=

    Understanding interobserver agreement: the kappa statistic , author=. Fam med , volume=

  31. [32]

    2025 , month =

    OpenAI , title =. 2025 , month =

    2025

  32. [33]

    Introducing GPT-5 , year =

  33. [34]

    Introducing GPT-5.2 , year =

  34. [35]

    Introducing GPT-5.3-Codex , year =

  35. [36]

    2025 , month =

    Anthropic , title =. 2025 , month =

    2025

  36. [37]

    Introducing Claude Sonnet 4.6 , year =

  37. [38]

    Introducing Claude Opus 4.6 , year =

  38. [39]

    2025 , eprint=

    DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models , author=. 2025 , eprint=

    2025

  39. [40]

    2025 , eprint=

    DeepSeek-V3 Technical Report , author=. 2025 , eprint=

    2025

  40. [41]

    2025 , eprint=

    Qwen2.5 Technical Report , author=. 2025 , eprint=

    2025

  41. [42]

    Nature , volume=

    DeepSeek-R1 incentivizes reasoning in LLMs through reinforcement learning , author=. Nature , volume=. 2025 , publisher=

    2025

  42. [43]

    1960 , publisher=

    Naive set theory , author=. 1960 , publisher=

    1960

  43. [45]

    2011 , publisher=

    Discrete Mathematics and Its Applications , author=. 2011 , publisher=

    2011

  44. [46]

    Mathematics and its Applications , author=

  45. [47]

    and Lean Community , title =

    Doll, Moritz and Carneiro, Mario and Lewis, Robert Y. and Lean Community , title =. 2022 , howpublished =

    2022

  46. [50]

    The Tenth International Conference on Learning Representations,

    Kunhao Zheng and Jesse Michael Han and Stanislas Polu , title =. The Tenth International Conference on Learning Representations,. 2022 , url =

    2022

  47. [55]

    2024 , howpublished =

    David Renshaw and contributors , title =. 2024 , howpublished =

    2024

  48. [58]

    2024 , url =

    A read-eval-print-loop for. 2024 , url =

    2024

  49. [59]

    PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition , booktitle =

    George Tsoukalas and Jasper Lee and John Jennings and Jimmy Xin and Michelle Ding and Michael Jennings and Amitayush Thakur and Swarat Chaudhuri , editor =. PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition , booktitle =. 2024 , url =

    2024

  50. [60]

    Huajian Xin and Z. Z. Ren and Junxiao Song and Zhihong Shao and Wanjia Zhao and Haocheng Wang and Bo Liu and Liyue Zhang and Xuan Lu and Qiushi Du and Wenjun Gao and Haowei Zhang and Qihao Zhu and Dejian Yang and Zhibin Gou and Z. F. Wu and Fuli Luo and Chong Ruan , title =. The Thirteenth International Conference on Learning Representations,. 2025 , url =

    2025

  51. [61]

    Nature , year =

    Thomas Hubert and Rishi Mehta and Laurent Sartran and others , title =. Nature , year =. doi:10.1038/s41586-025-09833-y , url =

    doi:10.1038/s41586-025-09833-y

  52. [62]

    Aristotle Achieves Gold Medal-Level Performance at the International Mathematical Olympiad, iOS App Beta Launch , howpublished =

  53. [63]

    2025 , eprint=

    Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience , author=. 2025 , eprint=

    2025

  54. [64]

    CoRR , volume =

    Luoxin Chen and Jinming Gu and Liankai Huang and Wenhao Huang and Zhicheng Jiang and Allan Jie and Xiaoran Jin and Xing Jin and Chenggang Li and Kaijing Ma and Cheng Ren and Jiawei Shen and Wenlei Shi and Tong Sun and He Sun and Jiahui Wang and Siran Wang and Zhihong Wang and Chenrui Wei and Shufa Wei and Yonghui Wu and Yuchen Wu and Yihang Xia and Huajia...

    Pith/arXiv arXiv doi:10.48550/arxiv.2507.23726 2025

  55. [66]

    CoRR , volume =

    Yichi Zhou and Jianqiu Zhao and Yongxin Zhang and Bohan Wang and Siran Wang and Luoxin Chen and Jiahui Wang and Haowei Chen and Allan Jie and Xinbo Zhang and Haocheng Wang and Luong Quoc Trung and Rong Ye and Phan Nhat Hoang and Huishuai Zhang and Peng Sun and Hang Li , title =. CoRR , volume =. 2025 , url =. doi:10.48550/ARXIV.2507.15225 , eprinttype =. ...

    Pith/arXiv arXiv doi:10.48550/arxiv.2507.15225 2025

  56. [70]

    CoRR , volume =

    Zhaoyu Li and Jialiang Sun and Logan Murphy and Qidong Su and Zenan Li and Xian Zhang and Kaiyu Yang and Xujie Si , title =. CoRR , volume =. 2024 , url =. doi:10.48550/ARXIV.2404.09939 , eprinttype =. 2404.09939 , timestamp =

    Pith/arXiv arXiv doi:10.48550/arxiv.2404.09939 2024

  57. [71]

    Jiang and Wenda Li and Mateja Jamnik , editor =

    Albert Q. Jiang and Wenda Li and Mateja Jamnik , editor =. Multi-language Diversity Benefits Autoformalization , booktitle =. 2024 , url =

    2024

  58. [72]

    Isabelle/HOL --- A Proof Assistant for Higher-Order Logic , isbn =

    Nipkow, Tobias and Paulson, Lawrence and Wenzel, Markus , year =. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic , isbn =. Lecture Notes in Computer Science - LNCS , doi =

  59. [73]

    1997 , month =

    Barras, Bruno and Boutin, Samuel and Cornes, Cristina and Courant, Judica. 1997 , month =

    1997

  60. [77]

    CoRR , volume =

    Auguste Poiroux and Antoine Bosselut and Viktor Kuncak , title =. CoRR , volume =. 2025 , url =. doi:10.48550/ARXIV.2510.25427 , eprinttype =. 2510.25427 , timestamp =

    doi:10.48550/arxiv.2510.25427 2025

  61. [80]

    The Thirteenth International Conference on Learning Representations,

    Qi Liu and Xinhao Zheng and Xudong Lu and Qinxiang Cao and Junchi Yan , title =. The Thirteenth International Conference on Learning Representations,. 2025 , url =

    2025

  62. [81]

    Rabe and Charles Staats and Mateja Jamnik and Christian Szegedy , editor =

    Yuhuai Wu and Albert Qiaochu Jiang and Wenda Li and Markus N. Rabe and Charles Staats and Mateja Jamnik and Christian Szegedy , editor =. Autoformalization with Large Language Models , booktitle =. 2022 , url =

    2022

  63. [82]

    Lean Workbook:

    Huaiyuan Ying and Zijian Wu and Yihan Geng and Jiayu Wang and Dahua Lin and Kai Chen , editor =. Lean Workbook:. Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 - 15, 2024 , year =

    2024

  64. [83]

    The Thirteenth International Conference on Learning Representations,

    Guoxiong Gao and Yutong Wang and Jiedong Jiang and Qi Gao and Zihan Qin and Tianyi Xu and Bin Dong , title =. The Thirteenth International Conference on Learning Representations,. 2025 , url =

    2025

  65. [85]

    Forty-first International Conference on Machine Learning,

    Logan Murphy and Kaiyu Yang and Jialiang Sun and Zhaoyu Li and Anima Anandkumar and Xujie Si , title =. Forty-first International Conference on Machine Learning,. 2024 , url =

    2024

  66. [88]

    The Thirteenth International Conference on Learning Representations,

    Jianqiao Lu and Yingjia Wan and Yinya Huang and Jing Xiong and Zhengying Liu and Zhijiang Guo , title =. The Thirteenth International Conference on Learning Representations,. 2025 , url =

    2025

  67. [91]

    2025 , eprint=

    ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings , author=. 2025 , eprint=

    2025

  68. [92]

    Introducing claude 4

    Anthropic. Introducing claude 4. https://www.anthropic.com/news/claude-4, May 2025. Accessed: 2026-01-22

    2025

  69. [93]

    Introducing claude sonnet 4.6, Feb

    Anthropic . Introducing claude sonnet 4.6, Feb. 2026. URL https://www.anthropic.com/news/claude-sonnet-4-6. Accessed: 2026-03-21

    2026

  70. [94]

    Azerbayev, B

    Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433, 2023. doi:10.48550/ARXIV.2302.12433. URL https://doi.org/10.48550/arXiv.2302.12433

    Pith/arXiv arXiv doi:10.48550/arxiv.2302.12433 2023

  71. [95]

    Barras, S

    B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filli \^a tre, E. Gim \'e nez, H. Herbelin, G. Huet, C. Mu \ n oz, C. Murthy, C. Parent-vigouroux, C. Paulin-Mohring, A. Sa \"i bi, and B. Werner. The coq proof assistant reference manual : Version 6.1. 06 1997

    1997

  72. [96]

    G. Chen, J. Wu, X. Chen, W. X. Zhao, R. Song, C. Li, K. Fan, D. Liu, and M. Liao. Reform: Reflective autoformalization with prospective bounded sequence optimization. CoRR, abs/2510.24592, 2025. doi:10.48550/ARXIV.2510.24592. URL https://doi.org/10.48550/arXiv.2510.24592

    doi:10.48550/arxiv.2510.24592 2025

  73. [97]

    de Moura and S

    L. de Moura and S. Ullrich. The lean 4 theorem prover and programming language. In A. Platzer and G. Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings , volume 12699 of Lecture Notes in Computer Science, pages 625--635. Springer, 2021. doi:10.1007/978-3-03...

    doi:10.1007/978-3-030-79876-5 2021

  74. [98]

    L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The lean theorem prover (system description). In A. P. Felty and A. Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings , volume 9195 of Lecture Notes in Computer Science, pages 378--388...

    doi:10.1007/978-3-319-21401-6 2015

  75. [99]

    DeepSeek-AI, A. Liu, B. Feng, B. Xue, B. Wang, B. Wu, C. Lu, C. Zhao, C. Deng, C. Zhang, C. Ruan, D. Dai, D. Guo, D. Yang, D. Chen, D. Ji, E. Li, F. Lin, F. Dai, F. Luo, G. Hao, G. Chen, G. Li, H. Zhang, H. Bao, H. Xu, H. Wang, H. Zhang, H. Ding, H. Xin, H. Gao, H. Li, H. Qu, J. L. Cai, J. Liang, J. Guo, J. Ni, J. Li, J. Wang, J. Chen, J. Chen, J. Yuan, J...

    Pith/arXiv arXiv 2025

  76. [100]

    DeepSeek-AI, A. Liu, A. Mei, B. Lin, B. Xue, B. Wang, B. Xu, B. Wu, B. Zhang, C. Lin, C. Dong, C. Lu, C. Zhao, C. Deng, C. Xu, C. Ruan, D. Dai, D. Guo, D. Yang, D. Chen, E. Li, F. Zhou, F. Lin, F. Dai, G. Hao, G. Chen, G. Li, H. Zhang, H. Xu, H. Li, H. Liang, H. Wei, H. Zhang, H. Luo, H. Ji, H. Ding, H. Tang, H. Cao, H. Gao, H. Qu, H. Zeng, J. Huang, J. L...

    Pith/arXiv arXiv 2025

  77. [101]

    M. Doll, M. Carneiro, R. Y. Lewis, and L. Community. The qify tactic. Mathlib4 Repository, 2022. URL https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Qify.lean. Accessed: 2026-01-23

    2022

  78. [102]

    G. Gao, Y. Wang, J. Jiang, Q. Gao, Z. Qin, T. Xu, and B. Dong. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025 . OpenReview.net, 2025. URL https://openreview.net/forum?id=Se6MgCtRhz

    2025

  79. [103]

    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. Nature, 645 0 (8081): 0 633--638, 2025 a

    2025

  80. [104]

    Q. Guo, J. Wang, J. Zhang, D. Kong, X. Huang, X. Xi, W. Wang, J. Wang, X. Cai, S. Zhang, and W. Ye. Autoformalizer with tool feedback. CoRR, abs/2510.06857, 2025 b . doi:10.48550/ARXIV.2510.06857. URL https://doi.org/10.48550/arXiv.2510.06857

    doi:10.48550/arxiv.2510.06857 2025

Showing first 80 references.