Pith. sign in

REVIEW 5 major objections 3 minor 12 references

FMC: Formalization of Natural Language Mathematical Competition Problems

T0 review · 5 major / 3 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read A fully automatic, training-free LLM pipeline with error feedback claims to formalize Olympiad-level problems into Lean at 81.74% semantic consistency, yielding a 3,922-problem benchmark that current theorem provers solve only 13–16% of…

desk verdict A useful autoformalization pipeline and a new Olympiad-scale Lean dataset, but the quality-certification claims don't survive the paper's own appendix. read the letter →

arxiv 2507.11275 v1 pith:3SGMM2T2 submitted 2025-07-15 cs.CL

Jiaxuan Xie , Chengwu Liu , Ye Yuan , Siqi Li , Zhiping Xiao , Ming Zhang This is my paper · ORCID
classification cs.CL
keywords autoformalizationLean4OlympiadmathematicsLLMpipelineerrorfeedbackbenchmarkdatasetautomatedtheoremprovingsemanticconsistency
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper sets out to show that a fully automatic, training-free pipeline can convert natural-language mathematics competition problems into Lean formal statements at scale, producing a dataset that is both Olympiad-difficult and usable as a benchmark. The pipeline translates each problem with the DeepSeek-R1 model under few-shot prompting, checks the Lean statement with the Lean 4 REPL, translates it back to natural language, and asks the model whether the backtranslation matches the original; failed statements are retried with the error messages fed back into the prompt. On 4,798 preprocessed IMOmath problems it reports 93.39% syntactic validity and 81.74% semantic consistency, yielding FMC: 3,922 natural-language problems aligned with 9,787 Lean statements, of which 64.46% were rated at least above-average by an LLM quality judge. The payoff would be a cheap, repeatable route to competition-level formal data, replacing the expert hand-annotation that previously was required for hard problems. The paper also positions FMC as a theorem-prover benchmark: three automated provers solve only 13–16% of a random 1,000-statement sample, placing its difficulty between ProofNet and FormalMATH.

What carries the argument

The carrying mechanism is the four-stage autoformalization loop: formal translation of a natural-language problem into Lean by a few-shot LLM prompt; syntactic verification by the Lean 4 REPL (via the DeepSeek-Prover verifier); backtranslation of the Lean statement into natural language; and a consistency check in which an LLM compares the backtranslation against the original problem and must confirm identical conditions and goals. Any failure at the verification or consistency stage produces an error message that is inserted into a revised prompt, and the translation model retries once; this 'error feedback' loop is what the paper credits for the improvement over the Lean Workbook pipeline, along with a stronger base model. The named object is the FMC pipeline, and its load-bearing parts are the off-the-shelf DeepSeek-R1 model used for all three language roles and the REPL verifier that supplies structured, interpretable error text.

What would settle it

Take a random sample of roughly 100 entries from the released FMC dataset that passed both the syntax and consistency checks and have a mathematician with Lean experience judge whether each Lean statement expresses exactly the original problem's conditions and conclusion. If the human-verified rate falls well below 81.74%, or if the $f(240)$ and candy-distribution statements from Appendix A appear in the released data as passed entries, then the consistency filter demonstrably fails and the dataset-quality claim reduces to the raw translation pass rate.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that error feedback is what makes the translate–verify–backtranslate–check loop strong enough to formalize Olympiad-level problems without human annotation: feeding Lean's error messages and the consistency checker's rationale into a second translation attempt raised the overall pass rate, with the semantic-feedback retries contributing the larger gain (10.52% on the ablation subset, versus a negligible effect from syntax-error messages), and sampling each problem five times at temperature 1.0 raised formalization accuracy from 59.65% to 91.22% on the same subset. The authors therefore claim that the resulting dataset strikes a balance between scale and difficulty: the 3,922-problem FMC set with 9,787 Lean statements, of which 64.46% were judged to be at least above-average quality, derived from problems at IMO and national-Olympiad difficulty. They demonstrate the benchmark value by showing that three automated theorem provers reach intermediate pass rates on a 1,000-problem sample (16.4% for Kimina-Prover, 15.7% for Goedel-Prover, 13.0% for DeepSeek-Prover-V1.5-RL), between ProofNet and FormalMATH and well below their 50–63% on miniF2F.

