1 Introduction↩︎

Auto-formalization is the task of automatically translating informal mathematical content into a formal language that can be processed by a theorem prover, such as Rocq [1], Lean [2], or Isabelle [3]. Because ordinary mathematical statements and proofs are written in a mixture of natural language and notation, their intended semantics may be underspecified and intermediate inferential steps are often left implicit. Therefore, auto-formalising mathematical content into a trusted theorem prover can greatly reduce the difficulty of verifying its correctness, while also making mathematical knowledge more reusable and accessible.

Recent advances in large language models (LLMs) have led to renewed interest in auto-formalization. Since these models are increasingly capable of processing both natural language and formal proof languages, they can be fine-tuned or directly prompted to generate formal statements from informal ones. Such capability can be further improved in several ways. For instance, models can be post-trained on synthetically generated informal-formal pairs [4], [5], augmented with retrieved formal definitions from libraries [6], [7], or embedded in an iterative refinement loop that uses feedback from the theorem prover [8], [9].

Despite the progress, auto-formalization remains intrinsically difficult. A major source of such difficulty is the fundamental discrepancy between informal mathematical writing and the formal languages used by existing theorem provers, as shown in Figure 1. We can observe that the Mizar [10] and Lean proof language often require a single informal proof step to be decomposed into several explicit declarations, assumptions, and proof obligations. For example, the informal phrase “Let \(x_n = a^{n+1} \;(0 < a < 1)\)” must be expanded into separate formal steps, including an explicit construction of the existence of such an \(a\). Similarly, the phrase “when \(n \to +\infty\)” can no longer remain a syntactic modifier attached to the statement, but must be incorporated into a formal proposition. Besides, ordinary mathematical notation must be resolved into specific library definitions, such as the scheme SEQ_1:sch 1 from the Mizar Mathematical Library [11], and the neighbourhood filter \(\mathcal{N} \;0\) from Mathlib [12].

This discrepancy challenges auto-formalization in two ways. First, it requires LLMs to bridge a substantial representational gap between informal mathematical text and formal proof languages. The scarcity of formal data further exacerbates this problem, especially for target formal languages with limited available corpora, such as those used by proof assistants with smaller libraries or user communities, as well as domain-specific formal languages.

Second, it makes the evaluation of semantic consistency non-trivial, i.e., determining whether the generated formal statement preserves the intended meaning of the original informal statement. Existing methods either rely on the availability of a reference formalization [7], [13] or use LLMs or human experts as judges, making the evaluation difficult to carry out. This issue has already had practical consequences. For example, Ospanov et al. [14] report discrepancies between the informal and formal statements for more than half of the problems in the miniF2F benchmark [15], thereby compromising the reliability of some previous evaluation results.

1.0.0.1 Overview of the Approach

To address these difficulties at a more fundamental level, we propose using a Relaxed Natural Formal Language (Relaxed NFL) as the target language for LLM-based auto-formalization. The Relaxed NFL is designed to remain as close as possible to natural mathematical language, so that auto-formalization into it resembles a structured normalization of informal mathematical text, rather than a full elaboration into a theorem prover language. This reduces the reasoning burden on LLMs and makes auto-formalization largely independent of the choice of a particular formal system.

The Relaxed NFL has a formally specified syntax, which enables it to be parsed and processed by machines. However, since it deliberately preserves part of the ambiguity, implicitness, and context dependence of informal mathematical writing, it is not suitable to be used directly as a verification target, but only as an intermediate representation of proof. We therefore elaborate the Relaxed NFL into a Core NFL with formally defined semantics, using a rule-based procedure supplemented by LLM-generated heuristics. These elaboration steps isolate the discrepancy between informal mathematical writing and the target formal system, which constitutes the main difficulty of auto-formalization. At the same time, since the input and output of each step can be formally specified, the overall process remains controllable and verifiable even when LLMs are involved.

From the Core NFL, we generate proof gaps, i.e., verification conditions whose validity is sufficient to verify the correctness of the proof. We discharge these proof gaps by prompting LLMs to synthesize proof scripts written in a domain-specific language. Beyond standard tactic operations such as case analysis, term rewriting, quantifier instantiation, and lemma application, the language provides commands for invoking theorem libraries and domain-specific solvers implemented as part of our system.

Figure 2 gives an overview of the entire auto-formalization pipeline.

1.0.0.2 Contributions

The contributions of this paper are summarized as follows:

• We propose a novel approach to LLM-based auto-formalization based on an intermediate representation that resembles informal mathematical writing.

• We study how to turn this intermediate representation into a semantically well-defined formal proof, and develop a verifiable elaboration procedure.

• We study how proof gaps generated along this pipeline can be effectively discharged by combining LLM-guided proof search with theorem library support and domain-specific solvers.

• We give concrete designs of our Relaxed NFL, Core NFL, and the domain-specific tactic language.

1.0.0.3 Organization of the Paper

The rest of this paper is organized as follows. Section 2 presents the Relaxed and the Core NFL, as well as the LLM-based auto-formalization process into Relaxed NFL. Section 3 demonstrates the elaboration of the Relaxed NFL into the Core NFL via three representative steps: notation resolution, problem-solving translation, and implicit variable scope resolution. Section 4 explains how proof gaps are generated from the Core NFL and subsequently discharged. Section 5 evaluates whether LLMs can reliably generate Relaxed NFL proofs under different settings. Finally, Sections 6 and 7 are devoted to related work and conclusions, respectively.

2 Natural Formal Language↩︎

In principle, natural formal language is intended to be extensible and can be instantiated in different mathematical domains. The particular natural formal languages presented in this paper are designed with reference to the proof structures, notation, and mathematical knowledge appearing in the textbook Problems in Mathematical Analysis by B. P. Demidovich [16].

The remainder of this section is organized as follows. We first briefly introduce the Relaxed NFL, then describe how informal mathematical proofs can be auto-formalized into the Relaxed NFL by using LLMs. Finally, we present the Core NFL, whose formal semantics is defined by a proof-gap generation function.

2.1 The Relaxed Natural Formal Language↩︎

The Relaxed NFL remains close to informal mathematical writing in two respects. First, it preserves the common reasoning patterns of informal proofs, so that the overall proof structure is largely maintained after auto-formalization. Second, it allows partially specified terms and propositions by retaining informal mathematical writing without requiring every expression to be resolved to a precise definition in a specific library.

As an example, Appendix 8 presents the Relaxed NFL formalization of an IMO functional-equation problem. As shown in this example, the Relaxed NFL is a declarative-style proof language. Among other things, user can introduce new symbols, derive intermediate conclusions, reason locally under assumptions, and solve equations.

The Relaxed NFL serves only as a surface syntax for LLM-based auto-formalization. Terms in the Relaxed NFL do not yet have fully precise mathematical meanings at this stage. Some notations may remain ambiguous, and information on variable scopes may be left implicit, as shown by the occurrence of free variables in expressions. These partially specified expressions are later resolved into precise mathematical objects through elaboration, as described in Section 3.

The detailed grammar of the Relaxed NFL is given in Appendix 9. The non-terminal <program> can be either a proof problem or a solving problem. They share the same reasoning steps, but are translated into the Core NFL differently. The non-terminal <term> represents mathematical propositions and expressions. We omit its grammar here and introduce the relevant fragments in Section 3 when needed.

2.2 Auto-Formalization into the Relaxed NFL↩︎

We instruct LLMs to translate informal mathematical content into the Relaxed NFL in two ways: in-context learning and fine-tuning.

For in-context learning, the prompt first provides the complete grammar of the Relaxed NFL, followed by 16 examples that serve as few-shot demonstrations. The model is then asked to translate the input into the target language. We then use the obtained informal-formal pairs as supervised training data, and perform LoRA fine-tuning [17] so that the model learns the grammar of the Relaxed NFL more directly.

2.3 The Core Natural Formal Language↩︎

The Core NFL is an internal proof language obtained by elaborating the surface-level constructs of the Relaxed NFL into a small number of primitive proof steps over formally specified terms. Unlike the Relaxed NFL, the Core NFL has a precisely defined semantics, and captures the information necessary for generating proof gaps.

We define the abstract syntax of the Core NFL as follows. We assume two syntactic categories: \(\mathsf{Term}\), whose elements represent mathematical expressions and propositions in the Core NFL, and \(\mathsf{Method}\), whose elements represent proof methods, with a distinguished element \(\varnothing_{\mathsf{M}}\) denoting the empty method. We write \(\mathsf{Term}^{*}\) for the set of finite, possibly empty sequences of terms.

