# Autoformalization with Large Language Models

Yuhuai Wu1,2† &Albert Q. Jiang3 &Wenda Li3 Markus N. Rabe1 &Charles Staats1
&Mateja Jamnik3 &Christian Szegedy1 1Google Research
2Stanford University
3University of Cambridge

###### Abstract

Autoformalization is the process of automatically translating from natural
language mathematics to formal specifications and proofs. A successful
autoformalization system could advance the fields of formal verification,
program synthesis, and artificial intelligence. While the long-term goal of
autoformalization seemed elusive for a long time, we show large language
models provide new prospects towards this goal. We make the surprising
observation that LLMs can correctly translate a significant portion (25.3%) of
mathematical competition problems perfectly to formal specifications in
Isabelle/HOL. We demonstrate the usefulness of this process by improving a
previously introduced neural theorem prover via training on these
autoformalized theorems. Our methodology results in a new state-of-the-art
result on the MiniF2F theorem proving benchmark, improving the proof rate from
$29.6\%$ to $35.2\%$.

00footnotetext: Correspondence to Yuhuai Wu (yuhuai@google.com).

##  1 Introduction

_Autoformalization_ refers to the task of automatically translating from
natural language mathematics to a formal language [48, 44]. The implication of
a successful autoformalization tool is huge in both practical and
philosophical terms. It would reduce the currently excessive cost of
formalization efforts [27], and in the long-term it could connect the various
research fields that automate aspects of mathematical reasoning, such as
automated theorem proving and computer algebra, to the vast body of
mathematical knowledge exclusively written up in natural language. Moreover,
autoformalization would be a true testament to machine understanding, grasping
both the fuzziness of natural language and the preciseness of formal language.

Recent advances in large language models [7, 9] showed promising capabilities
of understanding formal languages [8, 32]. However, the existing successes are
limited to formal languages where there exists a large body of corpus on the
web (e.g., Python language). Formal mathematics data is very scarce. For
example, one of the largest formal mathematics libraries, the Archive of
Formal Proofs, is only 180MB in size, that is less than $0.18\%$ of the
training data for the large language model Codex [8]. Moreover, unlike in the
case of commonly used programming languages, where natural language docstrings
are broadly available, there is almost zero aligned data between natural
language and formal mathematics. Therefore, it is unclear the recent successes
can directly contribute to the development of autoformalization.

In this work, we explore the prospects of autoformalization with large
language models. To our surprise, we find that large language models already
have a decent capability of formalizing natural language mathematics in an
interactive theorem prover. See Figure 1 for a perfect autoformalization
example. The model not only translates into syntactically correct Isabelle
code, but also grasps the non-trivial reasoning in natural language. We
randomly pick 150 formalizations and manually evaluate their correctness.
Among them, LLMs are capable of producing 38 perfect formalizations! As an
application, we further demonstrate that autoformalization can provide useful
training data for neural theorem provers. We use autoformalized statements as
targets for proof search with a neural theorem prover for Isabelle/HOL. After
fine-tuning our neural theorem prover on the proofs it found, its success rate
on the MiniF2F benchmark [54] increases significantly, achieving a new state-
of-the-art result of 35.2% theorems proven.

Case Study 1 Question: _"Prove that there is no function $f$ from the set of
non-negative integers into itself such that $f(f(n))=n+1987$ for every $n$."_
Codex Output: theorem fixes f :: "nat \<Rightarrow> nat" assumes "\<forall> n.
f (f n) = n + 1987" shows False

Figure 1: Case study 1: An example of a perfect translation from natural
language to Isabelle code.

##  2 Related Work

Early applications of machine learning in theorem proving include the works by
Schulz [42] and Urban [45], and later, directly guiding interactive proof
assistants using machine learning techniques [14]. The revolution of deep
learning then kicked off a new wave of interest in the topic starting with
DeepMath [1, 33].

Several approaches have been suggested to address data scarcity: Imitation-
free reinforcement learning was used to avoid the need for training on human
proofs [31, 5, 14, 51]. Also, hindsight experience replay [2] was used to
generate additional training data [4]. Hahn et al. [18], Schmitt et al. [41],
Kreber & Hahn [29] and Wu et al. [52] have shown that training on synthetic
formulas can be successful for temporal logics and inequalities. Rabe et al.
[39] masked out different subexpressions from formal mathematical statements
and generated 100 training examples for each source statement. Skip-tree data
can also be used to improve the performance of neural theorem provers [21].

Wang et al. [48] explored the use of supervised and unsupervised translation
techniques for autoformalization. Supervised translation yielded interesting
results, but relied on synthetic (natural-looking) data that was generated by
the Mizar theorem prover, while we rely on models trained via self-supervised
language modeling, not trained for this particular purpose.

##  3 Background

#### Formal Mathematics

A few important and complex results of mathematics and computer science have
been formalized manually using _interactive theorem provers_ , such as the
four color theorem [15], the Kepler conjecture [19], the odd-order theorem
[16] and the verification of a microkernel [27]. This gives us almost complete
certainty about the correctness of proofs, which can be of great value to
resolve doubt about the correctness of complicated mathematical proofs or
proving certain properties of software used in safety-critical applications,
such as aircraft components [28].

These projects relied on interactive theorem provers, such as Isabelle [50],
Coq [11], HOL Light [22], and Lean [12], which are essentially programming
languages that enable users to enter their statements and proofs in a formal
language, and which can then be checked automatically for correctness.
Interactive theorem provers offer a limited amount of automation, but projects
that formalize complex problems typically span many years of tedious work by
specialists. Only in narrow domains like chip design and the verification of
drivers in operating systems has the automation of logic made sufficient
progress to find commercial applications.

Progress in autoformalization and the automation of proofs might eventually
make mathematics a universally available tool and enable a paradigm shift in
science and the development of (safety-critical) software. Our interest in
formalizing mathematics, however, has an additional aspect. We believe that
autoformalization will serve a dual purpose and will not only accelerate the
development of tools for mathematical reasoning, but also provide a means to
ground machine learning systems, enabling a positive feedback loop between
machine learning and formal systems (cf. [44]).

#### Large Language Models

Our work relies heavily on large language models (LLMs), in particular on PaLM
[9] and Codex [8]. The training goal of these models is to predict the next
word given some prefix. This allows us to train these models on arbitrary
text, which is available in vast quantities. After training the models on
hundreds of billions of words (cf. [24]), they are often able to generate
high-quality text. We can also give these models an arbitrary prefix (the
_prompt_) that they are then supposed to continue, which gives us some control
over what they generate. This has been demonstrated with news articles,
conversations, summaries, jokes, and poems. LLMs have also been evaluated on
natural language word problems on datasets such as GSM8K [10] and MATH [23],
and have been shown to make progress on these benchmarks with increasing scale
[9].

#### In-context Learning

Large language models have shown a remarkable ability to learn patterns and
tasks within the current input (context) that they are given [7]: this is
called _in-context learning_ or _few-shot learning_. For example, if we prompt
a language model with a few pairs of English and matching French sentences,
and end with a new English sentence, then the language model is very likely to
pick up on the translation task and attempt a translation of the last English
sentence. This observation has been used, for example, to achieve strong
translation performance without access to large corpora of matching sentence
pairs [20].

This allows us to specify the task of autoformalization simply by giving a
couple of example formalizations. In Section 4 we will detail how exactly we
use in-context learning for autoformalization.

##  4 Autoformalization for Mathematical Competition Problems

Inspired by the success of LLMs for synthesizing computer code by co-training
on both natural language and code on web-scale data, we explore the
capabilities of LLMs to turn natural language mathematics into formalized
theorems for the interactive theorem prover Isabelle. This can be seen as a
machine translation task (cf. [49]) in which the input language is English and
output language is formal code used by the interactive proof assistant
Isabelle [50].

We first study autoformalization in a constrained setting – formalizing
mathematical competition problem statements. This setting has the advantage
that most of the required background theory and definition has been formalized
in the current libraries of Isabelle, so that formalizations are often
possible without introducing additional definitions.

We start assessing LLMs’ abilities to do autoformalization with a case study.
We manually pick two interesting natural language mathematical statements, and
prompt PaLM models of various scales [9] as well as Codex [8] to translate
them into a formal statement in Isabelle. Next, we study a dataset in which we
have human ground truth formalizations. The dataset is a subset of the miniF2F
[23] dataset consisting of 140 algebra problems and 120 number theory
problems. Using human formalizations as the reference, we compute the BLEU
scores of the formalizations produced by several LLMs. Lastly, we perform
human evaluations on failure cases in autoformalization on 150 problems.

Note that many mathematical competition statements are often of the form in
which one asks to find the answer to a certain problem, instead of _proving_ a
given proposition. However, formal mathematical statements are in the form of
propositions, instead of questions. To transform a question into a
proposition, we append the final answer after the question:

$\texttt{\$Problem\\_Statement }\emph{The final answer is }\texttt{\$Answer}.$

The format of the prompt we use to do autoformalization is:

$\displaystyle\text{Natural language version:
}\texttt{\$Natural\\_Language\\_Statement}.$ Translate the natural language
version to an Isabelle version:

###  4.1 Mathematical Competition Datasets

MATH [23] contains in total 12,500 (7,500 training and 5,000 test) middle
school and high school mathematical competition problems. Problems are taken
from past mathematical competitions, including AMC 10, AMC 12, AIME, and more,
and many can be found at http://aops.com/community/c3158_usa_contests. The
dataset contains seven categories: algebra, pre-algebra, intermediate algebra,
number_theory, precalculus, probability, geometry. Problem statements are
written in LaTeX.

MiniF2F [54] is a recently introduced benchmark containing 488 mathematical
competition statements manually formalized by humans in three different formal
languages. Its goal is to compare and benchmark methods across different
theorem provers for machine learning research. Some of these problems come
from the valid and test set of MATH algebra and number_theory, and others come
from previous International Mathematical Olympiad competitions or
AoPS111https://artofproblemsolving.com/. Note that the Isabelle formalizations
of the miniF2F benchmark were committed to the repository during March, 2022.
According to the public information on the large language models, we think it
is highly unlikely these formalizations were included in the pre-training
corpus.

Natural language version: _"Let $z=\frac{1+i}{\sqrt{2}}$, find
$(\sum_{i=1}^{1}2(z^{i^{2}}))\cdot(\sum_{i=1}^{1}2(\frac{1}{z^{i^{2}}}))$. The
final answer is 36."_ Translate the natural language version to an Isabelle
version:

    theorem
      fixes z::complex
      assumes h0: "z = (Complex (1/sqrt 2) (1/sqrt 2))"
      shows "(\<Sum>k::nat=1..12. (z^(k^2)))
                * (\<Sum> k::nat=1..12. 1/(z^(k^2)))=36"

Natural language version: _"Determine the value of $ab$ if
$\log_{8}a+\log_{4}b^{2}=5$ and $\log_{8}b+\log_{4}a^{2}=7$. The final answer
is 512"._ Translate the natural language version to an Isabelle version:

    theorem
      fixes a b ::real
      assumes "(ln a) / (ln 8) + (ln (b^2)) / (ln 4) = 5"
              "(ln b) / (ln 8) + (ln (a^2)) / (ln 4) = 7"
            shows "a * b = 512"

Figure 2: The two few-shot examplars used in case studies: both examples are
merely an illustration of a syntactical translation from from LaTeXto
Isabelle, without much sophistication in natural language understanding or
reasoning.

###  4.2 Case Studies

#### Experimental setup

For all our experiments, we use the standard greedy decoding (i.e.,
temperature 0, $p=1$) to obtain the autoformalizations. We randomly select two
mathematical statements for constructing the prompt. No prompt engineering /
tuning is performed when constructing the prompt. The examples are shown in
Figure 2. The natural language problem statements used in the case studies are
taken from the miniF2F dataset. In the case studies below, we highlight the
output of language models in red to distinguish it from the prompt.

#### Case Study $1$ (Figure 1)

We study the example shown in Figure 1, in which we ask LLMs to autoformalize
an International Mathematical Olympiad problem222A problem from IMO 1987. in
natural language. Surprisingly, Codex is able to autoformalize the natural
language statement as an Isabelle theorem perfectly, with output given. This
is surprising for the following reasons.

First of all, the amount of Isabelle code is very scarce on the internet. The
entire AFP library, the largest formal library that contains most of Isabelle
proofs, is only 180MB in size. Even assuming that all of this data was
included in the training of Codex, this makes at most $0.18\%$ of the
pretraining data on which Codex was trained. The fact that the model can write
syntactically correct Isabelle code at all is already fascinating.

Second, there is almost zero aligned data from natural language to Isabelle on
the web. While some Isabelle files have comments, they typically only give a
very high level description of what the theory being formalized is about. So
either LLMs are able to transfer knowledge quite successfully between natural
language and formal mathematics, or the task was learned mostly via few-shot
learning.

Last but not least, the model is capable of understanding and formalizing
nontrivial reasoning. First, the model is able to formalize the non-existence
statement via proof-by-contradiction. To formalize “there is no function
$f$…”, it assumes there is such a function, and aims to prove “False”. Second,
the model understands what it means by the phrase “to itself”, and correctly
infers the domain of function: `f :: "nat \<Rightarrow> nat"`.

On the other hand, PaLM made some syntactic mistakes while getting most of the
structure of the proof correctly, with outputs shown in Appendix B.1.

#### Case Study $2$ (Figure 3)