Load-bearing premise

The load-bearing premise is that the LLM-based consistency check — backtranslating the Lean statement and judging whether it matches the original problem's conditions and goals — reliably rejects semantically wrong formalizations, yet the paper's own appendices show formally verified and consistency-checked statements that are mathematically wrong (a mistaken value for $f(240)$, a candy-distribution formula using $k(k+3)/2$ instead of triangular numbers, and a combinatorics statement missing a key condition).

Editorial extensions

If this is right

  • Competition-level formal data can be produced cheaply and repeatedly: FMC required 161 million tokens and no fine-tuning, a cost profile that makes dataset reconstruction for new problem sources or languages feasible.
  • FMC gives theorem provers a difficulty plateau between ProofNet and FormalMATH (13–16% solve rates), one that separates provers that all succeed on miniF2F-class problems.
  • The cheap quality knobs are confirmed: few-shot examples, one error-feedback retry, and more samples per problem each measurably raise the pass rate, with per-problem sampling providing the largest gain.
  • Geometry is out of reach for this approach — the paper filters out all geometry problems because LLM formalizations omit implicit constraints and still pass both checks — so FMC covers algebra and number theory rather than the full Olympiad scope.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper's own appendix evidence implies the real semantic error rate is higher than 81.74%: formally verified and consistency-checked statements include a wrong value for $f(240)$, a candy-distribution formula using $k(k+3)/2$ in place of the triangular numbers $\frac{k(k+1)}{2}$, and a magician-card problem whose Lean text omits the distinct-pair condition. A human-annotated subsample, which th
  • Because the consistency judge is the same family of model that wrote the formalizations, the check may be biased toward agreement; downstream users should treat the 81.74% figure as a pipeline-internal estimate, not a certified accuracy.
  • A testable extension is per-domain consistency reporting: the authors' ablations and case studies suggest error modes cluster (recursion, 'find all' goals, combinatorics), so field-specific pass rates would make the benchmark far more informative than the aggregate number.
  • Since syntax-error feedback barely helped while semantic feedback helped a lot, a cheaper variant that skips the verifier-feedback step and retries only on semantic failures would likely match the full pipeline's accuracy at lower token cost; the paper's Table 6 numbers are consistent with that hypothesis.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

5 major / 3 minor

Summary. The paper proposes an automatic, training-free autoformalization pipeline that translates natural-language Olympiad problems into Lean statements using LLMs with error feedback. The pipeline combines formal translation, Lean formal verification, backtranslation, and an LLM-based consistency check. Using this pipeline, the authors construct the FMC dataset, reported as 3,922 natural-language problems aligned with 9,787 Lean statements, and claim 81.74% semantic consistency and 64.46% above-average quality. They further study the formalization and consistency-check capabilities of DeepSeek-R1, GPT-4o-mini, and Claude 3.7 Sonnet, and benchmark three automated theorem provers on the dataset. The central claim is that FMC is a high-quality, Olympiad-level benchmark for automated theorem provers.

Significance. If the central claims were established, the work would be useful: a large, automatically constructed Lean dataset from competition problems could support training and evaluation of theorem provers. The paper has concrete strengths: the pipeline is fully automatic and training-free, the ablation studies on few-shot learning, error feedback, and sampling are informative, and the appendix is unusually transparent in documenting formalization failures. However, the load-bearing validation is not established. The paper's own appendix and Table 4 show that the consistency checker passes mathematically incorrect formalizations and has only 74.1% accuracy on the authors' evaluation set, so the measured 'semantic consistency' cannot be read as semantic correctness. The 64.46% quality figure is an LLM-generated rating of research interest, not of mathematical fidelity. Consequently, the dataset's value as a benchmark is not supported by the evidence presented.