Based on this, we define the set of proof states \(\mathsf{PState}\) by \[\mathsf{PState} = \mathsf{Term}^{*} \times \mathsf{Term}.\] We write a proof state consisting of a sequence of assumptions \(\Gamma \in \mathsf{Term}^{*}\) and a proof goal \(G \in \mathsf{Term}\) in sequent form as \(\Gamma \vdash G\).

Let \(\mathsf{Proof}\) be the least set satisfying \[\begin{align} \mathsf{Proof} = \;& \{\mathsf{Forward}(M,P,\pi) \mid M \in \mathsf{Method},\;P \in \mathsf{Term},\;\pi \in \mathsf{Proof}\} \\ \cup \;& \{\mathsf{Backward}(M,P,\pi) \mid M \in \mathsf{Method},\;P \in \mathsf{Term},\;\pi \in \mathsf{Proof}\} \\ \cup \;& \{\mathsf{Subgoal}(P,\pi_1,\pi_2) \mid P \in \mathsf{Term},\;\pi_1,\pi_2 \in \mathsf{Proof}\} \\ \cup \;& \{\mathsf{QED}\}. \end{align}\] The set of Core NFL program \(\mathsf{Program}\) is then defined by \[\mathsf{Program} = \mathsf{PState} \times \mathsf{Proof}.\]

The constructors of \(\mathsf{Proof}\) are interpreted as follows:

• \(\mathsf{Forward}(M,P,\pi)\) derives the proposition \(P\) from the current proof state using the method \(M\), adds it to the available assumptions, and then continues with the proof \(\pi\).

• \(\mathsf{Backward}(M,P,\pi)\) reduces the current proof goal to the proposition \(P\) using the method \(M\), and then continues with the proof \(\pi\).

• \(\mathsf{Subgoal}(P,\pi_1,\pi_2)\) introduces the proposition \(P\) as an intermediate subgoal, proves it by \(\pi_1\), adds it to the available assumptions, and then continues with the proof \(\pi_2\).

• \(\mathsf{QED}\) terminates the proof, indicating that the current proof goal is derivable from the available assumptions.

A Core NFL program is therefore a pair \(\mathcal{P} = (\sigma,\pi)\), where \(\sigma \in \mathsf{PState}\) represents the current proof state, and \(\pi \in \mathsf{Proof}\) represents the proof to be executed from that state.

3 Elaborating the Relaxed NFL into the Core NFL↩︎

In this section, we present how the Relaxed NFL is elaborated into the Core NFL in a verifiable way. Such elaboration generally cannot be achieved by purely syntactic transformation of the proof. Instead, we often have to perform semantic analysis in order to recover information that is left implicit. Some of the simple cases can be formulated as deterministic rules, while others require a closer analysis of the proof and may even involve inferring the author’s intended meaning. In such cases, we use LLMs to give heuristics, while keeping the elaboration step verifiable by placing models inside a suitable harness. For example, the model may be restricted to choosing among a finite set of candidates generated by deterministic rules, or its output may be required to pass a dedicated checker before being accepted.

Since different mathematical domains use different notations and proof writing conventions, and tolerate different degrees of implicitness, the concrete elaboration process is dependent on the domain. In this section, we focus on mathematical analysis and present three representative elaboration steps extracted from our implementation. They exemplify three different levels at which ambiguity and implicitness arise in informal mathematical writing: the term level, the proof-step level, and the proof-state level.

Because the Core NFL can be regarded as a restricted fragment of the Relaxed NFL, we present the elaboration steps in this section as transformations on the Relaxed NFL itself. Each step resolves certain ambiguity or implicitness, thereby moving the proof closer to the Core NFL fragment.

3.1 Notation Resolution↩︎

A common source of ambiguity in informal mathematical writing is notation overloading, where the same notation may denote different mathematical objects. A simple example is the notation \(|x|\). Depending on the meaning of \(x\), \(|x|\) may denote the absolute value of a real number, or the cardinality of a set. Consequently, the surface syntax \(|x|\) in the Relaxed NFL does not automatically resolve to a Core NFL term by itself.

In order to perform notation resolution, we first need to augment the definition of terms in the Relaxed NFL with the following constructs:

Here, \(|\cdot|\) is the overloaded surface notation, while \(\mathsf{Abs}(\cdot)\) and \(\mathsf{Card}(\cdot)\) are disambiguated forms that can be deterministically translated into the corresponding Core NFL terms, namely the absolute value of a real number and the cardinality of a set. The predicates \(\mathsf{IsReal}\) and \(\mathsf{IsSet}\) record information about whether a term has been treated as a real number or as a set. They are not part of a static type system for Relaxed NFL, but annotations used to guide the interpretation of overloaded notation. In this respect, they are similar in spirit to Mizar’s soft type system [18].