In the next example, we ask LLMs to autoformalize a grade school mathematical
word problem. Remarkably, PaLM and Codex are both capable of formalizing the
statement perfectly. This is surprising because formalizations of grade school
math problems in interactive theorem provers are rare (if they exist at all),
as this type of mathematics is not of interest to formal mathematicians. Even
more, none of the examples in the prompt (see Figure 2) that we provide are of
this type. It is hence remarkable that the model is capable of extrapolating
to this type of statement, showing a great promise of using LLMs for
autoformalization.

To study this problem in more depth, we probe PaLM models of various sizes
(8B, 64B, 540B) with outputs shown in Appendix B.2, and notice that scale is
crucial for the LLMs ability to formalize. We observe that the 8B and 64B
models are incapable of formalizing this problem, but the largest 540B model
is able to produce a correct formalization.

Case Study 2 Question: Natural Language version: "_When all the girls at
Madeline’s school line up in rows of eight, there are seven left over. If
instead they line up in rows of four, how many are left over? The final answer
is 3._ " Translate the natural language version to an Isabelle version: PaLM
output: theorem fixes n::nat assumes "n mod 8 = 7" shows "n mod 4 = 3"

Case Study 3 Question: Natural language version: _"Let $f$ be a linear
function for which $f(6)-f(2)=12.$ What is $f(12)-f(2)?$ The final answer is
30."_ Translate the natural language version to an Isabelle version: Codex
output: theorem fixes f :: "real \<Rightarrow> real" assumes "linear f" "f 6 -
f 2 = 12" shows "f 12 - f 2 = 30"

Figure 3: Autoformalizations from natural language to Isabelle code. Left:
Case study 2 – perfect formalization by PaLM. Right: Case study 3 – incorrect
formalization by Codex.

#### Case Study $3$ (Figure 3)

In our third case study, Codex gives an incorrect formalization in Isabelle.
The mathematical statement involves a concept of “linear function”, which the
model fails to formalize correctly. Codex assumes this is already a known
concept in Isabelle, and made up a name: linear f. Can the model learn to
formalize such problems if the prompt contains an example that explains the
concept of a line? We explore this and give an affirmative answer to the
question (see Appendix B.3). Once seeing a tangentially related problem that
explains the concept of a “line”, Codex is able to perfectly formalize a
“linear function”. This shows the importance of the few shot examples we
include, and also how good a few-shot learners these models are!

#### Has the model memorized these formalizations?

Whilst we do not have access to the training set of Codex, we attempted to
find any occurrences of the formalizations produced in the case studies on the
internet. We Googled them in different variants and inspected the first page
of the search results. We tried variants with and without an “Isabelle”
prefix, with and without quotation marks and other special characters, and
also individual parts of it, such as “Isabelle "n mod 8 = 7"”, but we did not
find any occurrences of related statements. We also tested that we are indeed
able to find occurrences of Isabelle formalizations on the web with this
methodology, using pieces of formalizations picked from several websites,
including the Archive of Formal Proofs. Hence, we are confident that the model
has not memorized the formalizations it generated.

###  4.3 BLEU for Model Comparisons

The miniF2F benchmark contains 140 algebra problems and 120 number theory
problems from the MATH dataset. For these problems, we have human ground truth
formalizations in Isabelle, which gives us an evaluation set with pairs of
natural language statements (from MATH) and their formalizations. We use this
dataset to quantitatively compare different LLMs.

Given the observation about few shot learning in Case study 3, we decided to
add more relevant examples to each subject to improve the quality of
autoformalization. For each subject (i.e., algebra and number_theory), we
randomly sample 10 problems to construct the few shot prompt. The rest of the
problems are used for evaluation (i.e., 130 for algebra and 110 for
number_theory. We provide the prompt used in the Appendix A.1 and A.2.

We use PaLM models of varying sizes and Codex to perform the
autoformalization, and compute the BLEU scores of the formalizations, shown in
Table 1. Confirming our observation in Case study 2, we see a clear trend that
scaling improves translation, as the BLEU scores consistently improve when we
scale PaLM models from 8B to 540B, for both subjects. In addition, we see that
the Codex model is better at autoformalization measured by BLEU, possibly due
to the fact that Codex was trained on more formal data than PaLM.

Table 1: BLEU scores between the autoformalized statements and human formalized ground truth. Models $\backslash$ Subject | algebra | number_theory
---|---|---
PaLM 8B | 31.49 | 22.10
PaLM 64B | 43.13 | 31.43
PaLM 540B | 50.30 | 36.16
Codex | 57.13 | 43.33

###  4.4 Human Evaluation of Failure cases

To better understand LLMs’ ability to do autoformalization, we manually
inspect Codex’s autoformalizations of 150 random problems from the MATH
dataset [23]. 50 of the problem statements are sampled from the algebra
training set, 50 from number_theory and 50 from intermediate_algebra. For
algebra and number_theory, we use their corresponding prompt as in the last
section, shown in Appendix A.1 and A.2. For intermediate_algebra, we use the
prompt we used for algebra (Appendix A.1). We classify the failure modes of
these translations, shown in Table 2.

We see that out of 150 problems, Codex is capable of translating 38 problems
perfectly – a success rate of 25.3$\%$. The majority of the failures are due
to the misalignment of informal and formal definitions. For example, when
seeing the phrase “the greatest possible value”, the LLMs often fail to align
it with the function Greatest/Max in Isabelle. Another example is the failure
to align the factorial of $n$ (i.e., !n) to _fact n_ in Isabelle. Other common
failure modes include the misapplication of functions (e.g., applying a prefix
function in an infix way).

Table 2: Failure case study of 150 problems formalized by Codex. Failure cases $\backslash$ Subjects | algebra | number_theory | inter_alg
---|---|---|---
Perfect translation | 13 | 17 | 8
Incomplete/ill-formed/unclear prompt | 9 | 3 | 14
Fail to align definitions or concepts | 10 | 18 | 18
Inconsistent/missing assumption | 8 | 9 | 9
Syntactical/type error | 7 | 2 | 11
Missing definition in Isabelle | 0 | 12 | 3
Wrong application of functions | 6 | 13 | 16
Other | 6 | 2 | 1

##  5 Autoformalization for Neural Theorem Proving

To demonstrate the usefulness of the formalized statements, we explore if one
can improve neural theorem provers by training the neural models on proofs of
automatically translated theorems. In this section, we combine
autoformalization with expert iteration algorithms [3], and achieve a new
state of the art in miniF2F benchmark.

###  5.1 Expert Iteration with Autoformalization

The basic idea of expert iteration [3] is to iteratively generate a better
dataset using the model, and use the data to improve the model quality. This
allows the model to generate an even better quality of the dataset and hence a
better model, forming a self-improvement cycle.

In neural theorem proving, one way to get better quality data is to use
feedback from the proof checker to run many proof searches (or generate
multiple proofs) and check the proof attempts for correctness. Newly found
correct proofs can then be used as the new training data to improve the neural
prover [6, 37, 38]. The main critical ingredient that is needed is a set of
problem statements on which the model can perform proof search to obtain new
training data. However, unlike in Polu et al. [38], where one asks humans to
manually formalize a set of problems to get formal statements, here we use
LLMs to autoformalize the theorems in order to kick off the self-improvement
cycle.

More formally, denote a base neural theorem prover as $M_{0}$. Let the set of
autoformalized problems be $\mathcal{A}$. For each iteration $i=1\ldots N$, we
carry out the following procedure: use the language model $M_{i-1}$ with best-
first search to prove as many theorems as possible in $\mathcal{A}$, collect
the set of successful proofs $S_{i}$, concatenate successful problems from all
iterations with the formal mathematics problems to create the set
$\mathcal{A}_{i}=(\bigcup_{j\leq i}S_{i})\cup\mathcal{B}$, and fine-tune
$M_{0}$ on it for exactly one epoch to get a new model $M_{i}$. When we take
the union of successful proofs from all past iterations, we perform
deduplication by problem statements, similar to Polu et al. [38].

###  5.2 Neural Theorem Provers

To demonstrate the effectiveness of the approach, we start with a recently
introduced neural theorem prover for Isabelle, Thor [26]. The Thor agent is
fine-tuned on the PISA dataset [25] (extraction and interaction code under a
BSD license), which consists of 2.49 million proof steps from the Isabelle/HOL
library (under a BSD-style license) and the Archive of Formal Proofs (under
various licenses as described here). The model is trained with the objective
to predict the next token in a proof step, given the proof state and the last
proof step. When the ground truth proof step contains any of the keywords
metis, meson, and smt, the model learns to predict a special token <hammer>.
In evaluation, whenever the special token is emitted, Thor invokes the proof
method Sledgehammer [36] in Isabelle with a 30 second timeout.

We use a pre-trained and fine-tuned Thor agent as the base model ($M_{0}$).
The agent’s language model uses Wang [47]’s implementation (under an Apache
license 2.0) of a GPT-2 [40] style decoder-only transformer [46] model with
700M non-embedding parameters. The model has 24 layers, 24 attention heads, a
hidden dimension of 1536, and a vocabulary size of 50400. It uses the AdamW
[35] optimizer and is pre-trained on the GitHub + arXiv subsets of The Pile
[13] for 200,000 steps, with a context length of 2048 tokens. In pre-training
a warmup strategy [17] raises the learning rate linearly from 0 to $2\times
10^{-4}$ in 3,000 steps. Then a cosine learning rate scheduler [34] is used
for the rest of the pre-training, with a final learning rate of $1.2\times
10^{-5}$. The training has a global batch size of 32 sequences, or 65,536
tokens. For fine-tuning the learning rate strategy is the same, with 10,000
warmup steps, 90,000 annealing steps, maximum learning rate $3\times 10^{-4}$
and final learning rate $3\times 10^{-5}$. The global batch size is 144
sequences, or 294,912 tokens. The model’s evaluation loss reaches a minimum
after 13,000 steps and that checkpoint is used.

#### Machine specification

For experiments in this paper, we use a TPUv3 with 8 cores from Google Cloud
Platform. The Isabelle process has access to up to 32 CPU cores. Running all
the experiments in this paper requires a total of $3920$ TPU hours. Of the
$3920$ TPU hours, $3200$ are for running the proof search on the
autoformalized theorems, $240$ are for training the model on the successful
proofs, and $480$ are for evaluating the model on miniF2F.

###  5.3 Result

Table 3: Proof success rates on miniF2F. Model | _valid_ | _test_
---|---|---
PACT [21] | $23.9\%$ | $24.6\%$
FMSCL [38] | $33.6\%$ | $29.6\%$
Base model ($M_{0}$) [26] | $28.3\%$ | $29.9\%$
After $1$ expert iteration ($M_{1}$) | $36.1\%$ | $34.0\%$
After $2$ expert iterations ($M_{2}$) | $\mathbf{37.3}\%$ | $\mathbf{35.2\%}$

We use Codex with greedy decoding to formalize 3908 mathematical problems in
algebra, intermediate algebra, and number theory from the training set of MATH
[23], with the same few shot prompts used in Section 4.4. Out of them, 3363 of
the autoformalized theorems are syntactically correct. We then perform expert
iteration on this dataset.

We start with a neural theorem prover ($M_{0}$) as described in Section 5.2.
In our first iteration, $M_{0}$ proves 782 theorems, with a success rate of
$23.3\%$ (out of 3363). This gives us a new set of verified proofs to further
train the neural theorem prover. We proceed to fine-tune our neural theorem
prover in the fashion described in Section 5.1 to get a new prover ($M_{1}$).
This process is repeated in the second iteration, giving us 1011 successful
proofs from the autoformalized theorems ($30.1\%$). We fine-tuned $M_{0}$
again, but on the deduplicated concatenation of problems from PISA and
successful proofs found for the autoformalized theorems.

After each stage of fine-tuning, we evaluate the neural theorem prover on
miniF2F [54]. The results are shown in Table 3. The base model ($M_{0}$) has a
success rate of $28.3\%$ and $29.9\%$ on the validation and test fractions of
miniF2F respectively. It can be observed that the first expert iteration
increases the success rate of the neural prover by $7.8\%$ and $4.1\%$ to
$36.1\%$ and $34.0\%$ on the valid and test sets. The second iteration further
improves them both by $1.2\%$, to $37.3\%$ and $35.2\%$. By doing two expert
iterations on the autoformalized theorems, the neural prover achieves a
success rate that is $5.6\%$ higher than the previous state-of-the-art.

##  6 An Outlook on Autoformalizing Advanced Mathematics

So far, we focused on mathematical competition problems, in which we achieve
significant results using autoformalization. Not only can LLMs autoformalize
non-trivial theorems, the autoformalized theorems can also improve neural
prover performance. In this section, we take a peek into more advanced
mathematics. We hope to identify some of the limitations of our methods when
it comes to autoformalizing mathematics in the wild.

###  6.1 Autoformalization: from Natural Language to Isabelle

Autoformalization is extremely challenging in the sense that the model needs
to (1) bridge the logical gaps left in pen-and-paper proofs, (2) assume the
implicit contexts and assumptions, and (3) align informal definitions/concepts
to formal ones. This task is further complicated considering the context can
change from time to time and the same mathematical object can be formalized in
subtly different ways. In this paper, we only deal with autoformalization of
theorem statements, where the model is mainly challenged by definition
alignments. Compared to competition problems in Section 4.4, advanced
mathematical statements assume more context information that additionally
obscures the alignment.

Question: _An arbitrary product of compact spaces is compact._ Codex Output:
theorem fixes X :: "’a set set" assumes "\<forall>x \<in>X. compact x" shows
"compact (\<Prod> x \<in> X. x)" Figure 4: A formalization for an advanced
mathematical statement by Codex.

Figure 4 shows a typical case where the model fails to align the informal
definition to the formal one. Based on the notation used, the model does not
correctly distinguish between products of numbers, products of sets, and
products of topological spaces. In Isabelle, the correct conclusion for the
statement should be _compact_space (product_topology X I)_ , where $I$ is an
index set that ought to have been introduced in the _fixes_ and _assumes_
sections.

###  6.2 Informalization: from Isabelle to Natural Language

So far, we explored one direction of translation: from natural language
statement to formal statement in Isabelle. The other direction,
_informalization_ , is also of great importance for two reasons: (1) the
informal texts are much easier for humans to comprehend and communicate, and
(2) we can align translated informal statements with formal ones to create
data, and use the back-translation techniques [43] to potentially boost the
translator’s performance further. In this section, we explore Codex’s
capability of translating formal Isabelle statement to natural language.

A corpus of 38 formal-language theorems, lemmas, and definitions is selected
by an Isabelle expert. These statements are automatically translated to
informal mathematics using Codex; to see the prompt we used and the results
for all 38 examples, see Appendix A.3 and D.2. We present two examples of
informalization in Figure 5. Of the 38 examples, 36 were translated to a
reasonably coherent statement, and 29 of these statements (76%) were more-or-
less correct, giving a vastly better success rate than the 25% success rate of
formalization (Section 4.4). Our main conclusion is that for advanced
mathematics, the model is better at informalization than formalization,
showing the prospect of backtranslation style algorithms.

Note that the standard is more relaxed here since we assume a human reader
will supply the obvious context and correct mistakes when the intended meaning
is obvious (intended by the hypothetical human writer of these sentences). To
illustrate, an example of a minor “acceptable” error: assuming that “$w,z$ are
in the same connected component of the plane” when, in context, it is clear
that $w,z$ should be assumed to be in the same connected component of the
complement of a previously specified curve. (The assumption as originally
stated is trivial.) For an example of a major error: almost-perfect
translation of the Central Limit Theorem that omits the assumption of
identical distributions.

_lemma_ seteqI: "_$\mathopen{[\mkern-3.0mu[}$__$\bigwedge$_ x. x _$\in$_ A
_$\Longrightarrow$_ x _$\in$_ B;  _$\bigwedge$_ x. x _$\in$_ B
_$\Longrightarrow$_ x _$\in$_ A  _$\mathclose{]\mkern-3.0mu]}$_
_$\Longrightarrow$_ A = B" Translate the Isabelle version to a natural
language version: Codex Output: "If $A$ and $B$ are sets such that $A\subseteq
B$ and $B\subseteq A$, then $A=B$."