major comments (5)
  1. [§4.3, Table 1, Table 4] The reported 81.74% consistency-check pass rate is presented as the pipeline's 'formalization accuracy,' but the consistency checker has only 74.1% accuracy and 69.8% precision on the paper's own evaluation set (Table 4). The paper's Appendix A and B.3 give multiple statements that passed both formal verification and the consistency check yet are mathematically wrong. Since the proofs are placeholders ('by sorry'), Lean verification only confirms that the statements typecheck and does not establish mathematical truth. The 81.74% figure therefore cannot be interpreted as a validated semantic-correctness rate, and it does not support the central claim that the dataset is reliable enough to be a benchmark.
  2. [§A.1, §A.2, §B.3] The appendix documents examples that passed the pipeline but are mathematically incorrect. In §A.1, the candy-distribution formalization uses k*(k+3)/2 instead of the triangular-number pattern k*(k+1)/2 and omits the condition that n must be a power of two; the semiperimeter example encodes only two recursion levels rather than infinite iteration. In §A.2, the formalization of 'Find f(240)' asserts the incorrect value f(240)=38808. In §B.3, the magician-cards statement omits the requirement that the two pairs of boxes be distinct and omits the counting goal entirely. These are not边缘 examples: they are the paper's own case studies of failures, and at least the §B.3 statement appears in the final dataset. This directly contradicts the claim that passing formal verification and consistency check indicates a correct formalization.
  3. [§4.2, Figure 2] The geometry example in Figure 2 is explicitly described as a failed formalization that nevertheless passed both formal verification and the consistency check: the triangle angle-sum constraint and the equality-condition goal are missing. Although geometry problems are later excluded from the dataset, this example demonstrates that the consistency checker cannot reliably detect omitted implicit conditions. Since many Olympiad problems rely on such implicit constraints, the failure is not confined to geometry, and it undermines the use of the consistency check as a quality filter.
  4. [§4.3, 'Dataset Construction and Evaluation'] The quality assessment that yields 64.46% 'above average or higher' is performed by an LLM (DeepSeek-R1) using criteria such as research relevance, interdisciplinary potential, and innovativeness. No human validation, inter-annotator agreement, or error analysis is reported, and the criteria do not measure mathematical correctness or fidelity to the original problem. This rating therefore does not support the claim that the dataset is high-quality for automated theorem proving.
  5. [§5.5, Table 8] The benchmark experiments measure provers' success on the formal Lean statements in FMC. Because the formal statements have unproved bodies ('by sorry') and because the semantic alignment between the natural-language problems and the Lean statements is not reliable—as the appendix demonstrates—a prover's pass rate on FMC does not measure its ability to solve the original competition problems. The comparison with MiniF2F, ProofNet, and FormalMATH is therefore ambiguous, and the claim that FMC is 'competitive as a benchmark' is not supported.
minor comments (3)
  1. [Throughout] There are several typos and inconsistent spellings: 'Automformalization' in the title of §2.3, 'Olympaid' in §2.3, 'balances bwtween' in the conclusion, and 'it's' instead of 'its' in the introduction. The model name is spelled both 'Deepseek-R1' and 'DeepSeek-R1'; please standardize.
  2. [Appendix A] For each case study in Appendix A, please state explicitly whether the shown formalization is included in the final FMC dataset or was excluded. This is important for interpreting the examples as evidence about the dataset itself.
  3. [§3.4] The consistency-check prompt asks the model to determine whether two problems are the same in 'mathematical essence,' but the paper does not report any calibration or threshold analysis for this binary judgment. Adding a small human-labeled evaluation set with agreement rates would strengthen the reliability claims.

Circularity Check

3 steps flagged · score 6.0 of 10