We perform a static analysis over the Relaxed NFL and maintain an environment that stores such annotations. These annotations may come from two sources.

First, they may be introduced by the LLM during the initial auto-formalization process. The prompts are designed to encourage the LLM to preserve explicit information from the informal proof about what kind of mathematical object a term denotes. For example, the informal phrase “for every real number \(t\)” is supposed to be translated into the Relaxed NFL by introducing \(t\) together with the annotation \(\mathsf{IsReal}(t)\).

Second, our system may infer them by constraint propagation over such annotations. It derives constraints from operator signatures and records the corresponding annotations in the environment. For example, if an operator expects a set argument and is applied to \(t\), the constraint \(\mathsf{IsSet}(t)\) is generated.

After constraint propagation, the elaborator checks each unresolved overloaded notation. When the environment determines a unique interpretation, the notation is replaced by the corresponding disambiguated form. For instance, \(|t|\) is resolved as \(\mathsf{Abs}(t)\) if \(\mathsf{IsReal}(t)\) is available, and as \(\mathsf{Card}(t)\) if \(\mathsf{IsSet}(t)\) is available. Otherwise, the system queries the LLM with instructions, the surrounding proof context, and the finite set of remaining candidate interpretations, asking it to select the intended one.

3.2 Problem-Solving Translation↩︎

In addition to theorem proving, the Relaxed NFL also supports problem-solving. Problem-solving does not merely require proving a given proposition. Rather, it requires constructing an answer together with a proof that the answer is correct [19], [20]. For example, consider a Relaxed NFL program of the form: \[\texttt{Find all x such that P(x) \{ ... \}}\]

When it terminates, we should be able to identify a candidate solution set \(S\) and prove that \(S\) is exactly the set of all solutions. Once \(S\) has been determined, the ending of the problem-solving step is reduced to the following step: \[\texttt{We have forall (x), x in S <==> P(x)}\]

However, the candidate solution set \(S\) cannot be recovered at the syntactic level alone. This is because the reasoning steps of problem-solving may not all preserve logical equivalence with the original constraint \(P(x)\). Some may only derive a sufficient or necessary condition, and such steps are not distinguishable from their surface syntax alone. Therefore, identifying the exact solution set is a semantic task, as it depends on whether the derived candidates genuinely satisfy the original constraint.

This task is well suited to LLMs, because the model only needs to propose a candidate answer, whose validity can be verified symbolically. Thus, we use in-context learning to infer the exact candidate solution set for each problem-solving task by providing the model with instructions and the surrounding proof context. Other kinds of problem-solving steps are handled analogously.

In some cases, we explicitly check whether the candidates obtained satisfy the constraints. For example, consider a Relaxed NFL program of the form: \[\begin{array}{l} \texttt{Solve the system of equations P(x), Q(x) \{} \\ \texttt{\;\;... After checking, x = x0 satisfies the constraints} \\ \texttt{\}} \end{array}\] This can be translated into a step asserting that the checked candidate satisfies the original equations: \[\begin{array}{l} \texttt{Solve the system of equations P(x), Q(x) \{} \\ \texttt{\;\;... We have P(x0) and Q(x0)} \\ \texttt{\}} \end{array}\]

3.3 Implicit Variable Scope Resolution↩︎

Informal mathematical writing often omits parts of the information on the scope of variables. In particular, adjacent steps may share locally introduced variables and conditions without explicitly specifying their scope. For example, consider the following simplified Relaxed NFL proof adapted from Appendix 8:

Solve: Find all f such that
  ...,
  forall (x, y in Real),
    f(x - f(y)) = f(f(y)) + x * f(y) + f(x) - 1

Solution:
   Set f(0) = c
   ...
1. We have f(x) = frac(c + 1, 2) - frac(x ^ 2, 2)
2. [@method By x ^ 2 = (-x) ^ 2 @]
   We have f(x) = f(-x)
3. We have f(c) = f(-c)
4. We have f(c) = f(c) + c - 1
5. We have c = 1
6. We have f(x) = 1 - frac(x ^ 2, 2)