_lemma_ topologyI: "_$\mathopen{[\mkern-3.0mu[}$_  _$\bigwedge$_ x y.
_$\mathopen{[\mkern-3.0mu[}$_ is_open T x; is_open T y
_$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ is_open T (x  _$\cap$_ y);
_$\bigwedge$_ M.  _$\forall\,$_ m  _$\in$_ M. is_open T m  _$\Longrightarrow$_
is_open T (_$\bigcup\,$_ M)  _$\mathclose{]\mkern-3.0mu]}$_
_$\Longrightarrow$_ topology T" Translate the Isabelle version to a natural
language version: Codex Output: "If $T$ is a set and $T$ is closed under
finite intersections and arbitrary unions, then $T$ is a topology."

Figure 5: Two perfect translations from Isabelle code to natural language by
Codex.

##  7 Discussion

#### Promise of Autoformalization with LLMs

We have seen that automated formalization of informally given natural language
statements is generally possible, even with language models not trained for
this particular task. Also, automatically formalized statements are useful for
training and improving the reasoning capabilities of automated neural provers.
Our hope is that improved versions of this methodology will be capable of
enabling a positive feedback loop involving formalization and formal reasoning
that has the potential of reaching human level capabilities in both respects,
as was suggested by [44].

#### Limitations and future directions

We use a static model for the formalization process. For large-scale
autoformalization, we will need to formalize larger theories, preferably
without fine tuning the model, as training it could be cumbersome and resource
consuming. However, in order to utilize the newly added notions, the model
would need to keep whole large theories in the current context window, which
exceeds those of the current LLMs. This limits our approach to the generation
of fairly small pieces of formal mathematics and the automatic formalization
of entire theories including their definitions will require new research
ideas. One path towards this goal might be the use of continuous training or
expert iteration, cycle-consistency-based training [30, 48], or novel uses of
in-context learning. To generate larger theories we will also need neural
networks that can recall longer sequences (current LLMs are typically limited
to a few thousand words). Retrieval-augmented language models, such as the
memorizing transformer [53] offer one path to overcome this limitation.

#### Societal Impact

While the potential of creating negative societal impact through
formalizations is small, the use of LLMs always comes with risks. For example,
for deploying an autoformalization tool using LLMs we would need to consider
the inclusivity of variable and lemma names, and of the attribution of
scientific ideas.

## References

  * Alemi et al. [2016] Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban.  Deepmath - deep sequence models for premise selection.  In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett (eds.), _Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain_ , pp. 2235–2243, 2016.  URL http://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection.
  * Andrychowicz et al. [2017] Marcin Andrychowicz, Dwight Crow, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, Pieter Abbeel, and Wojciech Zaremba.  Hindsight experience replay.  In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), _Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA_ , pp. 5048–5058, 2017.  URL https://proceedings.neurips.cc/paper/2017/hash/453fadbd8a1a3af50a9df4df899537b5-Abstract.html.
  * Anthony et al. [2017] Thomas Anthony, Zheng Tian, and David Barber.  Thinking fast and slow with deep learning and tree search.  In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), _Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA_ , pp. 5360–5370, 2017.  URL https://proceedings.neurips.cc/paper/2017/hash/d8e1344e27a5b08cdfd5d027d9b8d6de-Abstract.html.
  * Aygün et al. [2021] Eser Aygün, Laurent Orseau, Ankit Anand, Xavier Glorot, Vlad Firoiu, Lei M. Zhang, Doina Precup, and Shibl Mourad.  Proving theorems using incremental learning and hindsight experience replay.  _CoRR_ , abs/2112.10664, 2021.  URL https://arxiv.org/abs/2112.10664.
  * Bansal et al. [2019a] Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy.  Learning to reason in large theories without imitation.  _CoRR_ , abs/1905.10501, 2019a.  URL http://arxiv.org/abs/1905.10501.
  * Bansal et al. [2019b] Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox.  Holist: An environment for machine learning of higher order logic theorem proving.  In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), _Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA_ , volume 97 of _Proceedings of Machine Learning Research_ , pp. 454–463. PMLR, 2019b.  URL http://proceedings.mlr.press/v97/bansal19a.html.
  * Brown et al. [2020] Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter, Christopher Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei.  Language models are few-shot learners.  In _NeurIPS_ , 2020.
  * Chen et al. [2021] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Joshua Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech Zaremba.  Evaluating large language models trained on code.  _CoRR_ , abs/2107.03374, 2021.  URL https://arxiv.org/abs/2107.03374.
  * Chowdhery et al. [2022] Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emily Reif, Nan Du, Ben Hutchinson, Reiner Pope, James Bradbury, Jacob Austin, Michael Isard, Guy Gur-Ari, Pengcheng Yin, Toju Duke, Anselm Levskaya, Sanjay Ghemawat, Sunipa Dev, Henryk Michalewski, Xavier Garcia, Vedant Misra, Kevin Robinson, Liam Fedus, Denny Zhou, Daphne Ippolito, David Luan, Hyeontaek Lim, Barret Zoph, Alexander Spiridonov, Ryan Sepassi, David Dohan, Shivani Agrawal, Mark Omernick, Andrew M. Dai, Thanumalayan Sankaranarayana Pillai, Marie Pellat, Aitor Lewkowycz, Erica Moreira, Rewon Child, Oleksandr Polozov, Katherine Lee, Zongwei Zhou, Xuezhi Wang, Brennan Saeta, Mark Diaz, Orhan Firat, Michele Catasta, Jason Wei, Kathy Meier-Hellstern, Douglas Eck, Jeff Dean, Slav Petrov, and Noah Fiedel.  PaLM: Scaling language modeling with pathways.  _CoRR_ , abs/2204.02311, 2022.  doi: 10.48550/arXiv.2204.02311.  URL https://doi.org/10.48550/arXiv.2204.02311.
  * Cobbe et al. [2021] Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman.  Training verifiers to solve math word problems.  _CoRR_ , abs/2110.14168, 2021.  URL https://arxiv.org/abs/2110.14168.
  * [11] Coq.  The Coq Proof Assistant.  http://coq.inria.fr.  URL http://coq.inria.fr.
  * de Moura et al. [2015] Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer.  The lean theorem prover (system description).  In Amy P. Felty and Aart Middeldorp (eds.), _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_ , pp. 378–388. Springer, 2015.  doi: 10.1007/978-3-319-21401-6\\_26.  URL https://doi.org/10.1007/978-3-319-21401-6_26.
  * Gao et al. [2020] Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy.  The Pile: An 800gb dataset of diverse text for language modeling.  _arXiv preprint arXiv:2101.00027_ , 2020.
  * Gauthier et al. [2021] Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish.  Tactictoe: Learning to prove with tactics.  _J. Autom. Reason._ , 65(2):257–286, 2021.  doi: 10.1007/s10817-020-09580-x.  URL https://doi.org/10.1007/s10817-020-09580-x.
  * Gonthier [2007] Georges Gonthier.  The four colour theorem: Engineering of a formal proof.  In Deepak Kapur (ed.), _Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, December 15-17, 2007. Revised and Invited Papers_ , volume 5081 of _Lecture Notes in Computer Science_ , pp. 333. Springer, 2007.  doi: 10.1007/978-3-540-87827-8\\_28.
  * Gonthier et al. [2013] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry.  A machine-checked proof of the odd order theorem.  In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (eds.), _Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings_ , volume 7998 of _Lecture Notes in Computer Science_ , pp. 163–179. Springer, 2013.  doi: 10.1007/978-3-642-39634-2\\_14.
  * Goyal et al. [2017] Priya Goyal, Piotr Dollár, Ross Girshick, Pieter Noordhuis, Lukasz Wesolowski, Aapo Kyrola, Andrew Tulloch, Yangqing Jia, and Kaiming He.  Accurate, large minibatch sgd: Training imagenet in 1 hour.  _arXiv preprint arXiv:1706.02677_ , 2017.
  * Hahn et al. [2021] Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner.  Teaching temporal logics to neural networks.  In _ICLR_ , 2021.
  * Hales et al. [2017] Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al.  A formal proof of the Kepler conjecture.  In _Forum of Mathematics, Pi_ , volume 5, pp. e2. Cambridge University Press, 2017.
  * Han et al. [2021] Jesse Michael Han, Igor Babuschkin, Harrison Edwards, Arvind Neelakantan, Tao Xu, Stanislas Polu, Alex Ray, Pranav Shyam, Aditya Ramesh, Alec Radford, and Ilya Sutskever.  Unsupervised neural machine translation with generative language models only.  _CoRR_ , abs/2110.05448, 2021.  URL https://arxiv.org/abs/2110.05448.
  * Han et al. [2022] Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu.  Proof artifact co-training for theorem proving with language models.  In _International Conference on Learning Representations_ , 2022.  URL https://openreview.net/forum?id=rpxJc9j04U.
  * Harrison [1996] John Harrison.  HOL Light: A tutorial introduction.  In Mandayam K. Srivas and Albert John Camilleri (eds.), _Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings_ , volume 1166 of _Lecture Notes in Computer Science_ , pp. 265–269. Springer, 1996\.
  * Hendrycks et al. [2021] Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt.  Measuring mathematical problem solving with the MATH dataset.  _CoRR_ , abs/2103.03874, 2021.  URL https://arxiv.org/abs/2103.03874.
  * Hoffmann et al. [2022] Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai, Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, Tom Hennigan, Eric Noland, Katie Millican, George van den Driessche, Bogdan Damoc, Aurelia Guy, Simon Osindero, Karen Simonyan, Erich Elsen, Jack W. Rae, Oriol Vinyals, and Laurent Sifre.  Training compute-optimal large language models.  _CoRR_ , abs/2203.15556, 2022.  doi: 10.48550/arXiv.2203.15556.  URL https://doi.org/10.48550/arXiv.2203.15556.
  * Jiang et al. [2021] Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu.  Lisa: Language models of isabelle proofs.  _6th Conference on Artificial Intelligence and Theorem Proving_ , 2021\.
  * Jiang et al. [2022] Albert Q. Jiang, Szymon Tworkowski Wenda Li, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik.  Thor: Wielding hammers to integrate language models and automated theorem provers.  _arXiv preprint arXiv:2205.10893_ , 2022.  URL https://arxiv.org/abs/2205.10893.
  * Klein et al. [2009] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood.  seL4: formal verification of an OS kernel.  In Jeanna Neefe Matthews and Thomas E. Anderson (eds.), _Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009_ , pp. 207–220. ACM, 2009.  doi: 10.1145/1629575.1629596.
  * Klein et al. [2018] Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby C. Murray, and Gernot Heiser.  Formally verified software in the real world.  _Commun. ACM_ , 61(10):68–77, 2018.  doi: 10.1145/3230627.  URL https://doi.org/10.1145/3230627.
  * Kreber & Hahn [2021] Jens U. Kreber and Christopher Hahn.  Generating symbolic reasoning problems with transformer GANs.  _CoRR_ , abs/2110.10054, 2021.  URL https://arxiv.org/abs/2110.10054.
  * Lample et al. [2018] Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato.  Unsupervised machine translation using monolingual corpora only.  In _6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, April 30 - May 3, 2018, Conference Track Proceedings_. OpenReview.net, 2018.  URL https://openreview.net/forum?id=rkYTTf-AZ.
  * Lederman et al. [2020] Gil Lederman, Markus N. Rabe, Sanjit Seshia, and Edward A. Lee.  Learning heuristics for quantified boolean formulas through reinforcement learning.  In _8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020_. OpenReview.net, 2020.  URL https://openreview.net/forum?id=BJluxREKDB.
  * Li et al. [2022] Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d’Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, Alexey Cherepanov, James Molloy, Daniel J. Mankowitz, Esme Sutherland Robson, Pushmeet Kohli, Nando de Freitas, Koray Kavukcuoglu, and Oriol Vinyals.  Competition-level code generation with alphacode.  _DeepMind_ , 2022.
  * Loos et al. [2017] Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk.  Deep network guided proof search.  In Thomas Eiter and David Sands (eds.), _LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017_ , volume 46 of _EPiC Series in Computing_ , pp. 85–105. EasyChair, 2017.  doi: 10.29007/8mwc.  URL https://doi.org/10.29007/8mwc.
  * Loshchilov & Hutter [2017] Ilya Loshchilov and Frank Hutter.  SGDR: stochastic gradient descent with warm restarts.  In _5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings_. OpenReview.net, 2017.  URL https://openreview.net/forum?id=Skq89Scxx.
  * Loshchilov & Hutter [2019] Ilya Loshchilov and Frank Hutter.  Decoupled weight decay regularization.  In _7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019_. OpenReview.net, 2019.  URL https://openreview.net/forum?id=Bkg6RiCqY7.
  * Paulson & Blanchette [2015] Lawrence Paulson and Jasmin Blanchette.  Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers.  02 2015.  doi: 10.29007/tnfd.
  * Polu & Sutskever [2020] Stanislas Polu and Ilya Sutskever.  Generative language modeling for automated theorem proving.  _CoRR_ , abs/2009.03393, 2020.  URL https://arxiv.org/abs/2009.03393.
  * Polu et al. [2022] Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever.  Formal mathematics statement curriculum learning, 2022.  URL https://arxiv.org/abs/2202.01344.
  * Rabe et al. [2021] Markus N. Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy.  Mathematical reasoning via self-supervised skip-tree training.  In _ICLR_ , 2021.
  * Radford et al. [2019] Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al.  Language models are unsupervised multitask learners.  _OpenAI blog_ , 1(8):9, 2019.
  * Schmitt et al. [2021] Frederik Schmitt, Christopher Hahn, Markus N. Rabe, and Bernd Finkbeiner.  Neural circuit synthesis from specification patterns.  In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (eds.), _Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual_ , pp. 15408–15420, 2021.  URL https://proceedings.neurips.cc/paper/2021/hash/8230bea7d54bcdf99cdfe85cb07313d5-Abstract.html.
  * Schulz [2001] Stephan Schulz.  Learning search control knowledge for equational theorem proving.  In Franz Baader, Gerhard Brewka, and Thomas Eiter (eds.), _KI 2001: Advances in Artificial Intelligence, Joint German/Austrian Conference on AI, Vienna, Austria, September 19-21, 2001, Proceedings_ , volume 2174 of _Lecture Notes in Computer Science_ , pp. 320–334. Springer, 2001.  doi: 10.1007/3-540-45422-5\\_23.
  * Sennrich et al. [2016] Rico Sennrich, Barry Haddow, and Alexandra Birch.  Improving neural machine translation models with monolingual data.  In _Proceedings of the 54th Annual Meeting of the Association for Computational Linguistics, ACL 2016, August 7-12, 2016, Berlin, Germany, Volume 1: Long Papers_. The Association for Computer Linguistics, 2016\.  doi: 10.18653/v1/p16-1009.  URL https://doi.org/10.18653/v1/p16-1009.
  * Szegedy [2020] Christian Szegedy.  A promising path towards autoformalization and general artificial intelligence.  In Christoph Benzmüller and Bruce R. Miller (eds.), _Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings_ , volume 12236 of _Lecture Notes in Computer Science_ , pp. 3–20. Springer, 2020.  doi: 10.1007/978-3-030-53518-6\\_1.  URL https://doi.org/10.1007/978-3-030-53518-6_1.
  * Urban [2004] Josef Urban.  MPTP - motivation, implementation, first experiments.  _J. Autom. Reason._ , 33(3-4):319–339, 2004.  doi: 10.1007/s10817-004-6245-1.
  * Vaswani et al. [2017] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin.  Attention is all you need.  In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), _Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA_ , pp. 5998–6008, 2017.  URL https://proceedings.neurips.cc/paper/2017/hash/3f5ee243547dee91fbd053c1c4a845aa-Abstract.html.
  * Wang [2021] Ben Wang.  Mesh-Transformer-JAX: Model-Parallel Implementation of Transformer Language Model with JAX.  https://github.com/kingoflolz/mesh-transformer-jax, May 2021.
  * Wang et al. [2018] Qingxiang Wang, Cezary Kaliszyk, and Josef Urban.  First experiments with neural translation of informal to formal mathematics.  In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), _Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings_ , volume 11006 of _Lecture Notes in Computer Science_ , pp. 255–270. Springer, 2018.  doi: 10.1007/978-3-319-96812-4\\_22.  URL https://doi.org/10.1007/978-3-319-96812-4_22.
  * Wang et al. [2020] Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban.  Exploration of neural machine translation in autoformalization of mathematics in mizar.  In _International Conference on Certified Programs and Proofs_ , 2020\.
  * Wenzel et al. [2008] Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow.  The Isabelle framework.  In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (eds.), _Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008\. Proceedings_ , volume 5170 of _Lecture Notes in Computer Science_ , pp. 33–38. Springer, 2008.  doi: 10.1007/978-3-540-71067-7\\_7.
  * Wu et al. [2021a] Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli.  Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning.  In Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (eds.), _Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual_ , pp. 9330–9342, 2021a.  URL https://proceedings.neurips.cc/paper/2021/hash/4dea382d82666332fb564f2e711cbc71-Abstract.html.
  * Wu et al. [2021b] Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse.  INT: an inequality benchmark for evaluating generalization in theorem proving.  In _9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021_. OpenReview.net, 2021b.  URL https://openreview.net/forum?id=O6LPudowNQm.
  * Wu et al. [2022] Yuhuai Wu, Markus N Rabe, DeLesley Hutchins, and Christian Szegedy.  Memorizing transformers.  In _10th International Conference on Learning Representations, ICLR 2022_. OpenReview.net, 2022.
  * Zheng et al. [2021] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu.  MiniF2F: a cross-system benchmark for formal olympiad-level mathematics.  _arXiv preprint arXiv:2109.00110_ , 2021.