The headline semantic-consistency and quality figures are self-referential: DeepSeek-R1 generates, backtranslates, and judges the formalizations, and the 64.46% quality rating is an LLM self-assessment; the paper's own case studies show wrong statements passing the checks.

  1. self definitional [Sections 3.1, 3.3, 3.4 and Section 5.1 (Table 4 discussion)]
    "One notable exception is that when GPT-4o-mini is used for both formalization and back-translation, its consistency check pass rate exceeds that of Deepseek-R1—likely due to an inflated accuracy from using the same model for both formalization and consistency checking."

    The main FMC pipeline runs the same DeepSeek-R1 model as translator (Section 3.1), backtranslator (Section 3.3), and consistency judge (Section 3.4). Therefore the reported 81.74% consistency-check pass rate is the rate at which the model judged its own round-tripped versions to be 'Same' in mathematical essence; it is not an external semantic-correctness measurement. The paper itself concedes that this design inflates pass rates: when one model is used for both formalization and consistency checking, the consistency pass rate is 'likely due to an inflated accuracy from using the same model.' The headline semantic-consistency number is thus a self-agreement statistic by construction.

  2. other [Section 4.3, Dataset Construction and Evaluation, Figure 3]
    "This study further assesses dataset quality by evaluating each mathematical theorem along five dimensions using a large language model ... Overall, 64.46% of the data received ratings of above average or higher, suggesting a generally acceptable dataset quality."

    The 64.46% above-average quality figure is produced by an LLM evaluating the pipeline's own formal statements on five subjective criteria, with no reported human validation or held-out external standard. The metric is the evaluator's own rating; presenting it as 'generally acceptable dataset quality' makes the rating itself the evidence for quality. As with a fitted parameter renamed as a prediction, the output is the model's self-assessment rather than an independent property of the dataset.

1 more flagged steps
  1. other [Appendix A.1, A.2, B.3 and Section 4.2 (Figure 2)]
    "the formalized conclusion's assertion that f(240)=38808 is incorrect, revealing a serious validation failure ... In this case, the formal statement in FMC does not precisely align with the original natural language description ... the FMC version fails to explicitly ensure that (b1,b2) and (b3,b4) refer to two distinct pairs of boxes ... does not specify the desired conclusion."

    The paper's own case studies document formalizations that passed Lean's syntax check and the consistency check yet are mathematically wrong or incomplete: f(240) is assigned an incorrect value, the candy-distribution formula uses k(k+3)/2 instead of triangular numbers, the magician-card statement omits the distinct-pair condition and the counting goal, and the geometry example misses the triangle constraints and equality goal. Thus the consistency check does not certify equivalence to the original problem. The labels 'successfully formalized' and the derived consistency/quality percentages are determined by the same model's self-consistent judgment, not by the mathematical content, so the acceptance criterion and the claimed quality measure are the same self-confirming signal.

full rationale

The derivation chain for the two headline quality numbers is internal rather than first-principles. DeepSeek-R1 formalizes the natural-language problem, backtranslates the Lean statement, and then judges whether the two are mathematically consistent; the reported 81.74% semantic consistency is therefore the model's round-trip self-agreement rate. The paper itself notes that using the same model for formalization and consistency checking inflates pass rates, and its own Appendix A/B case studies show wrong or incomplete statements that nevertheless passed both checks. Similarly, the 64.46% above-average quality rating is an LLM's evaluation of the pipeline's own output, without reported human validation, so it restates the evaluator's preference rather than an external quality measurement. The dataset does have some independent content: the Lean statements are concrete, and the automated-theorem-prover experiments provide external, falsifiable results. The paper is also transparent about the consistency checker's failures and does not rely on a load-bearing self-citation or an imported uniqueness theorem. But because the central semantic-consistency and quality claims reduce, by construction, to the same model family's self-judgment, the circularity is partial and material, warranting a score of 6.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new mathematical entities or axioms. The main assumptions are about the reliability of LLM-based semantic checking and quality assessment, and the representativeness of the filtered dataset. Free parameters are limited to prompt and sampling hyperparameters.

free parameters (3)
  • temperature = 1.0
    Set to 1.0 during formalization to balance syntactic correctness and output diversity; chosen by hand, not tuned on a dev set.
  • sampling number = 5
    Each problem is sampled five times per run; chosen due to computational constraints, not systematically optimized.
  • few-shot examples = 2 fixed examples (algebra, number theory)
    Two examples are included in the first translation prompt because they are common in Olympiad contests; no evidence of systematic selection.