Here, the same name \(x\) occurs free in Steps 1, 2, and 6, suggesting that these occurrences may refer to the same variable and requiring the current proof context to be interpreted within the scope of \(x\), which has two semantic implications.

First, variable scopes determine the interpretation of a term written in the Relaxed NFL. The declaration forall (x, y in Real) at the beginning of the problem provides evidence that its proof steps may enter the scope of a universally quantified real variable \(x\). Thus, Step 1 should be interpreted as deriving the closed proposition \(\forall x \in \mathbb{R},\, f(x)=\frac{c+1}{2}-\frac{x^2}{2}\). Similarly, Step 2 should be interpreted as deriving \(\forall x \in \mathbb{R},\, f(x)=f(-x)\). In this sense, the interpretation of a surface syntax term is determined by the current variable scope.

One may be tempted to think that this interpretation can always be obtained simply by closing the free variables syntactically occurring in the term. We show in the following paragraphs that this is not the case.

Second, variable scopes may also suggest how a proposition is derived, which in turn affects the interpretation of a term written in the Relaxed NFL. For example, for an arbitrarily fixed \(x \in \mathbb{R}\), Step 1 gives \(f(x)=\frac{c+1}{2}-\frac{x^2}{2}\). Together with Step 5, namely \(c=1\), it yields Step 6, namely \(f(x)=1-\frac{x^2}{2}\). Since the interpretation of Step 6 is still deriving the universal proposition \(\forall x \in \mathbb{R},\, f(x)=1-\frac{x^2}{2}\), rather than properties about one particular \(x\) in the current scope. What happens here is that, when \(c=1\), we prove \(\forall x \in \mathbb{R},\, f(x)=\frac{c+1}{2}-\frac{x^2}{2}\) \(\Rightarrow\) \(f(x)=1-\frac{x^2}{2}\) in order to justify \((\forall x \in \mathbb{R},\, f(x)=\frac{c+1}{2}-\frac{x^2}{2})\) \(\Rightarrow\) \((\forall x \in \mathbb{R},\, f(x)=1-\frac{x^2}{2})\), which constitutes a form of local derivation carried out within the scope of \(x\).

However, being in the same scope for \(x\) does not mean that the derivation is always local in the above sense. For example, in deriving Step 2 from Step 1, what is proved is the implication \((\forall x \in \mathbb{R},\, f(x)=\frac{c+1}{2}-\frac{x^2}{2})\) \(\Rightarrow\) \((\forall x \in \mathbb{R},\, f(x)=f(-x))\) itself, rather than \(\forall x \in \mathbb{R},\, f(x)=\frac{c+1}{2}-\frac{x^2}{2}\) \(\Rightarrow\) \(f(x)=f(-x)\), which in fact does not hold.

Similarly, when multiple variables are present in the scope, some of them may not occur freely in the derived surface syntax term, but a non-local derivation as shown in the previous paragraph will still make the interpretation to be quantified by these variables. It demonstrates that determining the precise interpretation of surface syntax terms which contains free variables involves a semantic analysis as to the actual reasoning pattern of the proof (local/non-local), instead of a syntactic analysis of free variables. Consequently, we delegate the resolution of implicit variable scopes to LLMs.

In order to perform implicit variable scope resolution, we first need to augment definition of proofs and terms in the Relaxed NFL with the following constructs:

The construct [@scope ... @] allows the LLM to explicitly annotate the implicit variable scope via <local_action_step> in the Relaxed NFL. The construct [@free ... @] marks the free variables occurring in a term, it is precomputed and annotated to the Relaxed NFL proof given to the LLM, helping it to infer the implicit scope covering the step.

The output of this elaboration step is then verified by a deterministic checker. The checker ensures that all the annotated free variables occur within a matching scope, and that no other part of the proof has been modified.

Finally, we eliminate the explicit variable scope annotation in the Relaxed NFL as in Figure 3. This is done by adding the content of variable scope annotation to every terms in the scope as quantifiers and premises.

4 Generating and Discharging Proof Gaps↩︎

In this section, we define the semantics of Core NFL programs. Rather than interpreting an element of \(\mathsf{Program}\) as a complete formal proof, we interpret it as a procedure that generates a collection of proof gaps. These proof gaps must subsequently be discharged by a trusted backend in order for the whole proof to be certified.

4.1 The Proof Gap Generator↩︎