Appendix

##  Appendix A Few-shot Prompts

###  A.1 Prompt used to formalize algebra problems

Natural language version: _"Simplify
$\left(\frac{4}{x}\right)^{-1}\left(\frac{3x^{3}}{x}\right)^{2}\left(\frac{1}{2x}\right)^{-3}$.
The final answer is $18x^{8}$"_. Translate the natural language version to an
Isabelle version: ⬇ theorem fixes x :: real assumes h0 : "x \<noteq> 0" shows
"1/(4/x) * ((3*x^3)/x)^2 * (1/(1 / (2 * x)))^3 = 18 * x^8" Natural language
version: _"For integers $n$, let_
$f(n)=\left\\{\begin{array}[]{cl}n^{2}&\text{ if }n\text{ is odd},\\\
n^{2}-4n-1&\text{ if }n\text{ is even}.\end{array}\right.$ _Find
$f(f(f(f(f(4)))))$. The final answer is 1"._ Translate the natural language
version to an Isabelle version: ⬇ theorem fixes f :: "int \<Rightarrow> int"
assumes "\<forall>n. odd n \<longrightarrow> f n = n^2" and "\<forall> n. even
n \<longrightarrow> f n = n^2 - 4*n -1" shows "f 4 = -1" Natural language
version: _"The volume of a cone is given by the formula $V=\frac{1}{3}Bh$,
where $B$ is the area of the base and $h$ is the height. The area of the base
of a cone is 30 square units, and its height is 6.5 units. What is the number
of cubic units in its volume? The final answer is 65"._ Translate the natural
language version to an Isabelle version: ⬇ theorem fixes b h v ::real assumes
"0 < b \<and> 0 < h \<and> 0 < v" and "v = 1 / 3 * (b * h)" and "b = 30" and
"h = 13 / 2" shows "v = 65" Natural language version: _"If
$3a+b+c=-3,a+3b+c=9,a+b+3c=19$, then find $abc$. The final answer is -56"._
Translate the natural language version to an Isabelle version: ⬇ theorem fixes
a b c :: real assumes "3 * a + b + c = -3" and "a + 3 * b + c = 9" and "a + b
+ 3 * c = 19" shows "a * b * c = -56"

Natural language version: _"If $f(x)=5x-12$, find a value for $x$ so that
$f^{-1}(x)=f(x+1)$. The final answer is $\frac{47}{24}$"._ Translate the
natural language version to an Isabelle version: ⬇ theorem fixes x :: real and
\<sigma>::"real \<Rightarrow> real" assumes "bij \<sigma>" and
\<sigma>:"\<forall> x. \<sigma> x = 5 * x - 12" and "\<sigma> (x + 1) = (inv
\<sigma>) x" shows "x = 47 / 24" Natural language version: _"What is the
$x$-coordinate for the $x$-intercept of the line containing the points $(7,4)$
and $(6,3)$? The final answer is 3"._ Translate the natural language version
to an Isabelle version: ⬇ theorem fixes a b :: real and f :: "real
\<Rightarrow> real" assumes h0 : "\<And>x. f x = a * x + b" and h1 : "f 7 = 4"
and h2 : "f 6 = 3" shows "f 3 = 0" Natural language version: _"Given
$2^{a}=32$ and $a^{b}=125$ find $b^{a}$. The final answer is 243"._ Translate
the natural language version to an Isabelle version: ⬇ theorem fixes a b ::
real assumes "2 powr a = 32" and "a powr b = 125" shows "b powr a = 243"
Natural language version: _"Let_ $f(x)=\begin{cases}x^{2}+9&\text{if }x<-5,\\\
3x-8&\text{if }x\geq-5.\end{cases}$ _If $f(x)=10$, find the sum of all
possible values of $x$. The final answer is 6"._ Translate the natural
language version to an Isabelle version: ⬇ theorem fixes f :: "real
\<Rightarrow> real" assumes "\<forall> x < -5. f x = x^2 + 5" and "\<forall> x
\<ge> -5. f x = 3 * x -8" shows "(\<Sum> k \<in> (f -‘ {10}). k) = 6" Natural
language version: _"Simplify $(9-4i)-(-3-4i)$. The final answer is 12"._
Translate the natural language version to an Isabelle version: ⬇ theorem fixes
q e :: complex assumes h0 : "q = Complex (Re 9) (Im (-4))" and h1 : "e =
Complex (Re (-3)) (Im (-4))" shows "q - e = 12" Natural language version:
_"What is the minimum possible value for $y$ in the equation $y=x^{2}-6x+13$?
The final answer is 4"._ Translate the natural language version to an Isabelle
version: ⬇ theorem fixes x y :: real assumes h0 : "y = x^2 - 6 * x + 13" shows
"4 \<le> y"

###  A.2 Prompt used to formalize number theory problems

Natural language version: _"If $n$ is a positive integer such that $2n$ has 28
positive divisors and $3n$ has 30 positive divisors, then how many positive
divisors does $6n$ have? The final answer is 35"._ Translate the natural
language version to an Isabelle version: ⬇ theorem fixes n :: nat assumes
"n>0" and "card ({k. k dvd (2*n)}) = 28" and "card ({k. k dvd (3*n)}) = 30"
shows "card ({k. k dvd (6*n)}) = 35" Natural language version: _"Let $n$ be
the number of integers $m$ in the range $1\leq m\leq 8$ such that
$\text{gcd}(m,8)=1$. What is the remainder when $3^{n}$ is divided by $8$? The
final answer is 1"._ Translate the natural language version to an Isabelle
version: ⬇ theorem fixes n :: nat assumes "n = card {k::nat. gcd k 8 = 1
\<and> 1\<le>k \<and> k < 8}" shows "(3^n) mod 8 = (1::nat)" Natural language
version: _"What is the remainder when $1+2+3+4+\dots+9+10$ is divided by 9?
The final answer is 1"._ Translate the natural language version to an Isabelle
version: ⬇ theorem "(\<Sum> k< 11. k) mod 9 = (1::nat)" Natural language
version: _"Cards are numbered from 1 to 100. One card is removed and the
values on the other 99 are added. The resulting sum is a multiple of 77. What
number was on the card that was removed? The final answer is 45"._ Translate
the natural language version to an Isabelle version: ⬇ theorem fixes x :: nat
assumes h0 : "1 \<le> x \<and> x \<le> 100" and h1 : "77 dvd
((\<Sum>k::nat=0..100. k)-x)" shows "x=45" Natural language version: _"Find
$9^{-1}\pmod{100}$, as a residue modulo 100. (Give an answer between 0 and 99,
inclusive.) The final answer is $89\pmod{100}$"._ Translate the natural
language version to an Isabelle version: ⬇ theorem fixes x::nat assumes "x <
100" and "x*9 mod 100 = 1" shows "x = 89"