assumptions (4)
  • domain assumption IMOmath problems are correct and at Olympiad difficulty as stated.
    The dataset quality starts from the assumption that scraped IMOmath problems are accurate official competition problems; used as the ground truth for all downstream evaluation.
  • domain assumption The LLM-based backtranslation and consistency check reliably detect semantic equivalence between natural language and formal statements.
    The pipeline relies on this to filter incorrect formalizations. The paper's own case studies show this assumption is violated, e.g., the candy distribution and f(240) examples passed both checks yet are mathematically wrong.
  • domain assumption The LLM-based quality rating with five criteria reflects actual dataset quality.
    The 64.46% above-average claim rests entirely on an LLM rating with no human evaluation or inter-annotator agreement.
  • domain assumption Excluding all geometry problems does not undermine the 'Olympiad-level' claim.
    Geometry is a major component of Olympiad mathematics, and its exclusion removes a large class of problems, making the dataset a biased sample.

how reviews work

0 comments
Cite this review

Pith. "Pith review of FMC: Formalization of Natural Language Mathematical Competition Problems." pith.science (2026). https://pith.science/paper/3SGMM2T2

@misc{pith2026250711275,
  author       = {Pith},
  title        = {Pith review of: FMC: Formalization of Natural Language Mathematical Competition Problems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3SGMM2T2}},
  note         = {Machine review of arXiv:2507.11275}
}
abstract

Efficient and accurate autoformalization methods, which leverage large-scale datasets of extensive natural language mathematical problems to construct formal language datasets, are key to advancing formal mathematical reasoning. In this paper, we propose an autoformalization pipeline based on large language models with error feedback, achieving a fully automatic and training-free formalization approach. Using this pipeline, we curate an Olympiad-level dataset aligning natural language problems with Lean formalizations. The dataset comprises $3,922$ mathematical problems in natural language and $9,787$ in Lean, of which $64.46\%$ were assessed as at least above-average quality, making it suitable as a benchmark for automated theorem provers. Additionally, we investigate the formalization and reasoning capabilities of various LLMs and empirically demonstrate that few-shot learning, error feedback, and increasing sampling numbers enhance the autoformalization process. Experiments of three automated theorem provers on the \dataset\ dataset also highlight its challenging nature and its value as a benchmark for formal reasoning tasks.

Figures

Figures reproduced from arXiv: 2507.11275 by the authors.

Figure 1
Figure 1. Autoformalization Pipeline. 3.1. Translation Within this autoformalization pipeline, the model is required to translate natural language mathematical problems into for￾mal language in two distinct scenarios: the first involves di￾rect translation guided by few-shot prompting, while the sec￾ond leverages error feedback incorporated into the prompt following a failed attempt. The first case occurs during the initial t… view at source ↗
Figure 2
Figure 2. presents an incorrect formalization example. The original problem, described in natural language, involves a mathematical proposition about the internal angle bisec￾tors of a triangle, where ma, mb, mc denote the lengths of the three angle bisectors, and Ma, Mb, Mc represent their extended lengths intersecting the circumcircle. The objec￾tive is to prove an inequality along with the conditions for equality. In the L… view at source ↗
Figure 3
Figure 3. , indicate strong performance in complexity and depth as well as community needs and gaps, but weaker per￾formance in interdisciplinary potential and innovativeness. This pattern closely relates to the original data selection, as Olympiad-level problems tend to be relatively challenging, and the Lean community currently lacks data of comparable difficulty. Overall, 64.46% of the data received ratings of above averag… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