A proof gap consists of a proof method together with a proof state. Formally, we define the set of proof gaps \(\mathsf{Gap}\) by: \[\mathsf{Gap} = \mathsf{PState} \times \mathsf{Method}.\] We write a proof gap consisting of a proof state \((\Gamma,G) \in \mathsf{PState}\) and method \(M \in \mathsf{Method}\) in sequent form as \(\Gamma \vdash_{M} G\). It represents the obligation of deriving the goal \(G\) from the available assumptions \(\Gamma\) using the method \(M\).

We denote by \(\Gamma\,P\) the sequence obtained by appending \(P\) to the end of \(\Gamma\). The proof gap generator for the Core NFL is a function \[\mathsf{PGG} : \mathsf{PState} \times \mathsf{Proof} \longrightarrow \mathcal{P}_{\mathrm{fin}}(\mathsf{Gap}),\] defined by structural recursion on the proof as follows: \[\begin{alignedat}{2} &\mathsf{PGG}(\Gamma \vdash G,\mathsf{Forward}(M,P,\pi)) &\;= {}& \{\Gamma \vdash_{M} P\} \cup \mathsf{PGG}(\Gamma\,P \vdash G,\pi), \\[0.6em] &\mathsf{PGG}(\Gamma \vdash G,\mathsf{Backward}(M,P,\pi)) &\;= {}& \{\Gamma\,P \vdash_{M} G\} \cup \mathsf{PGG}(\Gamma \vdash P,\pi), \\[0.6em] &\mathsf{PGG}(\Gamma \vdash G,\mathsf{Subgoal}(P,\pi_1,\pi_2)) &\;= {}& \mathsf{PGG}(\Gamma \vdash P,\pi_1) \cup \mathsf{PGG}(\Gamma\,P \vdash G,\pi_2), \\[0.6em] &\mathsf{PGG}(\Gamma \vdash G,\mathsf{QED}) &\;= {}& \{\Gamma \vdash_{\varnothing_{\mathsf{M}}} G\}. \end{alignedat}\]

4.2 Discharging Generated Proof Gaps↩︎

A Core NFL program is certified by checking all generated proof gaps. We define two functions \[\mathsf{CheckGap} : \mathsf{Gap} \to \{\bot,\top\}, \qquad \mathsf{CheckProgram} : \mathsf{Program} \to \{\bot,\top\},\] such that \[\forall \, (\sigma,\pi) \in \mathsf{Program},\, \mathsf{CheckProgram}(\sigma,\pi) = \bigwedge_{\mathcal{G} \in \mathsf{PGG}(\sigma,\pi)} \mathsf{CheckGap}(\mathcal{G}).\] Thus, for a Core NFL program \(\mathcal{P}\), \(\mathsf{CheckProgram}(\mathcal{P}) = \top\) means that all the generated proof gaps are successfully discharged.

4.2.1 Tactic Language for Proof Gaps↩︎

Since the Core NFL inherits the reasoning structure of the informal proof, the generated proof gaps may still contain non-trivial intermediate reasoning. As a result, relying only on automatic theorem proving techniques is often insufficient.

To address this issue, we use LLMs to facilitate the proof search. Concretely, we design a domain-specific tactic language that operates on individual proof gaps. Given a proof gap, the LLM is asked to synthesize a proof script in this language, which specifies a sequence of commands that either close the gap or reduce it to simpler subgaps. The method annotations in the Relaxed NFL, corresponding to the non-terminal <method> in Appendix 9, are used to provide proof search hints.

The main commands of the tactic language are summarized in Table 1. Most of them correspond to standard proof-state transformations in tactic-based proof languages. The last three commands are more special: auto_solve and auto_replace provides a higher level of automation by invoking our domain-specific solvers to close proof gaps directly or replace a term with a semantically equivalent one. get_prop retrieves and instantiates propositions from our theorem libraries, allowing the model to use established theorems without reconstructing them from scratch.

4.2.2 Theorem Libraries and Domain-Specific Solvers↩︎

The theorem libraries contain formalized propositions extracted from Problems in Mathematical Analysis, together with commonly used facts about sets, inequalities, elementary functions, limits, etc.

The domain-specific solvers are designed to discharge recurring proof gap patterns for which effective decision procedures are available. Rather than being used in isolation, these solvers are composed automatically. Each solver may close a proof gap directly or generate new subgaps, which can in turn be handled by other solvers. This is implemented as a breadth-first search. The main solvers are summarized in Table 2.