Natural language version: "Suppose $m$ is a two-digit positive integer such
that $6^{-1}\pmod{m}$ exists and $6^{-1}\equiv 6^{2}\pmod{m}$. What is $m$?
The final answer is 43". Translate the natural language version to an Isabelle
version: ⬇ theorem fixes m x :: nat assumes h0 : "10 \<le> m" and h1 : "m
\<le> 99" and h2 : "(6 * x) mod m = 1" and h3 : "(x - 6^2) mod m = 0" shows "m
= 43" Natural language version: "Find $24^{-1}\pmod{11^{2}}$. That is, find
the residue $b$ for which $24b\equiv 1\pmod{11^{2}}$. Express your answer as
an integer from $0$ to $11^{2}-1$, inclusive. The final answer is 116".
Translate the natural language version to an Isabelle version: ⬇ theorem fixes
b::int assumes "\<forall>b::int. 0\<le>b \<and> b\<le>11^2 \<and> [b * 24 = 1]
(mod (11^2))" shows "b = 116" Natural language version: _"Given that $p\geq 7$
is a prime number, evaluate_ $1^{-1}\cdot 2^{-1}+2^{-1}\cdot
3^{-1}+3^{-1}\cdot 4^{-1}+\cdots+(p-2)^{-1}\cdot(p-1)^{-1}\pmod{p}.$ _The
final answer is $2\pmod{p}$"._ Translate the natural language version to an
Isabelle version: ⬇ theorem fixes p :: nat assumes "prime p" and "7 \<le> p"
shows "(\<Sum> k \<in> {1..<p-1}. (inv_mod k p)* (inv_mod (k+1) p)) = 2"
Natural language version: _"What is the remainder when
$2000+2001+2002+2003+2004+2005+2006$ is divided by $7$? The final answer is
0"._ Translate the natural language version to an Isabelle version: ⬇ theorem
"(2000 + 2001 + 2002 + 2003 + 2004 + 2005 + 2006) mod 7 = (0::nat)" Natural
language version: _"One morning each member of Angela’s family drank an
8-ounce mixture of coffee with milk. The amounts of coffee and milk varied
from cup to cup, but were never zero. Angela drank a quarter of the total
amount of milk and a sixth of the total amount of coffee. How many people are
in the family? The final answer is 5"._ Translate the natural language version
to an Isabelle version: ⬇ theorem fixes x y n ::nat assumes "x / 4 + y / 6 =
(x + y) / n" and "n\<noteq>0" "x\<noteq>0" "y\<noteq>0" shows "n = 5"

###  A.3 Prompt used for informalization

Isabelle version: ⬇ theorem fixes z::complex assumes h0: "z = (Complex (1/sqrt
2) (1/sqrt 2))" shows "(\<Sum>k::nat=1..12. (z^(k^2))) * (\<Sum> k::nat=1..12.
1/(z^(k^2))) =36" Translate the Isabelle version to a natural language
version: _"Let $z=\frac{1+i}{\sqrt{2}}$, find
$(\sum_{i=1}^{1}2(z^{i^{2}}))\cdot(\sum_{i=1}^{1}2(\frac{1}{z^{i^{2}}}))$. The
final answer is 36."_ Isabelle version: ⬇ theorem fixes a b ::real assumes
"(ln a) / (ln 8) + (ln (b^2)) / (ln 4) = 5" "(ln b) / (ln 8) + (ln (a^2)) /
(ln 4) = 7" shows "a * b = 512" Translate the Isabelle version to a natural
language version: "Determine the value of $ab$ if $\log_{8}a+\log_{4}b^{2}=5$
and $\log_{8}b+\log_{4}a^{2}=7$. The final answer is 512".

##  Appendix B More on case Studies

###  B.1 Case Study 1

Here we show the output given by PaLM model 540B. The model got the most
structure correctly, but made some syntactical errors.

Question: Natural language version: "Prove that there is no function $f$ from
the set of non-negative integers into itself such that $f(f(n))=n+1987$ for
every $n$." Translate the natural language version to an Isabelle version:
PaLM 540B Output: ⬇ theorem fixes f :: "nat -> nat" assumes "forall n::nat.
f(f(n)) = n + 1987" shows "false"

###  B.2 Case Study 2

We show below the output given by PaLM models of different sizes.

Question: Natural Language version: "_When all the girls at Madeline’s school
line up in rows of eight, there are seven left over. If instead they line up
in rows of four, how many are left over? The final answer is 3._ " Translate
the natural language version to an Isabelle version: PaLM 540B output: ⬇
theorem fixes n::nat assumes "n mod 8 = 7" shows "n mod 4 = 3"

Question: Natural Language version: "_When all the girls at Madeline’s school
line up in rows of eight, there are seven left over. If instead they line up
in rows of four, how many are left over? The final answer is 3._ " Translate
the natural language version to an Isabelle version: PaLM 64B output: ⬇
theorem fixes girls :: nat assumes "(girls / 8) + 7 = girls" shows "girls = 3"

Question: Natural Language version: "_When all the girls at Madeline’s school
line up in rows of eight, there are seven left over. If instead they line up
in rows of four, how many are left over? The final answer is 3._ " Translate
the natural language version to an Isabelle version: PaLM 8B output: ⬇ theorem
fixes a b ::real assumes "(ln a) / (ln 8) + (ln (b^2)) / (ln 4) = 7" "(ln b) /
(ln 8) + (ln (a^2)) / (ln 4) = 3"}} shows "a * b = 3"

###  B.3 Case Study 3

If we include the following example in the prompt in additional to the two
examples shown in Figure 2:

Natural language version: "What is the $x$-coordinate for the $x$-intercept of
the line containing the points $(7,4)$ and $(6,3)$? The final answer is 3".
Translate the natural language version to an Isabelle version: ⬇ theorem fixes
a b :: real and f :: "real \<Rightarrow> real" assumes h0 : "\<And>x. f x = a
* x + b" and h1 : "f 7 = 4" and h2 : "f 6 = 3" shows "f 3 = 0"

Then Codex was able to formalize the problem perfectly:

Question: Natural language version: "Let $f$ be a linear function for which
$f(6)-f(2)=12.$ What is $f(12)-f(2)?$ The final answer is 30." Translate the
natural language version to an Isabelle version: Codex Output: ⬇ theorem fixes
a b :: real and f :: "real \<Rightarrow> real" assumes h0 : "\<And>x. f x = a
* x + b" and h1 : "f 6 - f 2 = 12" shows "f 12 - f 2 = 30"

Note that this additional example in the prompt is only tangentially related.
The phrase “linear function” is not even mentioned. Instead, it shows an
example how to formalize a _line_. But that is sufficient for the model to
understand how to formalize a “linear function”.

##  Appendix C More Examples on Mathematical Competition Problems

###  C.1 Perfect Translations

Question: Natural language version: _"At what point does the line containing
the points $(1,7)$ and $(3,11)$ intersect the $y$-axis? Express your answer as
an ordered pair. The final answer is (0,5)"._ Translate the natural language
version to an Isabelle version: Codex Output: ⬇ theorem fixes a b :: real and
f :: "real \<Rightarrow> real" assumes h0 : "\<And>x. f x = a * x + b" and h1
: "f 1 = 7" and h2 : "f 3 = 11" shows "f 0 = 5"

Question: Natural language version: _"A map of the town that Annie, Barbara,
and Charlie live in can be represented by the Cartesian plane. Annie is
located at $(6,-20)$ and Barbara is located at $(1,14)$. They agree to meet at
the closest point that is equidistant from their current locations and walk
upwards together to get to Charlie’s location at $\left(\frac{7}{2},2\right)$.
How many units upward do Annie and Barbara walk together to get to Charlie?
The final answer is 5."_ Translate the natural language version to an Isabelle
version: Codex Output: ⬇ theorem fixes a b c :: "real \<times> real" assumes
h0 : "a = (6, -20)" and h1 : "b = (1, 14)" and h2 : "c = (7 / 2, 2)" shows
"dist a c + dist b c = 5"

Question: Natural language version: "Let $x$ be a positive integer, and define
the integers $n=x^{2}+2x+17$ and $d=2x+5$. When dividing $n$ by $d$, the
quotient is $x$, and the remainder is $7$. Find $x$. The final answer is 2".
Codex Output: ⬇ theorem fixes x n d :: int assumes h0 : "x > 0" and h1 : "n =
x^2 + 2 * x + 17" and h2 : "d = 2 * x + 5" and h3 : "n div d = x" and h4 : "n
mod d = 7" shows "x = 2"

Question: Natural language version: "A line segment begins at $(1,3)$. It is 5
units long and ends at the point $(4,x)$ and $x>0$. What is the value of $x$?
The final answer is 7". Codex Output: ⬇ theorem fixes x :: real assumes h0 :
"x > 0" and h1 : "5 = sqrt ((4 - 1)^2 + (x - 3)^2)" shows "x = 7"

Natural language version: "A line segment begins at $(1,3)$. It is 5 units
long and ends at the point $(4,x)$ and $x>0$. What is the value of $x$? The
final answer is 7". Codex Output: ⬇ theorem fixes x :: real assumes h0 : "x >
0" and h1 : "5 = sqrt ((4 - 1)^2 + (x - 3)^2)" shows "x = 7"

Question: Natural language version: "Let $f(x)=x^{2}-2x$. How many distinct
real numbers $c$ satisfy $f(f(f(f(c))))=3$? The final answer is 9". Codex
Output: ⬇ theorem fixes f :: "real \<Rightarrow> real" assumes h0 : "\<forall>
x. f x = x^2 - 2 * x" shows "card {c. f (f (f (f c))) = 3} = 9"

Question: Natural language version: "Find the solutions to $z^{4}=-4.$ Enter
the solutions, separated by commas. The final answer is 1 + i, 1 - i, -1 + i,
-1 - i". Codex Output: ⬇ theorem fixes z :: complex assumes "z^4 = -4" shows
"z = 1 + \<i> \<or> z = 1 - \<i> \<or> z = -1 + \<i> \<or> z = -1 - \<i>"

Question: Natural language version: "Let $z$ be a complex number satisfying
$z^{2}=4z-19+8i$. Given that $|z|$ is an integer, find $z.$ The final answer
is 3 + 4i". Codex Output: ⬇ theorem fixes z :: complex assumes h0 : "z^2 = 4 *
z - 19 + 8 * \<i>" and h1 : "norm z \<in> \<int>" shows "z = 3 + 4 * \<i>"

Question: Natural language version: "The sequence $(a_{n})$ satisfies
$a_{1}+a_{2}+a_{3}+\dots+a_{n}=n^{2}a_{n}$ for all $n\geq 2.$ If $a_{63}=1,$
find $a_{1}.$ The final answer is 2016". Codex Output: ⬇ theorem fixes a ::
"nat \<Rightarrow> real" assumes h0 : "\<forall> n \<ge> 2. (\<Sum> k = 1..n.
a k) = n^2 * a n" and h1 : "a 63 = 1" shows "a 1 = 2016"

Question: Natural language version: "Find the units digit of the following
within the indicated number base: $52_{7}+62_{7}$ The final answer is 4".
Codex Output: ⬇ theorem fixes x y :: nat assumes "x < 7" and "y < 7" shows
"((x*7+2) + (y*7+2)) mod 7 = 4"

Question: Natural language version: "How many factors of 8000 are perfect
squares? The final answer is 8". Codex Output: ⬇ theorem fixes n :: nat
assumes "n = card {k::nat. k^2 dvd 8000}" shows "n = 8"

Question: Natural language version: "Solve the congruence $11n\equiv
7\pmod{43}$, as a residue modulo 43. (Give an answer between 0 and 42.) The
final answer is 28". Codex Output: ⬇ theorem fixes n :: nat assumes "n < 43"
and "(11 * n) mod 43 = 7" shows "n = 28"

Question: Natural language version: "What is the 100th digit after the decimal
point of the decimal representation of 1/7? The final answer is 8". Codex
Output: ⬇ theorem fixes x :: nat assumes "x = (1/7) * 10^100" shows "x mod 10
= 8"

Question: Natural language version: "Two positive integers $m$ and $n$ are
chosen such that $m$ is the smallest positive integer with only two positive
divisors and $n$ is the largest integer less than $100$ with exactly three
positive divisors. What is $m+n$? The final answer is 51". Codex Output: ⬇
theorem fixes m n :: nat assumes "m = (LEAST k. card {d. d dvd k \<and> d > 0}
= 2)" and "n = (GREATEST k. card {d. d dvd k \<and> d > 0} = 3 \<and> k <
100)" shows "m + n = 51"

###  C.2 Incorrect Translations

In this section, we present failure cases for each of the categories in Table
2 in Section. 4.4.