12 extracted references · 7 canonical work pages

  1. [1]

    Relevance to Current Research: Does the statement address a problem or concept that is actively being researched in mathematics or related fields? Higher relevance scores indicate greater potential interest

    work page

  2. [2]

    (Integers a and b are called relatively prime if the greatest common divisor of a and b is 1.) FMC: theorem test (n : N) (h0 : 2 ≤ n) : Finset.sum (Finset.filter (\lambda ab : N × N => ab.1 < ab.2 ∧ ab.2 ≤ n ∧ ab.1 + ab.2 > n ∧ Nat.gcd ab.1 ab.2 = 1) (Finset.product (Finset.Icc 1 n) (Finset.Icc 1 n))) (\lambda ab => 1 / (ab.1 * ab.2 : Q)) = 1 / 2 := by so...

    work page 2000

  3. [3]

    Interdisciplinary Potential : Does the statement offer opportunities for interdisciplinary research, connecting mathematics with other fields such as computer science, physics, or biology? Interdisciplinary projects often garner wide interest

    work page

  4. [4]

    Community Needs and Gaps: Does the statement fill an identified need or gap within the Lean4 community or the broader mathematical community? Addressing these needs directly correlates with interest

    work page

  5. [5]

    Analysis

    Innovativeness: How innovative is the statement? Does it propose new methods, concepts, or applications? Innovation drives interest and engagement. Customize your evaluation for each problem accordingly, assessing it as’excellent’,’good’, ’above average’,’fair’ or’poor’. You should respond in the following JSON format for each statement: {"Analysis ": (Pr...

    work page

  6. [6]

    URL https://openreview.net/forum? id=Vcw3vzjHDb. Yu, Z., Peng, R., Ding, K., Li, Y ., Peng, Z., Liu, M., Zhang, Y ., Yuan, Z., Xin, H., Huang, W., Wen, Y ., Zhang, G., 10 FMC: Formalization of Natural Language Mathematical Competition Problems and Liu, W. Formalmath: Benchmarking formal mathe- matical reasoning of large language models, 2025. URL https://...

    arXiv 2025

  7. [9]

    Complexity and Depth : Is the statement complex enough to challenge existing theories and methodologies, yet deep enough to provide significant insights or advancements? Complexity and depth showcase Lean4’s capabilities and attract interest

    work page

  8. [388]

    DeepSeek-AI

    Springer, Cham, July 2015. DeepSeek-AI. Deepseek-r1: Incentivizing reasoning capa- bility in llms via reinforcement learning, 2025a. URL https://arxiv.org/abs/2501.12948. DeepSeek-AI. Deepseek-v3 technical report, 2025b. URL https://arxiv.org/abs/2412.19437. Dong, K. and Ma, T. Stp: Self-play llm theorem provers with iterative conjecturing and proving, 20...

    arXiv 2015

Show all 12 references
  1. [1993]

    org/CorpusID:27548688

    URL https://api.semanticscholar. org/CorpusID:27548688. Paulson, L. C. Experience with Isabelle : A generic the- orem prover. Technical Report UCAM-CL-TR-143, University of Cambridge, Computer Laboratory, Au- gust 1988. URL https://www.cl.cam.ac.uk/ techreports/UCAM-CL-TR-143....

    1988 arXiv

  2. [2020]

    ISBN 9781713829546

    Curran Associates Inc. ISBN 9781713829546. Chowdhery, A., Narang, S., Devlin, J., Bosma, M., Mishra, G., Roberts, A., Barham, P., Chung, H. W., Sutton, C., Gehrmann, S., Schuh, P., Shi, K., Tsvyashchenko, S., Maynez, J., Rao, A., Barnes, P., Tay, Y ., Shazeer, N., Prabhakaran,...

    2023 arXiv

  3. [2023]

    org/CorpusID:263609132

    URL https://api.semanticscholar. org/CorpusID:263609132. 9 FMC: Formalization of Natural Language Mathematical Competition Problems Huang, Y ., Lin, X., Liu, Z., Cao, Q., Xin, H., Wang, H., Li, Z., Song, L., and Liang, X. MUSTARD: Mastering uni- form synthesis of theorem and p...

  4. [2024]

    URL https://openreview.net/forum? id=8xliOUg9EW. IMOmath. Problems from olympiads. https: //imomath.com/index.cgi?page= problemsFromOlympiads, 2025. Accessed: 2025-03-14. Islam, N., Islam, Z., and Noor, N. A Survey on Opti- cal Character Recognition System. arXiv e-prints, art...

    2025 doi arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.