5 Evaluation↩︎

We evaluate the learnability of the Relaxed NFL as a target language for LLM-based auto-formalization. We report pass@1 and pass@3. An auto-formalization attempt is counted as a pass if it can semantically yield semantically well-defined proof gaps, while the discharge of these proof gaps is not included in this evaluation. For each problem, we sample three independent candidates from the model. The pass@1 rate is the proportion of problems for which the first generated candidate is counted as a pass, while the pass@3 rate is the proportion of problems for which at least one of the three generated candidates is counted as a pass.

Our dataset contains 3600 problems extracted by OCR from Problems in Mathematical Analysis, covering major topics in elementary mathematical analysis, including limits, continuity, differentiation, integration, series, and multivariable calculus.

We first use Qwen3-235B-A22B-Instruct [21], a large MoE model with 235B total parameters and 22B activated parameters, for the few-shot auto-formalization described in Section 2.2. Without chain-of-thought prompting (CoT), the model achieves 44.4% pass@1 and 72.3% pass@3. With CoT, the rates increase to 70.3% pass@1 and 90.4% pass@3.

We then select 2,000 correctly generated informal-formal pairs from this stage as supervised training data, and use the remaining examples as the test set. Finally, we fine-tune Qwen2.5-7B-Instruct [22], a smaller dense model from an earlier generation of the Qwen series, with LoRA, using rank \(r=128\), scaling factor \(\alpha=256\), and learning rate \(\eta=10^{-4}\). The fine-tuned model achieves 83.6% pass@1 and 89.9% pass@3. The results are summarized in Table 3.

These results show that Relaxed NFL proofs can be reliably generated by LLMs. In the few-shot prompting experiments, we observe that many failed samples are caused by the model drifting toward other formal languages, such as LaTeX-like notation. This suggests that these failures mainly reflect the model’s prior bias toward familiar mathematical syntaxes, rather than an intrinsic difficulty of learning the Relaxed NFL grammar. When the model is allowed to reason explicitly about the target grammar, it is less likely to drift away from Relaxed NFL, as suggested by the improvement brought by CoT.

More importantly, the fine-tuning result shows that the Relaxed NFL can be learned by smaller models with a lightweight training method and limited training data. Using only 2,000 informal-formal pairs and LoRA fine-tuning, Qwen2.5-7B-Instruct achieves a higher pass@1 rate than the much larger Qwen3-235B-A22B-Instruct with CoT, and a comparable pass@3 rate. This suggests that a suitable target language can substantially reduce the difficulty of LLM-based auto-formalization.

6 Related Work↩︎

6.0.0.1 Theorem-Proving Large Language Models

One important role of auto-formalization is to synthesize large amounts of formal proof data. Since the available formal proof corpora are relatively scarce, auto-formalization has become an essential component in the training pipelines of theorem proving LLMs, i.e., LLMs whose primary goal is to prove theorems in proof assistants. For example, the post-training data of DeepSeek-Prover [23], Goedel-Prover [24], and AlphaProof [25] all contain a large number of auto-formalized Lean 4 proofs.

However, existing work on theorem-proving language models mainly focuses on exploring more effective post-training methods and proof-search strategies. For instance, DeepSeek-Prover-V2 [26] uses reinforcement learning to help the model decompose a problem into subgoals. Other systems improve the quality of the feedback available to the model. For instance, Seed-Prover [27] combines Lean compiler feedback, proved lemmas, and self-summarization to refine generated proofs, while LEGO-Prover [28] maintains a growing library of verified lemmas and uses them as skills during inference. In contrast, relatively less attention has been paid to whether the reasoning ability of LLMs can be improved by carefully designing the target formal representation itself, or to what kind of language is suitable for mathematical reasoning by LLMs while still remaining machine-checkable. In this respect, our work is complementary to these systems.

6.0.0.2 Natural-Language-Like Formal Languages

Proof languages that aim to resemble natural language, or that take readability as a design goal, are usually described as declarative-style proof languages. Unlike term-style or procedural-style proof languages, they allow users to write proofs by explicitly stating assumptions, intermediate claims, and local arguments, which are common structures in informal mathematical writing. Many theorem provers support such declarative style. For example, Isabelle’s Isar [29] language represents proofs as structured mathematical texts. It supports nested proof contexts and the introduction of local variables, but its proof contexts are still tied to the current proof obligation, and local variables and assumptions cannot be introduced with the same flexibility as in informal mathematical writing.