Error category: incomplete/ill-formed/unclear prompt Question: Natural
language version: "Find the largest value of $t$ such that
$\frac{13t^{2}-34t+12}{3t-2}+5t=6t-1.$ The final answer is \frac{5". Codex
Output: ⬇ theorem fixes t :: real assumes h0 : "13 * t^2 - 34 * t + 12 = 3 * t
- 2" and h1 : "5 * t = 6 * t - 1" shows "t = 5 / 2"

Error category: fail to align definitions or concepts Question: Natural
language version: "What is the smallest four-digit positive integer that is
divisible by 47? The final answer is 1034". Codex Output: ⬇ theorem fixes x ::
nat assumes "x > 999" and "x < 10000" and "47 dvd x" shows "x = 1034"

Here, the translator correctly captured the meaning of "four-digit positive
integer" (i.e., "x > 999" and "x < 10000") and that of "divisible by 47"
(i.e., "47 dvd x"). However, it fails to align the "smallest" concept to the
one in Isabelle.

Error category: inconsistent/missing assumption Question: Natural language
version: "Jack walked up a hill at a speed of $(x^{2}-11x-22)$ miles per hour.
Meanwhile, Jill walked a total distance of $(x^{2}-3x-54)$ miles in $(x+6)$
hours. If Jack and Jill walked at the same speed, what is that speed, in miles
per hour? The final answer is 4". Codex Output: ⬇ theorem fixes x :: real
assumes h0 : "x^2 - 11 * x - 22 = x^2 - 3 * x - 54" shows "x = 4"

Here, the translator missed the "($x+6$)" part in the natural language—it
should be translated to "x^2 - 11 * x - 22 = (x^2 - 3 * x - 54)/(x+6)"
instead. Also, the conclusion is incorrect either: it should be "x^2 - 11 * x
- 22 = 4" or "(x^2 - 3 * x - 54)/(x+6) = 4".

Error category: syntactical/type error) Question: Natural language version:
"Find $\sum_{N=1}^{1024}\lfloor\log_{2}N\rfloor.$ The final answer is 8204".
Codex Output: ⬇ theorem fixes N :: nat shows "(\<Sum> N = 1..1024. nat
\<lfloor>log 2 N\<rfloor>) = 8204"

In the current version, N will be inferred as a real number, so that the
interval "1..1024" will be a real interval from 1 to 1024. This is incorrect,
and sum over such infinite interval will result in 0 (i.e., "(\<Sum> N =
1..1024. nat \<lfloor>log 2 N\<rfloor>) = 0"). The correct version requires an
explicit type conversion: "(\<Sum> N = 1..1024. \<lfloor>log 2 (of_int
N)\<rfloor>) = 8204".

Error category: missing definition in Isabelle Question: Natural language
version: "The product of two positive three-digit palindromes is 436,995. What
is their sum? The final answer is 1332". Codex Output: ⬇ theorem fixes x y ::
nat assumes "100 \<le> x \<and> x \<le> 999" and "100 \<le> y \<and> y \<le>
999" and "x * y = 436995" shows "x + y = 1332"

The only missing part in this example is the definition of palindromes. It
appears that the translator does not know what a palindrome is so that it
chooses to drop it from the assumptions.

Error category: wrong application of functions Question: Natural language
version: "If the operation $Z$ is defined as $aZb=b+10a-a^{2}$, what is the
value of $2Z6$? The final answer is 22". Codex Output: ⬇ theorem fixes a b ::
real assumes h0 : "a Z b = b + 10 * a - a^2" shows "2 Z 6 = 22"

The function Z should be applied in a prefix way in Isabelle. Also, the
translator missed the "for all" quantifier in the assumption. The correct
assumption should be "\<forall> a b. Z a b = b + 10 * a - a^2".

Error category: other Question: Natural language version: "Simplify:
$|{-3^{2}+4}|$ The final answer is 5". Codex Output: ⬇ theorem fixes x :: real
assumes h0 : "x = - 3 ^2 + 4" shows "abs x = 5"

Here, a parenthesis should be placed around 3 ^2 (i.e., "x = - (3 ^2) + 4").
This is a subtle issue to operator precedence in Isabelle.

Error category: other Question: Natural language version: "How many numbers
from $1$ to $150$ are not perfect squares or perfect cubes? The final answer
is 135". Codex Output: ⬇ theorem fixes n :: nat assumes "n \<le> 150" shows
"card {k::nat. k \<le> n \<and> \<not> (\<exists> m. m^2 = k \<or> m^3 = k) }
= 135"

The translator somehow introduces an unnecessary variable n and assumed "n
\<le> 150". The correct translation should have n replaced with 150 in the
conclusion: "card {k::nat. k \<le> 150 \<and> \<not> (\<exists> m. m^2 = k
\<or> m^3 = k) } = 135".

##  Appendix D More Examples on Advanced Mathematics

###  D.1 Formalization

Question: Natural language version: "Let $f$ be a continuous function from a
compact convex set $S$ to itself. Then there exists $x\in S$ such that
$f(x)=x$." Translate the natural language version to an Isabelle version:
Codex Output: ⬇ theorem fixes f :: "’a::real_normed_vector \<Rightarrow> ’a"
assumes "continuous_on S f" "compact S" "convex S" shows "\<exists>x\<in>S. f
x = x"

Here, we asked the model to formalize the statement of the famous Brouwer’s
fixed-point theorem. The model made two mistakes. The first one is that the
model erroneously assume the function is on a real normed vector space rather
than a euclidean space or a banach space. This is quite understandable as we
left this information in the source. The second and more critical error is
that the absence of the assumption of $f$ mapping from $S$ to itself (i.e.,
$f(S)\subseteq S$ or $f(S)=S$).

Question: Let $\gamma$ be a closed path in the complex plane, and $z$ be a
point not on $\gamma$. Then the winding number of $\gamma$ around $z$ is an
integer. Codex Output: ⬇ theorem fixes \<gamma> :: "real \<Rightarrow>
complex" and z :: complex assumes "continuous_on {0..1} \<gamma>" "\<gamma> 0
= \<gamma> 1" "z \<notin> \<gamma> ‘ {0..1}" shows "winding_number \<gamma> z
\<in> \<int>"

Here, the model has made a perfect translation–not only the model correctly
infers that a path in the complex plane should be a function from the real
interval $[0,1]$ to complex, it also manages to align a path being closed to
the assumption `\<gamma> 0 = \<gamma> 1`.

###  D.2 Informalization

The following lemma statements are from the standard library of Isabellle
(i.e., HOL-Complex_Analysis and HOL-Probability).

_proposition_ openin_clauses:  _fixes_ U :: "’a topology"  _shows_ "openin U
{}" "_$\bigwedge$_ S T. openin U S  _$\Longrightarrow$_ openin U T
_$\Longrightarrow$_ openin U (S _$\cap$_ T)" "_$\bigwedge$_ K. (_$\forall\,$_
S  _$\in$_ K. openin U S)  _$\Longrightarrow$_ openin U (_$\bigcup\,$_ K)"
Translate the Isabelle version to a natural language version: Codex Output: ⬇
Let $U$ be a topology, then $U$ is open if and only if it satisfies the
following conditions: 1. $U$ is open. 2. If $S$ and $T$ are open, then $S \cap
T$ is open. 3. If $K$ is a collection of open sets, then $\cup K$ is open.

_lemma_ openin_Int[intro]:  "openin U S  _$\Longrightarrow$_ openin U T
_$\Longrightarrow$_ openin U (S  _$\cap$_ T)" Translate the Isabelle version
to a natural language version: Codex Output: "Let $U$ be a topology, then
$\emptyset$ is open in $U$, if $S$ and $T$ are open in $U$, then $S\cap T$ is
open in $U$, if $K$ is a collection of sets, and each set in $K$ is open in
$U$, then $\bigcup K$ is open in $U$".

_lemma_ openin_Int[intro]:  "openin U S  _$\Longrightarrow$_ openin U T
_$\Longrightarrow$_ openin U (S  _$\cap$_ T)" Translate the Isabelle version
to a natural language version: Codex Output: "If $S$ and $T$ are open in $U$,
then $S\cap T$ is open in $U$".

_lemma_ openin_Inter [intro]:  _assumes_ "finite  _$\mathcal{F}$_ "
"_$\mathcal{F}$_  _$\not=$_ {}" "_$\bigwedge$_ X. X  _$\in$_  _$\mathcal{F}$_
_$\Longrightarrow$_ openin T X"   _shows_ "openin T
(_$\bigcap\,$__$\mathcal{F}$_)" Translate the Isabelle version to a natural
language version: Codex Output: "If $T$ is a topological space, and
$\mathcal{F}$ is a finite non-empty collection of open subsets of $T$, then
$\bigcap\mathcal{F}$ is open in $T$".

_lemma_ openin_subtopology:  "openin (subtopology U V) S
_$\longleftrightarrow$_ (_$\exists\,$_ T. openin U T  _$\wedge$_ S = T
_$\cap$_ V)" Translate the Isabelle version to a natural language version:
Codex Output: "$S$ is open in the subtopology of $U$ induced by $V$ if and
only if there exists an open set $T$ in $U$ such that $S=T\cap V$".

_lemma_ closedin_subtopology_Un: "_$\mathopen{[\mkern-3.0mu[}$_ closedin
(subtopology X T) S; closedin (subtopology X U) S
_$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ closedin (subtopology X (T
_$\cup$_ U)) S" Translate the Isabelle version to a natural language version:
Codex Output: "If $S$ is closed in $T$ and $S$ is closed in $U$, then $S$ is
closed in $T\cup U$".

_lemma_ connected_closedin: "connected S  _$\longleftrightarrow$_
(_$\nexists\,$_ E1 E2. closedin (top_of_set S) E1  _$\wedge$_ closedin
(top_of_set S) E2  _$\wedge$_ S  _$\subseteq$_ E1  _$\cup$_ E2  _$\wedge$_ E1
_$\cap$_ E2 = {}  _$\wedge$_ E1  _$\not=$_ {}  _$\wedge$_ E2  _$\not=$_ {})"
Translate the Isabelle version to a natural language version: Codex Output: "A
set $S$ is connected if and only if there does not exist two closed sets
$E_{1}$ and $E_{2}$ such that $S\subseteq E_{1}\cup E_{2}$, $E_{1}\cap
E_{2}=\emptyset$, $E_{1}\neq\emptyset$ and $E_{2}\neq\emptyset$".

_definition_ continuous_map  _where_ "continuous_map X Y f  _$\equiv$_
(_$\forall\,$_ x  _$\in$_ topspace X. f x  _$\in$_ topspace Y)  _$\wedge$_
(_$\forall\,$_ U. openin Y U  _$\longrightarrow$_ openin X {x  _$\in$_
topspace X. f x  _$\in$_ U})" Translate the Isabelle version to a natural
language version: Codex Output: "A function $f$ from a topological space $X$
to a topological space $Y$ is continuous if for every open set $U$ in $Y$, the
preimage $f^{-1}(U)$ is open in $X$".

_definition_ continuous_map  _where_ "continuous_map X Y f  _$\equiv$_
(_$\forall\,$_ x  _$\in$_ topspace X. f x  _$\in$_ topspace Y)  _$\wedge$_
(_$\forall\,$_ U. openin Y U  _$\longrightarrow$_ openin X {x  _$\in$_
topspace X. f x  _$\in$_ U})" Translate the Isabelle version to a natural
language version: Codex Output: "A continuous map $f:X\rightarrow Y$ is a map
such that for every open set $U\subset Y$, the preimage $f^{-1}(U)$ is open in
$X$".

_lemma_ connectedin_separation: "connectedin X S  _$\longleftrightarrow$_ S
_$\subseteq$_ topspace X  _$\wedge$_ (_$\nexists\,$_ C1 C2. C1  _$\cup$_ C2 =
S  _$\wedge$_ C1  _$\not=$_ {}  _$\wedge$_ C2  _$\not=$_ {}   _$\wedge$_ C1
_$\cap$_ X closure_of C2 = {}  _$\wedge$_ C2   _$\cap$_ X closure_of C1 = {})"
(_is_ "?lhs = ?rhs") Translate the Isabelle version to a natural language
version: Codex Output: "$S$ is connected in $X$ if and only if $S\subseteq X$
and there do not exist two non-empty sets $C_{1}$ and $C_{2}$ such that
$C_{1}\cup C_{2}=S$ and $C_{1}\cap X\overline{C_{2}}=\emptyset$ and $C_{2}\cap
X\overline{C_{1}}=\emptyset$".

_lemma_ connectedin_Union:  _assumes_  _$\mathcal{U}$_ : "_$\bigwedge$_ S. S
_$\in$_  _$\mathcal{U}$_  _$\Longrightarrow$_ connectedin X S"  _and_ ne:
"_$\bigcap\,$__$\mathcal{U}$_  _$\not=$_ {}"  _shows_ "connectedin X
(_$\bigcup\,$__$\mathcal{U}$_)" Translate the Isabelle version to a natural
language version: Codex Output: "If $S$ is connected in $X$ for all
$S\in\mathcal{U}$ and $\bigcap_{S\in\mathcal{U}}S\neq\emptyset$, then
$\bigcup_{S\in\mathcal{U}}S$ is connected in $X$".

_lemma_ compact_space_alt: "compact_space X  _$\longleftrightarrow$_
(_$\forall\,$__$\mathcal{U}$_. (_$\forall\,$_ U  _$\in$_  _$\mathcal{U}$_.
openin X U)  _$\wedge$_ topspace X  _$\subseteq$_
_$\bigcup\,$__$\mathcal{U}$_  _$\longrightarrow$_
(_$\exists\,$__$\mathcal{F}$_. finite  _$\mathcal{F}$_  _$\wedge$_
_$\mathcal{F}$_  _$\subseteq$_  _$\mathcal{U}$_  _$\wedge$_ topspace X
_$\subseteq$_  _$\bigcup\,$__$\mathcal{F}$_))" Translate the Isabelle version
to a natural language version: Codex Output: "A topological space $X$ is
compact if and only if for every open cover $\mathcal{U}$ of $X$, there exists
a finite subcover $\mathcal{F}$ of $\mathcal{U}$".

_lemma_ compactin_subtopology:  "compactin (subtopology X S) T
_$\longleftrightarrow$_ compactin X T  _$\wedge$_ T  _$\subseteq$_ S"
Translate the Isabelle version to a natural language version: Codex Output:
"$T$ is compact in $S$ if and only if $T$ is compact in $X$ and $T\subseteq
S$".

_lemma_ closedin_compact_space: "_$\mathopen{[\mkern-3.0mu[}$_ compact_space
X; closedin X S _$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ compactin
X S" Translate the Isabelle version to a natural language version: Codex
Output: "If $X$ is a compact space and $S$ is a closed subset of $X$, then $S$
is a compact space".

_lemma_ compactin_discrete_topology: "compactin (discrete_topology X) S
_$\longleftrightarrow$_ S  _$\subseteq$_ X  _$\wedge$_ finite S" Translate the
Isabelle version to a natural language version: Codex Output: "$S$ is compact
in the discrete topology on $X$ if and only if $S$ is a finite subset of $X$".

_lemma_ image_compactin:  _assumes_ cpt: "compactin X S"  _and_ cont:
"continuous_map X Y f"  _shows_ "compactin Y (f ‘ S)" Translate the Isabelle
version to a natural language version: Codex Output: "If $S$ is compact in $X$
and $f$ is continuous from $X$ to $Y$, then $f(S)$ is compact in $Y$".

_lemma_ continuous_on_open: "continuous_on S f  _$\longleftrightarrow$_
(_$\forall\,$_ T. openin (top_of_set (f ‘ S)) T  _$\longrightarrow$_ openin
(top_of_set S) (S  _$\cap$_ f -‘ T))" Translate the Isabelle version to a
natural language version: Codex Output: "$f$ is continuous on $S$ if and only
if for any open set $T$ in $f(S)$, $f^{-1}(T)$ is open in $S$".

_lemma_ continuous_closedin_preimage_gen:  _assumes_ "continuous_on S f" "f ‘
S  _$\subseteq$_ T"  "closedin (top_of_set T) U"  _shows_ "closedin
(top_of_set S) (S  _$\cap$_ f -‘ U)" Translate the Isabelle version to a
natural language version: Codex Output: "If $f$ is continuous on $S$ and
$f(S)\subseteq T$, and $U$ is closed in $T$, then $S\cap f^{-1}(U)$ is closed
in $S$".

_theorem_ Casorati_Weierstrass:  _assumes_ "open M" "z  _$\in$_ M" "f
holomorphic_on (M - {z})"  _and_ "_$\bigwedge$_ l.  _$\neg$_ (f
_$\xrightarrow{\hphantom{AAA}}$_ l) (at z)"  "_$\bigwedge$_ l.  _$\neg$_
((inverse  _$\circ$_ f)  _$\xrightarrow{\hphantom{AAA}}$_ l) (at z)"  _shows_
"closure(f ‘ (M - {z})) = UNIV" Translate the Isabelle version to a natural
language version: Codex Output: "Let $f$ be a holomorphic function on an open
set $M$ containing $z$. If $f$ is not constant in any neighborhood of $z$ and
$f^{-1}$ is not constant in any neighborhood of $z$, then $f(M-\\{z\\})$ is
dense in $\mathbb{C}$".

_theorem_  _assumes_ "open M" "z  _$\in$_ M" "f holomorphic_on (M - {z})"
_and_ "_$\bigwedge$_ l.  _$\neg$_ (f  _$\xrightarrow{\hphantom{AAA}}$_ l) (at
z)"  "_$\bigwedge$_ l.  _$\neg$_ ((inverse  _$\circ$_ f)
_$\xrightarrow{\hphantom{AAA}}$_ l) (at z)"  _shows_ "closure(f ‘ (M - {z})) =
UNIV" Translate the Isabelle version to a natural language version: Codex
Output: "Let $M$ be an open set and $z\in M$. Let $f$ be a holomorphic
function on $M-\\{z\\}$. If $f$ is not bounded in any neighborhood of $z$ and
$\frac{1}{f}$ is not bounded in any neighborhood of $z$, then $f(M-\\{z\\})$
is dense in $\mathbb{C}$.

_theorem_ great_Picard:  _assumes_ "open M" "z  _$\in$_ M" "a  _$\not=$_ b"
_and_ holf: "f holomorphic_on (M - {z})"  _and_ fab: "_$\bigwedge$_ w. w
_$\in$_ M - {z}  _$\Longrightarrow$_ f w  _$\not=$_ a  _$\wedge$_ f w
_$\not=$_ b"  _obtains_ l  _where_ "(f  _$\xrightarrow{\hphantom{AAA}}$_ l)
(at z)   _$\vee$_ ((inverse  _$\circ$_ f)  _$\xrightarrow{\hphantom{AAA}}$_ l)
(at z)" Translate the Isabelle version to a natural language version: Codex
Output: "Let $f$ be a holomorphic function on $M-\\{z\\}$, where $M$ is an
open set and $z\in M$. If $f(z)\neq a$ and $f(z)\neq b$, then $f$ or
$\frac{1}{f}$ has a limit at $z$".

_theorem_ brouwer:  _fixes_ f :: "’a::euclidean_space  _$\Rightarrow$_ ’a"
_assumes_ S: "compact S" "convex S" "S  _$\not=$_ {}"  _and_ contf:
"continuous_on S f"  _and_ fim: "f ‘ S  _$\subseteq$_ S"  _obtains_ x  _where_
"x  _$\in$_ S"  _and_ "f x = x" Translate the Isabelle version to a natural
language version: Codex Output: "Let $f$ be a continuous function from a
compact convex set $S$ to itself. Then there exists $x\in S$ such that
$f(x)=x$".

_theorem_ Jordan_curve:  _fixes_ c :: "real  _$\Rightarrow$_ complex"
_assumes_ "simple_path c"  _and_ loop: "pathfinish c = pathstart c"  _obtains_
inner outer  _where_ "inner  _$\not=$_ {}" "open inner" "connected inner"
"outer  _$\not=$_ {}" "open outer" "connected outer" "bounded inner" "_$\neg$_
bounded outer" "inner  _$\cap$_ outer = {}" "inner  _$\cup$_ outer = -
path_image c" "frontier inner = path_image c" "frontier outer = path_image c"
Translate the Isabelle version to a natural language version: Codex Output:
"Let $c$ be a simple closed curve. Then there exist two disjoint open sets $U$
and $V$ such that $U$ is bounded, $V$ is unbounded, $U\cup
V=\mathbb{C}\setminus c$, $U\cap V=\emptyset$, $\partial U=c$, and $\partial
V=c$".

_corollary_ Jordan_disconnected:  _fixes_ c :: "real  _$\Rightarrow$_ complex"
_assumes_ "simple_path c" "pathfinish c = pathstart c"  _shows_ "_$\neg$_
connected(- path_image c)" Translate the Isabelle version to a natural
language version: Codex Output: "If $c$ is a simple closed curve, then
$R^{2}-c$ is not connected".

_theorem_ inverse_squares_sums: "(_$\lambda$_ n. 1 / (n + 1)_2_) sums (pi _2_
/ 6)" Translate the Isabelle version to a natural language version: Codex
Output: "Find the sum of the series $\sum_{i=1}^{\infty}\frac{1}{(i+1)^{2}}$.
The final answer is $\frac{\pi^{2}}{6}$".

_proposition_ connected_space_product_topology:
"connected_space(product_topology X I)  _$\longleftrightarrow$_ (_$\Pi$__E_ i
_$\in$_ I. topspace (X i)) = {}  _$\vee$_ (_$\forall\,$_ i  _$\in$_ I.
connected_space(X i))" Translate the Isabelle version to a natural language
version: Codex Output: "The product topology of a family of topological spaces
is connected if and only if the product of the topological spaces is empty or
each topological space is connected".

_theorem_ (_in_ ring_of_sets) caratheodory’:  _assumes_ posf: "positive M f"
_and_ ca: "countably_additive M f"  _shows_ "_$\exists\,$__$\mu$_ :: ’a set
_$\Rightarrow$_ ennreal.  (_$\forall\,$_ s  _$\in$_ M.  _$\mu$_ s = f s)
_$\wedge$_ measure_space  _$\Omega$_ (sigma_sets  _$\Omega$_ M)  _$\mu$_ "
Translate the Isabelle version to a natural language version: Codex Output:
"Let $M$ be a $\sigma$-algebra on $\Omega$, and $f$ be a positive countably
additive function on $M$. Then there exists a measure $\mu$ on $M$ such that
$\mu(s)=f(s)$ for all $s\in M$ and $(\Omega,M,\mu)$ is a measure space".

_lemma_ sigma_finite_density_unique:  _assumes_ borel: "f  _$\in$_
borel_measurable M" "g  _$\in$_ borel_measurable M"  _and_ fin:
"sigma_finite_measure (density M f)" _shows_ "density M f = density M g
_$\longleftrightarrow$_ (AE x in M. f x = g x)" Translate the Isabelle version
to a natural language version: Codex Output: "Let $f$ and $g$ be two
measurable functions on a sigma-finite measure space $M$. Then $f$ and $g$ are
equal almost everywhere if and only if the measures $\mu_{f}$ and $\mu_{g}$
are equal".

_lemma_ mvt_simple:  _fixes_ f :: "real  _$\Rightarrow$_ real"  _assumes_ "a <
b"  _and_ derf: "_$\bigwedge$_ x.  _$\mathopen{[\mkern-3.0mu[}$_ a  _$\leq$_
x; x  _$\leq$_ b _$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ (f
has_derivative f’ x) (at x within {a..b})"  _shows_ "_$\exists\,$_ x
_$\in$_{a<..<b}. f b - f a = f’ x (b - a)" Translate the Isabelle version to a
natural language version: Codex Output: "Let $f$ be a function defined on
$[a,b]$ and differentiable on $(a,b)$. Then there exists a point $c\in(a,b)$
such that $f(b)-f(a)=f^{\prime}(c)(b-a)$".

_theorem_ second_countable_borel_measurable:  _fixes_ X ::
"’a::second_countable_topology set set"  _assumes_ eq: "open =
generate_topology X"  _shows_ "borel = sigma UNIV X" Translate the Isabelle
version to a natural language version: Codex Output: "Let $X$ be a set of open
sets in a second countable topology. Then the Borel $\sigma$-algebra is the
$\sigma$-algebra generated by $X$".

_theorem_ borel_measurable_ereal_iff_real:  _fixes_ f :: "’a  _$\Rightarrow$_
ereal"  _shows_ "f  _$\in$_ borel_measurable M  _$\longleftrightarrow$_
((_$\lambda$_ x. real_of_ereal (f x))  _$\in$_ borel_measurable M  _$\wedge$_
f -‘ {_$\infty$_}   _$\cap$_ space M  _$\in$_ sets M  _$\wedge$_ f -‘
{-_$\infty$_}  _$\cap$_ space M  _$\in$_ sets M)" Translate the Isabelle
version to a natural language version: Codex Output: "Let $f$ be a function
from $M$ to $\mathbb{R}$, then $f$ is measurable if and only if $f$ is
measurable and $f^{-1}(\infty)$ and $f^{-1}(-\infty)$ are measurable sets".

_theorem_ condensation_test:  _assumes_ mono: "_$\bigwedge$_ m. 0 < m
_$\Longrightarrow$_ f (Suc m)  _$\leq$_ f m"  _assumes_ nonneg: "_$\bigwedge$_
n. f n  _$\geq$_ 0"  _shows_ "summable f  _$\longleftrightarrow$_ summable
(_$\lambda$_ n. 2^n * f (2^n))" Translate the Isabelle version to a natural
language version: Codex Output: "Let $f$ be a non-negative function such that
$f(n+1)\leq f(n)$ for all $n$. Prove that $f$ is summable if and only if
$2^{n}f(2^{n})$ is summable".

_theorem_ ratio_test_convergence:  _fixes_ f :: "nat  _$\Rightarrow$_ real"
_assumes_ pos_f: "eventually (_$\lambda$_ n. f n > 0) sequentially"  _defines_
"l  _$\equiv$_ liminf (_$\lambda$_ n. ereal (f n / f (Suc n)))"  _assumes_ l:
"l > 1"  _shows_ "summable f" Translate the Isabelle version to a natural
language version: Codex Output: "Let $f$ be a positive function, and let $l$
be the limit inferior of the sequence $\frac{f(n)}{f(n+1)}$. If $l>1$, then
$f$ is summable".

_theorem_ Stone_Weierstrass_polynomial_function:  _fixes_ f ::
"’a::euclidean_space  _$\Rightarrow$_ ’b::euclidean_space"  _assumes_ S:
"compact S"  _and_ f: "continuous_on S f"  _and_ e: "0 < e"  _shows_
"_$\exists\,$_ g. polynomial_function g  _$\wedge$_ (_$\forall\,$_ x  _$\in$_
S. norm(f x - g x) < e)" Translate the Isabelle version to a natural language
version: Codex Output: "Let $f$ be a continuous function on a compact set $S$.
Then there exists a polynomial function $g$ such that $\forall x\in
S,|f(x)-g(x)|<\epsilon$.

_theorem_ Riemann_mapping_theorem: "open S  _$\wedge$_ simply_connected S
_$\longleftrightarrow$_ S = {}  _$\vee$_ S = UNIV  _$\vee$_ (_$\exists\,$_ f
g. f holomorphic_on S  _$\wedge$_ g holomorphic_on ball 0 1  _$\wedge$_
(_$\forall\,$_ z  _$\in$_ S. f z  _$\in$_ ball 0 1  _$\wedge$_ g(f z) = z)
_$\wedge$_ (_$\forall\,$_ z  _$\in$_ ball 0 1. g z  _$\in$_ S  _$\wedge$_ f(g
z) = z))" Translate the Isabelle version to a natural language version: Codex
Output: "Let $S$ be a simply connected open set. Then $S$ is either empty, the
whole plane, or there exists a holomorphic function $f$ from $S$ to the unit
disk and a holomorphic function $g$ from the unit disk to $S$ such that
$g\circ f$ is the identity function on $S$ and $f\circ g$ is the identity
function on the unit disk."

_theorem_ Residue_theorem:  _fixes_ s pts::"complex set"  _and_ f::"complex
_$\Rightarrow$_ complex"  _and_ g::"real  _$\Rightarrow$_ complex"  _assumes_
"open s" "connected s" "finite pts"  _and_ holo:"f holomorphic_on s-pts"
_and_ "valid_path g"  _and_ loop:"pathfinish g = pathstart g"  _and_
"path_image g  _$\subseteq$_ s-pts"  _and_ homo:"_$\forall\,$_ z. (z
_$\notin$_ s)  _$\longrightarrow$_ winding_number g z = 0"  _shows_
"contour_integral g f =  2 * pi *  _$\mathrm{i}$_ *(_$\sum\,$_ p _$\in$_ pts.
winding_number g p * residue f p)" Translate the Isabelle version to a natural
language version: Codex Output: "Let $f$ be a holomorphic function on a
connected open set $S$ and let $g$ be a closed path in $S$ that does not pass
through any of the points in the finite set $P$. Then $\int_{g}f(z)dz=2\pi
i\sum_{p\in P}Res(f,p)$".