Lean’s verbose-lean4 language [30] combines declarative and procedural styles. It provides declarative constructs such as have, while also allowing users to manipulate the proof state through a more natural-language-like surface syntax that is subsequently elaborated into tactics. However, it has limited support for structured proofs. For example, nested subproofs are mainly expressed through by-blocks, whose contents must be written as tactics rather than in the same declarative style. The Mizar proof language [10] and Naproche’s ForTheL [31] also follow a declarative style close to conventional mathematical prose. Previous work has shown that such natural-language-like proof languages can improve LLM-based auto-formalization. For instance, Draft, Sketch, and Prove [32] uses natural-language drafts to generate Isar proof skeletons.

The Relaxed NFL presented in this paper not only supports structured proofs organized by introducing local variables and assumptions, but also has richer structures such as problem-solving. In this respect, the Relaxed NFL is closer to informal mathematical writing. More importantly, terms and propositions in existing proof languages usually have to refer to precise library definitions, and do not allow partially specified expressions or the occurrence of free variables, while the Relaxed NFL preserve the surface form of informal mathematical notation, allowing a degree of ambiguity and context dependence. Subsequent elaboration steps can repair term-level ambiguities and explicitly reconstruct implicit local proof contexts to eliminate free variables, thereby offloading part of the reasoning burden from LLMs during auto-formalization.

7 Conclusion↩︎

In this paper, we present an auto-formalization pipeline based on a relaxed natural formal language. The main idea is to use an intermediate representation that remains close to informal mathematical writing, instead of directly instructing LLMs to generate the formal proof language of a specific theorem prover. This design reduces the representational gap that LLMs need to bridge and makes auto-formalization less dependent on the details of a particular formal system.

We introduce the Relaxed NFL as a surface language for LLM-based auto-formalization, and the Core NFL as a semantically well-defined proof language. We then describe a verifiable elaboration pipeline from the Relaxed NFL to the Core NFL, taking notation resolution, problem-solving translation, and implicit variable scope resolution as examples.

To verify the correctness of proofs, we generate proof gaps from the Core NFL and design a dedicated domain-specific tactic language in which LLMs can generate proof scripts to discharge these gaps. We incorporate theorem libraries and domain-specific solvers as part of our system to enhance the tactic language and facilitate LLM-based proof gap discharging.

Our work demonstrates the feasibility and benefits of using a proof language closer to natural mathematical writing for auto-formalization. With a carefully designed elaboration process, the logical rigor that is intentionally left implicit in the relaxed proof language can be recovered in a controlled and verifiable way, thereby supporting proof verification. Such design not only makes the language easier for LLMs to acquire and use, but also improves the readability of formal proofs.

8 An example proof written in the Relaxed NFL↩︎

This appendix presents the Relaxed NFL formalization of a functional-equation problem from the 1999 International Mathematical Olympiad. The solution is adapted from the one available on the Art of Problem Solving website: https://artofproblemsolving.com/wiki/index.php/1999_IMO_Problems/Problem_6.

Solve: Find all f such that
  IsFunc(f),
  f : Real -> Real,
  forall (x, y in Real),
    f(x - f(y)) = f(f(y)) + x * f(y) + f(x) - 1

Solution:
  Set f(0) = c
  
  [@method Substitute x = y = 0 into forall (x, y in Real),
    f(x - f(y)) = f(f(y)) + x * f(y) + f(x) - 1 @]
  We have f(-c) = f(c) + c - 1

  Assume c = 0 holds {
    We have f(0) = f(0) - 1
    Contradiction
  }

  We have c != 0

  [@method Substitute x = f(y) into forall (x, y in Real),
    f(x - f(y)) = f(f(y)) + x * f(y) + f(x) - 1 @]
  We have c = f(x) + x ^ 2 + f(x) - 1

  Solve the system of equations c = f(x) + x ^ 2 + f(x) - 1 {
    We have f(x) = frac(c + 1, 2) - frac(x ^ 2, 2)
  }

  [@method By x ^ 2 = (-x) ^ 2 @]
  We have f(x) = f(-x)
  We have f(c) = f(-c)
  We have f(c) = f(c) + c - 1
  We have c = 1
  We have f(x) = 1 - frac(x ^ 2, 2)

9 Grammar of the Relaxed Natural Formal Language↩︎

References↩︎