_theorem_ integer_winding_number: "_$\mathopen{[\mkern-3.0mu[}$_ path
_$\gamma$_ ; pathfinish  _$\gamma$_ = pathstart  _$\gamma$_ ;  z  _$\notin$_
path_image  _$\gamma$__$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_
winding_number   _$\gamma$_ z  _$\in$_  __" Translate the Isabelle version to
a natural language version: Codex Output: "Let $\gamma$ be a closed path in
the complex plane, and $z$ be a point not on $\gamma$. Then the winding number
of $\gamma$ around $z$ is an integer".

_lemma_ winding_number_eq: "_$\mathopen{[\mkern-3.0mu[}$_ path  _$\gamma$_ ;
pathfinish  _$\gamma$_ = pathstart  _$\gamma$_ ; w  _$\in$_ S; z  _$\in$_ S;
connected S;  S  _$\cap$_ path_image  _$\gamma$_ =
{}_$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ winding_number
_$\gamma$_ w = winding_number  _$\gamma$_ z" Translate the Isabelle version to
a natural language version: Codex Output: "Let $\gamma$ be a closed path in
the plane, and let $w,z$ be two points in the plane. If $\gamma$ does not pass
through $w$ or $z$, and $w,z$ are in the same connected component of the
plane, then the winding number of $\gamma$ about $w$ is the same as the
winding number of $\gamma$ about $z$".

_corollary_ winding_number_zero_outside: "_$\mathopen{[\mkern-3.0mu[}$_ path
_$\gamma$_ ; convex s; pathfinish  _$\gamma$_ = pathstart  _$\gamma$_ ; z
_$\notin$_ s; path_image  _$\gamma$_  _$\subseteq$_ s
_$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ winding_number  _$\gamma$_
z = 0" Translate the Isabelle version to a natural language version: Codex
Output: "If $\gamma$ is a path, $s$ is a convex set, $\gamma$ is a closed
path, $z$ is not in $s$, and $\gamma$ is in $s$, then the winding number of
$\gamma$ around $z$ is 0".

_lemma_ winding_number_zero_at_infinity:  _assumes_  _$\gamma$_ : "path
_$\gamma$_ "  _and_ loop: "pathfinish  _$\gamma$_ = pathstart  _$\gamma$_ "
_shows_ "_$\exists\,$_ B.  _$\forall\,$_ z. B  _$\leq$_ norm z
_$\longrightarrow$_ winding_number  _$\gamma$_ z = 0" Translate the Isabelle
version to a natural language version: Codex Output: "Let $\gamma$ be a closed
path, then there exists a constant $B$ such that for all $z$, if $|z|>B$, then
the winding number of $\gamma$ at $z$ is 0".

_lemma_ winding_number_homotopic_paths:  _assumes_ "homotopic_paths (-{z}) g
h"  _shows_ "winding_number g z = winding_number h z" Translate the Isabelle
version to a natural language version: Codex Output: "If $g$ and $h$ are
homotopic paths in $\mathbb{C}-\\{z\\}$, then the winding number of $g$ around
$z$ is equal to the winding number of $h$ around $z$".

_lemma_ simple_closed_path_winding_number_cases:  _assumes_ "simple_path
_$\gamma$_ " "pathfinish  _$\gamma$_ = pathstart  _$\gamma$_ "  "z  _$\notin$_
path_image  _$\gamma$_ "  _shows_ "winding_number  _$\gamma$_ z  _$\in$_
{-1,0,1}" Translate the Isabelle version to a natural language version: Codex
Output: "If $\gamma$ is a simple closed path, $z$ is not in the image of
$\gamma$, then the winding number of $\gamma$ at $z$ is either -1, 0 or 1".

_corollary_ Cauchy_theorem_primitive:  _assumes_ "_$\bigwedge$_ x. x  _$\in$_
S  _$\Longrightarrow$_ (f has_field_derivative f’ x) (at x within S)"  _and_
"valid_path g" "path_image g  _$\subseteq$_ S"  "pathfinish g = pathstart g"
_shows_ "(f’ has_contour_integral 0) g" Translate the Isabelle version to a
natural language version: Codex Output: "If $f$ is a function with a
derivative $f^{\prime}$ on a set $S$, and $g$ is a closed path in $S$, then
$\int_{g}f^{\prime}(z)dz=0$".

_theorem_ (_in_ prob_space) central_limit_theorem_zero_mean:  _fixes_ X ::
"nat  _$\Rightarrow$_ ’a  _$\Rightarrow$_ real"  _and_  _$\mu$_ :: "real
measure"  _and_  _$\sigma$_ :: real  _and_ S :: "nat  _$\Rightarrow$_ ’a
_$\Rightarrow$_ real"  _assumes_ X_indep: "indep_vars (_$\lambda$_ i. borel) X
UNIV"  _and_ X_mean_0: "_$\bigwedge$_ n. expectation (X n) = 0"  _and_
_$\sigma$_ _pos: "_$\sigma$_ > 0"  _and_ X_square_integrable: "_$\bigwedge$_
n. integrable M (_$\lambda$_ x. (X n x)_2_)"  _and_ X_variance: "_$\bigwedge$_
n. variance (X n) =  _$\sigma$__2_ "  _and_ X_distrib: "_$\bigwedge$_ n. distr
M borel (X n) =  _$\mu$_ "  _defines_ "S n  _$\equiv$_  _$\lambda$_ x.
_$\sum\,$_ i<n. X i x"  _shows_ "weak_conv_m (_$\lambda$_ n. distr M borel
(_$\lambda$_ x. S n x / sqrt (n *  _$\sigma$__2_))) std_normal_distribution"
Translate the Isabelle version to a natural language version: Codex Output:
"Let $X_{1},X_{2},\cdots$ be a sequence of independent random variables with
mean 0 and variance $\sigma^{2}$. Let $S_{n}=\sum_{i=1}^{n}X_{i}$. Then
$S_{n}/\sqrt{n\sigma^{2}}$ converges in distribution to a standard normal
distribution".

_proposition_ compact_space_product_topology: "compact_space(product_topology
X I)  _$\longleftrightarrow$_ topspace(product_topology X I) = {}  _$\vee$_
(_$\forall\,$_ i  _$\in$_ I. compact_space(X i))" Translate the Isabelle
version to a natural language version:  Codex Output: "If $X_{i}$ is a compact
space for all $i\in I$, then $X_{1}\times X_{2}\times\cdots\times X_{n}$ is a
compact space".

Lemma statements in the remainder of this section are from the _Topology_
entry in the AFP.333https://www.isa-
afp.org/browser_info/current/AFP/Topology/Topology.html All the natural
language version is generated by the Codex model.

_lemma_ seteqI: "_$\mathopen{[\mkern-3.0mu[}$__$\bigwedge$_ x. x _$\in$_ A
_$\Longrightarrow$_ x _$\in$_ B;  _$\bigwedge$_ x. x _$\in$_ B
_$\Longrightarrow$_ x _$\in$_ A  _$\mathclose{]\mkern-3.0mu]}$_
_$\Longrightarrow$_ A = B" Translate the Isabelle version to a natural
language version: Codex Output: "If $A$ and $B$ are sets such that $A\subseteq
B$ and $B\subseteq A$, then $A=B$."

_lemma_ (_in_ carrier) openI: "m  _$\in$_ T  _$\Longrightarrow$_ m open"
Translate the Isabelle version to a natural language version: Codex Output:
"If $m$ is a topology on a set $T$, then $m$ is open."

_lemma_ (_in_ carrier) openE: "_$\mathopen{[\mkern-3.0mu[}$_ m open; m
_$\in$_ T  _$\Longrightarrow$_ R  _$\mathclose{]\mkern-3.0mu]}$_
_$\Longrightarrow$_ R" Translate the Isabelle version to a natural language
version: Codex Output: "If $m$ is an open set in a topological space $T$, then
$m\in T$."

_lemma_ (_in_ topology) open_kriterion:  _assumes_ t_contains_open:
"_$\bigwedge$_ x. x _$\in$_ t  _$\Longrightarrow$_  _$\exists\,$_ t’. t’ open
_$\wedge$_ x _$\in$_ t’  _$\wedge$_ t’ _$\subseteq$_ t"  _shows_ "t open"
Translate the Isabelle version to a natural language version:  Codex Output:
"If $t$ is a subset of a topological space $T$ such that for every $x\in t$,
there exists an open set $t^{\prime}$ such that $x\in t^{\prime}$ and
$t^{\prime}\subseteq t$, then $t$ is open."

_lemma_ (_in_ carrier) carrierI [intro]: "_$\mathopen{[\mkern-3.0mu[}$_ t
open; x  _$\in$_ t  _$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ x
_$\in$_ carrier" Translate the Isabelle version to a natural language version:
"If $t$ is an open set in a topological space $T$ and $x\in t$, then $x\in
T$."

_lemma_ (_in_ topology) Un_open [intro!]:  _assumes_ abopen: "A open" "B open"
_shows_ "A  _$\cup$_ B open" Translate the Isabelle version to a natural
language version: Codex Output: "If $A$ and $B$ are open sets in a topological
space $T$, then $A\cup B$ is open."

_lemma_ topologyI: "_$\mathopen{[\mkern-3.0mu[}$__$\bigwedge$_ x y.
_$\mathopen{[\mkern-3.0mu[}$_ is_open T x; is_open T y
_$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ is_open T (x  _$\cap$_ y);
_$\bigwedge$_ M.  _$\forall\,$_ m  _$\in$_ M. is_open T m  _$\Longrightarrow$_
is_open T (_$\bigcup\,$_ M)  _$\mathclose{]\mkern-3.0mu]}$_
_$\Longrightarrow$_ topology T" Translate the Isabelle version to a natural
language version: Codex Output: "If $T$ is a set and $T$ is closed under
finite intersections and arbitrary unions, then $T$ is a topology."

_lemma_ (_in_ topobase) topo_open: "t open = (t  _$\in$_ topo B)" Translate
the Isabelle version to a natural language version: Codex Output: "If $B$ is a
topological base of a topological space $T$, then $t$ is open if and only if
$t\in B$."

_lemma_ (_in_ topobase) topo_induct [case_names basic inter union, induct set:
topo, consumes 1]:  _assumes_ opn: "x open"  _and_ bas: "_$\bigwedge$_ x. x
_$\in$_ B  _$\Longrightarrow$_ P x"  _and_ int: "_$\bigwedge$_ x y.
_$\mathopen{[\mkern-3.0mu[}$_ x open; P x; y open; P y
_$\mathclose{]\mkern-3.0mu]}$_  _$\Longrightarrow$_ P (x  _$\cap$_ y)"  _and_
uni: "_$\bigwedge$_ M. (_$\forall\,$_ t _$\in$_ M. t open  _$\wedge$_ P t)
_$\Longrightarrow$_ P (_$\bigcup\,$_ M)"  _shows_ "P x" Translate the Isabelle
version to an natural language version: Codex Output: "If $B$ is a topological
base of a topological space $T$, then $P(x)$ holds for all open sets $x$ if
$P(x)$ holds for all $x\in B$ and $P(x)$ is closed under finite intersections
and arbitrary unions."