# Towards a mathematics formalisation assistant using large language models

Ayush Agrawal
Microsoft Research
Bangalore, India
<EMAIL_ADDRESS>&Siddhartha Gadgil
Department of Mathematics
Indian Institute of Science
Bangalore, India
<EMAIL_ADDRESS>
&Navin Goyal
Microsoft Research
Bangalore, India
<EMAIL_ADDRESS>&Ashvni Narayanan 11footnotemark: 1
London School of Geometry and Number Theory
London, UK
<EMAIL_ADDRESS>&Anand Rao Tadipatri 11footnotemark: 1
Indian Institute of Science Education and Research
Pune, India
<EMAIL_ADDRESS>Equal contribution, names are in
alphabetical order

###### Abstract

Mathematics formalisation is the task of writing mathematics (i.e.,
definitions, theorem statements, proofs) in natural language, as found in
books and papers, into a formal language that can then be checked for
correctness by a program. It is a thriving activity today, however
formalisation remains cumbersome. In this paper, we explore the abilities of a
large language model (Codex) to help with formalisation in the Lean theorem
prover. We find that with careful input-dependent prompt selection and
postprocessing, Codex is able to formalise short mathematical statements at
undergrad level with nearly 75% accuracy for $120$ theorem statements. For
proofs quantitative analysis is infeasible and we undertake a detailed case
study. We choose a diverse set of $13$ theorems at undergrad level with proofs
that fit in two-three paragraphs. We show that with a new prompting strategy
Codex can formalise these proofs in natural language with at least one out of
twelve Codex completion being easy to repair into a complete proof. This is
surprising as essentially no aligned data exists for formalised mathematics,
particularly for proofs. These results suggest that large language models are
a promising avenue towards fully or partially automating formalisation.

##  1 Introduction

Mathematics (definitions, theorems, proofs, remarks) as found in books and
papers is written in a semi-formal style combining natural language with
formal language in specialized notation. We refer to the language of this
style of writing mathematics as _natural language_ or NL. _Formalisation of
mathematics_ consists of writing mathematics in a _formal language_ that can
then be checked and manipulated by a computer. NL mathematics writing, while
being more rigorous than writing in most other domains, falls far short of the
standard of detail and rigour required for full formalisation. Formalisation
is done with the help of _proof assistants_. A proof assistant consists of a
formal language in which mathematical statements can be encoded along with a
piece of software that assists in writing and checking proofs in the formal
language up to the foundational axioms. See under Prompt in Figure 1 for some
examples. Formalisation is an old endeavour that is thriving with several
actively developed libraries of formalised mathematics for major proof
assistants including Coq, Isabelle, Lean and Mizar. A major use of proof
assistants is in software and hardware verification but here we are concerned
with their applications in mathematics: checking formalised mathematics
automatically results in a much higher degree of confidence in the correctness
of proofs. Formalisation promises to open up new possibilities in mathematical
exposition, teaching, research and collaboration (Massot, 2021; Buzzard,
2022); in addition, it can facilitate automated proof discovery, e.g. (Lample
et al., 2022).

Formalisation of mathematics today poses a barrier to entry because of the
need to learn to use proof assistants; it is also notoriously labour-intensive
because many details normally taken for granted in the language of mathematics
must be supplied when formalising. _Autoformalisation_ Wang et al. (2018) is
the task of (semi-)automatically turning a piece of mathematics in natural
language into a formalised one. An autoformalisation tool that speeds-up
formalisation or fully automates it would be of great value by enabling the
above advantages of formalisation and opening up new ones Szegedy (2020).

Autoformalisation is challenging. It is a natural language understanding
problem for the language of mathematics. While the language of mathematics is
stylized compared to natural language in other domains and deals with
relatively narrow subject matter, it retains much of the complexity in
addition to presenting new challenges for autoformalisation of its own,
including supplying missing details and assumptions that are taken for granted
by humans, and semantically mapping concepts in the informal description to
those in the formal corpus (Ganesalingam, 2013; Massot, 2021).

Autoformalisation also presents practical challenges in the application of
modern deep learning-based methods: the amount of formalised mathematics
available is much smaller than code in major programming languages.
Furthermore, there is very little aligned data between informal and formal
mathematics. Autoformalisation implicitly includes semantic search in the
formalised library. Autoformalisation of proofs is much more than independent
autoformalisation of each statement in the proof: one needs to maintain
context across the proof and find correspondence between NL constructs and
tactics in formal proofs.

In this paper we worked with Lean, a popular proof assistant with two actively
used versions: Lean 3 (de Moura et al., 2015) and Lean4 (de Moura & Ullrich,
2021). The rapidly evolving Lean mathematical library (abbreviated mathlib) is
one of the largest libraries of formal mathematics. mathlib is currently 226MB
in size. mathlib is monolithic by design, ensuring that formalisations of
different parts of mathematics can be combined easily. The resulting
standardization of terminology in mathlib and its good coverage make Lean an
attractive target for autoformalisation.

To our knowledge, the only form in which aligned data occurs in mathlib is as
docstrings for definitions and theorem statements. Furthermore, there is a
complete lack of aligned data for proofs: while some examples of natural
language proofs together with their corresponding formal proofs occur in the
blueprints of some Lean formalisation projects, e.g. the Liquid Tensor
Experiment, these are only a handful and highly specialised.

Our contributions. In this paper we apply a large language model
(specifically, Codex) to the problem of autoformalisation. We focused on two
different tasks: (1) translating theorem statements of a form similar to
docstrings of mathlib to theorems (in Lean 4), and (2) translating (outlines
of) NL proofs to Lean proofs (in Lean 3). The latest version of Lean, Lean 4,
is (in addition to an interactive theorem prover) a full-fledged programming
language with a fast runtime. This allows a seamless integration of proofs,
programs and meta-programs. We use Lean 4 for one set of experiments and Lean
3 for the other because, at the time of writing, mathlib was only partially
available in Lean 4 (via a partial binary port). Hence we use Lean 4 where its
additional capabilities are important and Lean 3 where these are not used and
the larger library is of greater value. More details on Lean are in Appendix
A.

Theorem statement autoformalisation. For the evaluation dataset, we chose
$120$ theorem statements at the undergrad level so that the relevant concepts
(background theory and definitions) were mostly already in mathlib. Since
mathlib is substantial (it has a significant fraction of undergrad mathematics
curriculum apart from many advanced results), this is not a restriction. We
focused on theorem statements at the undergrad and more advanced level from
various areas of mathematics. These statements tend to be more challenging for
autoformalisation compared to mathematics competition problems studied in
prior work (Wu et al., 2022) as they often assume more in terms of implicit
context and draw from a much larger background (Wu et al., 2022).

We experimented with using input-dependent prompting, with mathlib as a
database. Specifically, we chose our few-shot prompts to consist of theorem-
docstring pairs from mathlib where the docstring is close in a sentence
similarity metric to the statement to be formalised. We also experimented with
filtering outputs generated at high temperatures by checking validity in Lean
4 and some other post-processing.

Our results showed that there is a strong effect of both prompt engineering
and selection, and even more when used in combination and that a reasonably
large fraction are elaborated when both prompt engineering and selection is
done (the results improve further when more prompts are used).

In the context of autoformalisation, we are the first to use input-dependent
prompting. Our use of elaboration for postprocessing is novel. Both of these
are greatly facilitated by the availability of mathlib, and the nature of Lean
4, which gives easy access to its internals and in Lean 4 itself – the latter
allowing shared code and avoiding context switching.

Autoformalisation of proofs. We chose an evaluation dataset of 13 NL theorems
and their proofs. (Due to the lack of data for proofs and need for manual
inspection of the outputs, a larger scale study was infeasible.) The theorem
statements are at the undergrad level with a proof fitting in two-three
paragraphs. They are diverse across several axes: (1) proof techniques such as
proof by contradiction, induction, algebraic manipulations etc., (2) domains
such as topology, analysis, group theory, linear algebra, representation
theory, and algebraic number theory, (3) difficulty level.

Our chosen proofs are much longer than a typical theorem statement and we
didn’t observe Codex outputting a completely correct proof. We instead relaxed
the requirement of autoformalisation to produce a (faulty) proof that is easy
to repair for humans, saving time and effort compared to formalising from
scratch. We experimented with several output formal proof formats depending on
the level of detail, and with or without NL comments interspersed in the
proofs. We designed fixed few-shot prompts for each of these formats. We
undertook a detailed manual study of the outputs. We found that _proofs with
comments work better_ ; for about half of the formal proofs Codex output would
save significant effort and for the rest it would save some effort. Proofs
with comments is a new kind of prompting strategy in line with other recent
prompting strategies such as chain-of-thought prompting Wei et al. (2022).
Presumably, interleaving of NL comments helps Codex align its output with the
NL proof.

All of our datasets were carefully controlled for the possibility of overlap
with the training data of Codex as we discuss in more detail later in the
paper. We make all of our data available as supplementary material. In
summary, our contributions are

  * •

Design of a postprocessing technique for theorem statement autoformalisation
resulting in significantly improved performance when combined with prompt
engineering.

  * •

First study of proof autoformalisation and design of a prompting technique for
proof autoformalisation. With this technique, Codex is able to produce
_useful_ partially correct formal proofs in at least one out of thirteen
completions.

  * •

A detailed case study of proof autoformalisation which may be useful for
future work.

inline]If we make our dataset sufficiently large, that can also be a
contribution. We should allow crowdsourcing. Organisation. After discussion of
related work in Section 2, we discuss in detail autoformalisation of theorem
statements in Section 3 and of proofs in Section 4. We conclude in Section 5.

##  2 Background and related work

Natural language understanding has a long history in AI; here we can only
briefly touch upon the most relevant subfields of this large field.

Semantic parsing and program synthesis from natural language specification.
Semantic parsing is the task of translating a natural language utterance into
a logical form. Tasks are normally restricted to specific domains and the
logical forms come from a domain-specific language ranging from first-order
logic to regular expressions, e.g. (Kamath & Das, 2019; Hahn et al., 2022).

Large Language Models and mathematics. The advent of transformer-based large
language models (LLMs) for natural languages, e.g. (Devlin et al., 2018; Brown
et al., 2020), has brought about a sea change in natural language processing.
This is largely fueled by the remarkable ability of LLMs to achieve good
performance on a diverse set of tasks, ranging from translation to solving
math word problems, via few-shot demonstrations in the prompt even though the
LLMs are only trained on the language modelling objective. With careful prompt
design, these latent abilities can be further teased out, e.g., (Liu et al.,
2021; Wei et al., 2022). The input-dependent prompting we use has precedent in
prior work, e.g., Jain et al. (2022). Prompt design can be combined with
postprocessing to select the best among many answers generated at higher
temperatures, e.g., (Jain et al., 2022; Li et al., 2022; Wang et al., 2022)
based on their performance on unit tests and other metrics.

Specifically, LLMs applied to code, e.g. (Chen et al., 2021; Fried et al.,
2022), have led to new advances in program synthesis from natural language
specification. In this paper, we will be using a Codex (Chen et al., 2021)
version code-davinci-002. LLMs and related methods have been used for solving
mathematical problems (Lewkowycz et al., 2022) with natural language
solutions, for proving theorems in natural language (Welleck et al., 2022),
and for proof search, e.g. (Lample et al., 2022).

Autoformalisation. While the term _autoformalisation_ was coined in Wang et
al. (2018), the problem itself has a long history; see Wang et al. (2020).
Autoformalisation can be thought of as semantic parsing for the domain of
mathematics. Mathematics is a far larger and sophisticated domain than most
domains considered in semantic parsing.

Wang et al. (2020) applied deep learning-based methods to autoformalisation by
treating it as a language translation problem. They construct datasets for
supervised and unsupervised neural machine translation and evaluate the
syntactic distance of the output from the gold output by metrics such as BLEU
but do not provide data for correctness. The recent work Wu et al. (2022) is
closest to ours and stimulated our work. They considered statement
autoformalisation in Isabelle/HOL using LLMs. For their quantitative results,
their statements were from middle school to undergrad mathematical
competitions (Zheng et al., 2022). These problems use only elementary
concepts. Their quantitative studies are for fixed few-shot prompts. While a
direct comparison with their results is not possible due to the use of
different proof assistants and datasets, our method compares favourably with
their method (fixed few-shot prompting with greedy decoding) as shown in the
next section. Our input-dependent prompting is not applicable on their dataset
due to the lack of availability of aligned data at the elementary level of
statements in their datasets. Lean Chat is a fixed-prompt autoformalisation
tool for Lean 3 based on Codex.

##  3 Autoformalising theorem statements

Here we discuss autoformalisation of theorem statements.

###  3.1 Evaluation datasets

We used three test sets with $40$ natural language statements each. The
natural language statements were of the same form as typical doctrings in
mathlib: single sentences often with Lean code fragments (including names and
formulas not in LaTeX but in unicode) enclosed in backticks. We call such
strings docstring-style strings.

Our first set consisted of mathematical theorems (some were conjectures as
well) in areas well-represented by mathlib, such as undergraduate-level number
theory, group theory and topology.

The other two sets were designed to minimize contamination due to similar
results being in the training of Codex. Our second set consisted of what we
called _silly statements_ , such as _every vector space with dimension 2 is
finite dimensional_. While being true, these were easy and/or absurdly
specific, so unlikely to appear in this precise form anywhere else. We created
this set by looking at theorems in mathlib and modifying them.

The third set consisted of _false statements_ : these obviously cannot appear
in any library. The statements in this set were closely related to those in
mathlib or our first dataset: for example, while our first dataset had the
statement _every field is a ring_ our third dataset had its (false) converse
_every ring is a field_.

###  3.2 Techniques

We used Codex to translate an input text in natural language to code in Lean
4. Codex takes as input a prompt and returns completion(s). We generated a
prompt from the input text and post-processed completions as described below.
Figure 1 is an example of a prompt, the initial result (with one completion
shown) and the result after post-processing. We remark that this example needs
prompt engineering, as we see in Section 3.3.

Input text: “If a vector space has dimension ‘2‘ then it is finite
dimensional.” Prompt: ⬇ /– If a vector space has a finite basis, then it is
finite-dimensional. -/  theorem {K : Type u} {V : Type v} [division_ring K]
[add_comm_group V] [module K V] {ι : Type w} [fintype ι] (h : basis ι K V) :
finite_dimensional K V :=  …  /– A vector space has dimension at most ‘1‘ if
and only if there is a single vector of which all vectors are multiples. -/
theorem {K : Type u} {V : Type v} [division_ring K] [add_comm_group V] [module
K V] : module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v :=
/– If a vector space has dimension ‘2‘ then it is finite dimensional. -/
theorem Codex Completion: ⬇ {K : Type u} {V : Type v} [division_ring K]
[add_comm_group V] [module K V] (h : module.rank K V = 2) : finite_dimensional
K V Post-processed code in Lean 4: ⬇ theorem ∀ {K : Type u} {V : Type v} [inst
: DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
Module.rank K V = 2 → FiniteDimensional K V Figure 1: Example of a prompt, the
initial result and the result after post-processing. Part of the prompt was
elided to save space; full prompt appears in Appendix B.1.

Prompt engineering. Given an input text to be translated, we chose example
prompts from mathlib whose docstrings are similar to the input text. We used
two notions of similarity: proximity in sentence embeddings (described further
in Section B.4) and keyword matching (described further in Section B.5), with
the number of sentences chosen by the user. This style of prompt design
appears in the previous work, e.g., Jain et al. (2022). The docstrings and the
corresponding Lean code were extracted from mathlib documentation. From these
a prompt was constructed as in Figure 1 following a template, with the prompt
consisting of the example doc-strings followed by theorem statements
essentially in the same syntax as Lean Code and doc-strings, followed by the
statement to be translated in the format of a doc-string and an incomplete
line with the word “theorem”.

Post processing. Lean 4 code is compiled in two phases: a parser converts a
string into a _Syntax_ object, and an elaborator converts a _Syntax_ object
into a type-correct expression. The elaboration step is a much stricter
analogue of type-checking in a strongly-typed language. It is roughly a formal
analogue of supplying all the implicit details in an NL theorem statement.
Lean 4 is unique among proof assistants in being implemented in Lean 4 and
providing an interpreter API, which facilitates our implementation.

We parsed the Codex completions, translated from Lean 3 to Lean 4 and auto-
corrected (as described in Section B.2) to obtain Syntax objects corresponding
to (syntactically valid) completions. We attempted to elaborate each of these.
Thus, restriction to completions which are successfully parsed and elaborated
gives a strong filter.

###  3.3 Results

We tested the effects of the prompt engineering and post-processing as well as
the final quality of translations for the datasets described in Section 3.1.

Success rates for the Elaborater We begin with quantitative results showing
the utility of both prompt engineering and elaboration filtering for the
datasets described in Section 3.1. By elaboration filtering we mean that of
the many (typically 15-20) completions returned by Codex, we only consider
those which are successfully parsed and elaborated. We emphasize that by using
the features of Lean 4 the elaboration filtering was programmatic and
efficient (which would not be case, for instance, if each completion was used
to generate a program which was checked by an external compiler).

We summarize the number of statements that were elaborated for each of the
three sets of statements in Table 1. For each set, we considered results with
$4$ fixed prompts (those used by Lean Chat) and $4$ prompts chosen by sentence
similarity. For each of these cases we considered answers chosen greedily
(i.e., temperature 0 and 1 completion) and those obtained by choosing several
completions at temperature $0.8$ with filtering and selection. We made three
runs for each configuration, and the result reported is the _median_. We also
ran a configuration with the Codex recommended default temperature $0.2$ and
with fixed prompts. The results of this are included in parentheses in the
entries for the greedy case. As $11$ of the theorem statements were present in
mathlib we also ran all the configurations excluding these and obtained
similar results as above: in particular $23$ of the $29$ statements were
elaborated with prompt engineering and selection.

We see in the next section that elaboration is a good proxy measure for
accuracy. Thus, we can justify the claims made in 1.

| Theorems | Silly Statements | False Statements
---|---|---|---
| Fixed | Input-dependent | Fixed | Input-dependent | Fixed | Input-dependent
Greedy | 20 (18) | 21 | 19 (21) | 28 | 15 (16) | 23
Filtered | 25 | 29 | 29 | 34 | 24 | 30
Table 1: Numbers of elaborated statements; numbers in parenthesis are for temperature $0.2$ (instead of $0$) with one completion | false statements | silly statements | theorem statements
---|---|---|---
Elaborated | 32 | 34 | 33
Correct | 21 | 26 | 30
Some correct | 28 | 32 | 30
All wrong | 4 | 2 | 3
Table 2: Correctness of elaborated statements

The example in Figure 1 illustrates the effect of prompt engineering. None of
the $15$ completions were elaborated in all the three runs with the fixed
(Lean Chat) prompts. The completions often used the wrong name from mathlib or
assumed a definition was at a different level of abstraction (e.g., modules
versus vector spaces) from that of mathlib. We also saw that a larger number
of examples did lead to more sentences being elaborated, but the effect was
not strong enough to quantify robustly.

Correctness of elaboration. Next, we analysed how often completions that were
successfully elaborated were correct. In the case where more than one
completion was elaborated, we considered both whether the chosen completion
was correct and whether any of the elaborated completions were correct.

For each of the three sets, we considered a configuration with high
temperature and prompt engineering – specifically, we considered the
configuration with the highest number of elaborated statements111All
configurations had temperature $0.8$; we used $10$ sentence similarity prompts
and $4$ keyword based prompts and obtained $15$ completions for theorems and
silly statements and used $12$ sentence similarity prompts and $8$ keyword
based prompts and obtained $20$ completions for false statements., as our goal
was to test elaboration as a proxy measure for correctness. We manually
checked the correctness of the selected completion for the elaborated
completions, as reported in Table 2.

Further, the statements where all completions were wrong involved some concept
for which we had very few prompts available, in part due to the incomplete
state of the binary port of mathlib, also suggesting that elaboration is a
good proxy measure.

##  4 Autoformalisation of Proofs

As discussed in Sec. 1, this task presents new difficulties on top of
autoformalisation of theorem statements. Input-dependent prompting, which was
an important ingredient in the previous section, is presently infeasible for
proofs due the the lack of aligned data for proofs. Elaboration, another
important ingredient for theorem statements, is also infeasible for proofs
since it is very rare for the language model to output a completely correct
proof. Therefore, instead of aiming for completely correct formalised proofs,
we aim for _useful_ formalised proof outputs: those that can be easily
repaired to construct a correct formalised proof, saving time and effort
compared to formalisation from scratch. With this relaxation, we see that LLMs
show promise.

###  4.1 Methodology

Evaluation dataset. We collected 13 natural language theorems and their proofs
from various sources such as ProofWiki, university courses etc., of varying
proof technique, domain and difficulty level. We carefully checked if a
similar proof is already formalised in Lean (in mathlib or elsewhere on the
internet). While in some cases a similar proof does appear, in all cases the
structure of our NL proof was significantly different or different formalisms
were used (we provide details for each theorem in Appendix D). Since we
measure autoformalisation performance according to the faithfulness of the
output proof to our NL proof, we believe there is minimal risk that our output
were memorized by Codex from its training data. We also used a few hand-
written natural language proofs. Some of these are listed below (the full list
is in Section C.1)

  1. 1.

_Absolute Value Function is Convex_ (abs_convex): Let
$f:\mathbb{R}\to\mathbb{R}$ be the absolute value function on the real
numbers. Then $f$ is convex.

  2. 2.

_Schur’s Lemma_ (schur_lemma): Let $V$ and $W$ be vector spaces; and let
$\rho_{V}$ and $\rho_{W}$ be irreducible representations of $G$ on $V$ and $W$
respectively. If $V$ and $W$ are not isomorphic, then there are no nontrivial
representations of $G$ on $V$ and $W$ respectively.

  3. 3.

_Schur’s Inequality_ (schur_ineq): Let $x,y,z\in\mathbb{R}_{\geq 0}$ be
positive real numbers such that $x\geq y\geq z\geq 0$. Let
$t\in\mathbb{R},t>0$ be a (strictly) positive real number. Then:
$x^{t}(x-y)(x-z)+y^{t}(y-z)(y-x)+z^{t}(z-x)(z-y)\geq 0$

  4. 4.

_Contraction Mapping theorem_ (contraction_mapping): Let $B$ be a Banach
space, $M$ a closed subset of $B$, and $\Phi$ a mapping from $M$ to $M$ such
that for some $k\in[0,1)$, $\|\Phi(x)-\Phi(y)\|\leq k\|x-y\|$ for any two
points $x$ and $y$ in $M$. Then there is a unique point $z$ in $M$ such that
$\Phi(z)=z$.

inline]Give all the sources, natural language proofs and meta-data in the
Appendix? inline]Should we talk about the inherent subjective bias of
selection like Natural prover paper mentioned or about the small evaluation
data size?

inline]cite Natural-prover paper inline]evaluation schema inline]Not
recognising Mathlib P of powerset

⬇ /–‘theorem‘  Power Set is Closed under Intersection Let $S$ be a set.  Let
$\powerset S$ be the power set of $S$.  Then:  :$\forall A, B \in \powerset S:
A \cap B \in \powerset S$ ‘proof‘  Let $A, B \in \powerset S$.  Then by the
definition of power set, $A \subseteq S$ and $B \subseteq S$.  From
Intersection is Subset we have that $A \cap B \subseteq A$.  It follows from
Subset Relation is Transitive that $A \cap B \subseteq S$.  Thus $A \cap B \in
\powerset S$ and closure is proved.  {{qed}}  -/  theorem
power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈ $\mathcal{P}$
S, (A ∩ B) ∈ $\mathcal{P}$ S :=  begin – $A$ and $B$ are sets. $A$ and $B$
belong to power set of $S$ assume (A : set α) (hA : A ∈ $\mathcal{P}$ S) (B :
set α) (hB : B ∈ $\mathcal{P}$ S),  – Then $A ⊆ S$ and $B ⊆ S$, by power set
definition have h1 : (A ⊆ S) ∧ (B ⊆ S), from by {split,apply
set.subset_of_mem_powerset,exact hA,apply set.subset_of_mem_powerset,exact
hB},  – Then $(A ∩ B) ⊆ A$, by intersection of set is a subset have h2 : (A ∩
B) ⊆ A, from by apply set.inter_subset_left,  – Then $(A ∩ B) ⊆ S$, by subset
relation is transitive have h3 : (A ∩ B) ⊆ S, from by {apply set.subset.trans
h2 h1.left},  – Hence $(A ∩ B) ∈ $\mathcal{P}$ S$, by power set definition
show (A ∩ B) ∈ $\mathcal{P}$ S, from by {apply set.mem_powerset h3},  end
Figure 2: One of the examples in the prompt for the full-proof-with-comments
format

Proof formats. We experimented with several _formal proof formats_ ; all
formats use forward reasoning (see Appendix A for more on forward vs. backward
reasoning). Proof formats differ in their ease of translation by a language
model and in their utility to a user. Proof formats vary across two axes: the
level of detail and whether the formal proof has comments. The three levels of
detail are the following.

Full proof. This corresponds to the complete proof.

Proof outline. This consists of the main steps of the proof listed in order.
In Lean code, an outline is given by a series of have statements with sorry as
a placeholder for the intermediate proofs. Although an outline contains far
less information than a full proof, a tool that is capable of producing good
outlines could still be valuable to a user since one could, in principle,
iteratively produce outlines of the main proof and all its steps, until one is
left with trivial steps that can handled by automation.

Proof outline with premises. This format is at an intermediate level of
detail: each proof step is listed along with a list of premises from which it
can be deduced. This is done by introducing a fictitious new Lean tactic auto
that takes as arguments the list of theorems that go into a proof along with
an optional list of Lean tactics that may be helpful.

Proofs at each level of detail can be used as is or combined with comments
(each step preceded by a comment explaining that step). This results in a
total of _six formats_. For an example, see the formal proof in Figure 2.

Prompts. We designed few-shot prompts (one for each format) for our chosen set
of theorems. The prompts consist of three theorems with corresponding proofs;
we illustrate one such theorem for full proof with comments in Figure 2 and
the full prompt can be found in Section B.1.

Hyperparameters. We initially considered four temperatures 0, 0.2, 0.4 and
0.8. We sampled three outputs for each of the latter three, and a single
output for the former.

Evaluation. To generate proofs in different formats, we queried Codex with a
prompt consisting of example natural language proofs and the corresponding
step-wise Lean proofs in the appropriate format, followed by the natural
language proof to be translated. For evaluation, we manually inspected the
generated outputs via the following grading scheme.

Theorem statement formalisation: $0$ if the output is incorrect; $1$ if the
output is somewhat correct; $2$ if the output is fully correct.

Proof formalization. $0$ if the output does not help with formalising the
complete proof; $1$ if the output slightly decreases the effort needed to
formalise the complete proof; $2$ if the output makes it substantially easier
to formalise the complete proof; $3$ if the output only needs few minor
corrections; $4$ if the output is fully correct.

As manual grading of proof output by Codex is time-consuming, after a
preliminary analysis we focused on three formats, namely those with comments,
and on temperatures 0.4 and 0.8, as the results were better in these cases.
Outputting proof formats with comments might help Codex relate the natural
language proof with the formalised Lean proof at a more granular level. Hence,
for each theorem, we analysed 18 Codex completions (6 per proof format). The
model was initially given the task of formalising the theorem statement as
well as the proof. Later, we also prompted the model with correct Lean
statements for some theorems and assigned it the task of the formalisation of
the respective proofs.

inline]example of each format?

###  4.2 Results

Overall, we found that the generated proofs were well aligned with the natural
language proofs and also well-structured as per Lean style. These proofs could
therefore be used as a good starting points for formalisation assistance as
illustrated in Figure 3. We summarise the scores given to the Codex
completions after manual inspection in Figure 6. No completion received a
perfect score of $4$. For $8$ of the $13$ theorems, at least one Codex
completion (out of $18$), was marked $3$. The other $5$ theorems got a maximum
of $2$. The main sources of lower scores were errors related to incorrect
natural language statement translations that could be mathematically
incorrect, irrelevant or invalid Lean code. Some lower scores were also due to
step repetitions. These results are given and errors analysed in detail in
Section C; here we present a synopsis.

The best proof format depended on the nature of the proof, with more detailed
formats often better (i.e., with more intermediate details) for harder to
formalise proofs, while the results were good for all formats for easy to
formalise statements. Including the correct Lean theorem statements did not
show a clear improvement. However, in the case of the lowest scoring theorem
without the correct statements, including the correct statement improved the
score from $1$ to $2$.

inline]add squeeze theorem in appendix?

Capabilities shown by Codex. In schur_ineq, the natural language proof had
statements that simply mentioned that all the terms are non-negative and
concluded the proof. Interestingly, Codex completions had these details
formalised as intermediate steps.

Codex sometimes expanded a definition instead of using the mathlib definition
directly; for example, $A=A^{T}$ instead of is_symm A. Codex also generated
plausible theorem names, which were in line with mathlib style.

Errors in completions. Occasionally the completion had invalid Lean syntax,
e.g., x ≥ y ≥ z ≥ 0 (copied directly from the natural proof) instead of the
valid Lean syntax x ≥ y ∧ y ≥ z ∧ z ≥ 0. There was an instance where Codex
generated a proof in what seemed like a different language. In some cases, we
observed that the completion used an undeclared variable in the proof. For
example, it declared t > 0 without introducing t: ℝ.

There were a few instances where proof-steps were syntactically correct but
mathematically incorrect, for instance stating |α*x + β*y| = α*|x| + β*|y|
instead of the triangle inequality.

Sometimes natural language translations were wrong, although they were
mathematically valid statements and valid Lean code. For example, in
schur_lemma, Codex confuses a homomorphism being “non-zero” with a
homomorphism being “nowhere zero”. In a proof of the contraction_mapping,
Codex defines a sequence $x$ to be $x(i):=\phi(x(i))$, instead of the
inductive definition: $x(0):=x\\_{0}$ and $x(i+1):=\phi(x(i))$.

Sometimes the Codex completion contained contradicting proof steps (even in
cases not involving proof of contradiction). As an example, in a generated
proof of schur_lemma, there were two statements, one stating that the kernel
of a homomorphism is trivial, and the next one stating the opposite.

inline]add examples for unrelated comments and lean statements inline]give
mathlib style names

Hallucinations. Codex sometimes output names that looked realistic but are not
present in mathlib, e.g. convex_function instead of convex_on.

Deviation from Natural Language Proof. Occasionally the output proof formats
deviated from the natural language proofs, with Codex merging different proofs
from distinct sources, leading to conflicting notation.

⬇ theorem abs_convex : ∀ (x y : ℝ), ∀ (α β : ℝ), α ≥ 0 ∧ β ≥ 0 ∧ α + β = 1 →
abs (α * x + β * y) ≤ (α * abs x + β * abs y) :=  begin assume (x y : ℝ) (α β
: ℝ) (h1 : α ≥ 0 ∧ β ≥ 0 ∧ α + β = 1),  – expand the absolute value function
have h2 : abs ($\alpha$ * x + $\beta$ * y) = ($\alpha$ * x + $\beta$ * y),
from by rw abs_of_nonneg (add_nonneg (mul_nonneg h1.left (abs_nonneg x))
(mul_nonneg h1.right (abs_nonneg y))), – apply the triangle inequality have h3
: abs (α * x + β * y) ≤ abs (α * x) + abs (β * y), from by apply abs_add,  –
apply the absolute value of product have h4 : abs (α * x + β * y) ≤ abs α *
abs x + abs β * abs y, from by {  rw [ $\leftarrow$ abs_mul α x, $\leftarrow$
abs_mul β y] at h3, exact h3}, – apply the absolute value definition have h5 :
abs (α * x + β * y) ≤ α * abs x + β * abs y, from by {  rw abs_of_nonneg
h1.left at h4, rw abs_of_nonneg h1.right.left at h4, exact h4}, – apply the
definition of absolute value function have h6 : abs ($\alpha$ * x + $\beta$ *
y) $\leq$ $\alpha$ * abs x + $\beta$ * abs y, from by rw abs_of_nonneg
h1.right at h5, show abs (α * x + β * y) ≤ α * abs x + β * abs y, from h6 h5,
end Figure 3: Correction of a Codex completion of _Absolute Value Function is
Convex_. The text highlighted in red is to be deleted and the text highlighted
in green and underlined is to be added.

inline]add memorization clues

##  5 Limitations and future work

With our techniques, Codex shows promising performance for autoformalisation
of docstring-style theorem statements and for proofs There are many avenues
for future work.

Using docstrings from mathlib in the present form does not give adequate
examples of complex LaTeX formulas and of some mathematical idioms. An
additional database of prompts targeting these could address this. Further, we
can make use of Lean’s easily extensible syntax to incorporate more
mathematical notation. One way to improve selection is to reverse the
translation to obtain NL text from Lean code and use a similarity measure with
the original text to select the best completion. While preliminary experiments
show this is useful, presently it is too slow to be practical.

Better equality testing for theorem statements will also result in better
filtering. Unlike program synthesis, for theorem autoformalisation, there is
no obvious counterpart of unit tests. Better equality testing with the correct
Lean formal statement, however, can serve the role of unit tests.

Outputs generated by our framework can be a useful starting point for
formalisation, potentially saving considerable time and effort. Presently
about one or two out of up to 18 completions tend to be useful; recognizing
these automatically will reduce effort. We did not experiment with interactive
formalisation as evaluation becomes harder. It would be interesting to combine
our framework with automatic proof search or repair ideas: partial proofs,
being close to complete proofs, can serve as a good starting point for proof
search. This could result in an autoformalisation system that is closer to
being autonomous.

## References

  * 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 Hugo Larochelle, Marc’Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (eds.), _Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual_ , 2020.  URL https://proceedings.neurips.cc/paper/2020/hash/1457c0d6bfcb4967418bfb8ac142f64a-Abstract.html.
  * Buzzard (2022) Kevin Buzzard.  What is the point of computers? a question for pure mathematicians.  In _International Congress of Mathematicians_ , 2022.  URL https://arxiv.org/pdf/2112.11598.pdf.
  * Campos et al. (2018) Ricardo Campos, Vítor Mangaravite, Arian Pasquali, Alípio Mário Jorge, Célia Nunes, and Adam Jatowt.  A text feature based automatic keyword extraction method for single documents.  In _European conference on information retrieval_ , pp. 684–691. Springer, 2018.
  * 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.
  * de Moura & Ullrich (2021) Leonardo de Moura and Sebastian Ullrich.  The lean 4 theorem prover and programming language.  In André Platzer and Geoff Sutcliffe (eds.), _Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings_ , volume 12699 of _Lecture Notes in Computer Science_ , pp. 625–635. Springer, 2021.  doi: 10.1007/978-3-030-79876-5“˙37.  URL https://doi.org/10.1007/978-3-030-79876-5_37.
  * 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.
  * Devlin et al. (2018) Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova.  Bert: Pre-training of deep bidirectional transformers for language understanding, 2018.  URL https://arxiv.org/abs/1810.04805.
  * Fried et al. (2022) Daniel Fried, Armen Aghajanyan, Jessy Lin, Sida Wang, Eric Wallace, Freda Shi, Ruiqi Zhong, Wen-tau Yih, Luke Zettlemoyer, and Mike Lewis.  Incoder: A generative model for code infilling and synthesis, 2022.  URL https://arxiv.org/abs/2204.05999.
  * Ganesalingam (2013) Mohan Ganesalingam.  _The Language of Mathematics - A Linguistic and Philosophical Investigation_ , volume 7805 of _Lecture Notes in Computer Science_.  Springer, 2013.  ISBN 978-3-642-37011-3.  doi: 10.1007/978-3-642-37012-0.  URL https://doi.org/10.1007/978-3-642-37012-0.
  * Hahn et al. (2022) Christopher Hahn, Frederik Schmitt, Julia J Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner.  Formal specifications from natural language.  _arXiv preprint arXiv:2206.01962_ , 2022.
  * Jain et al. (2022) Naman Jain, Skanda Vaidyanath, Arun Iyer, Nagarajan Natarajan, Suresh Parthasarathy, Sriram Rajamani, and Rahul Sharma.  Jigsaw: Large language models meet program synthesis.  In _Proceedings of the 44th International Conference on Software Engineering_ , ICSE ’22, pp. 1219–1231, New York, NY, USA, 2022. Association for Computing Machinery.  ISBN 9781450392211.  doi: 10.1145/3510003.3510203.  URL https://doi.org/10.1145/3510003.3510203.
  * Kamath & Das (2019) Aishwarya Kamath and Rajarshi Das.  A survey on semantic parsing.  In _1st Conference on Automated Knowledge Base Construction, AKBC 2019, Amherst, MA, USA, May 20-22, 2019_ , 2019.  doi: 10.24432/C5WC7D.  URL https://doi.org/10.24432/C5WC7D.
  * Lample et al. (2022) Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix.  Hypertree proof search for neural theorem proving.  _CoRR_ , abs/2205.11491, 2022.  doi: 10.48550/arXiv.2205.11491.  URL https://doi.org/10.48550/arXiv.2205.11491.
  * Lewkowycz et al. (2022) Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra.  Solving quantitative reasoning problems with language models.  _NeurIPS 2022_ , abs/2206.14858, 2022.  doi: 10.48550/arXiv.2206.14858.  URL https://doi.org/10.48550/arXiv.2206.14858.
  * Li et al. (2022) Yujia Li, David H. 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.  _CoRR_ , abs/2203.07814, 2022.  doi: 10.48550/arXiv.2203.07814.  URL https://doi.org/10.48550/arXiv.2203.07814.
  * Liu et al. (2021) Pengfei Liu, Weizhe Yuan, Jinlan Fu, Zhengbao Jiang, Hiroaki Hayashi, and Graham Neubig.  Pre-train, prompt, and predict: A systematic survey of prompting methods in natural language processing, 2021.  URL https://arxiv.org/abs/2107.13586.
  * Massot (2021) Patrick Massot.  Why formalize mathematics.  2021\.  URL https://www.imo.universite-paris-saclay.fr/~pmassot/files/exposition/why_formalize.pdf.
  * Reimers & Gurevych (2019) Nils Reimers and Iryna Gurevych.  Sentence-bert: Sentence embeddings using siamese bert-networks.  In _Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing_. Association for Computational Linguistics, 11 2019\.  URL http://arxiv.org/abs/1908.10084.
  * 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.
  * 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\.
  * Wang et al. (2022) Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou.  Self-consistency improves chain of thought reasoning in language models, 2022.  URL https://arxiv.org/abs/2203.11171.
  * Wei et al. (2022) Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed H. Chi, Quoc Le, and Denny Zhou.  Chain of thought prompting elicits reasoning in large language models.  _NeurIPS 2022_ , abs/2201.11903, 2022.  URL https://arxiv.org/abs/2201.11903.
  * Welleck et al. (2022) Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi.  Naturalprover: Grounded mathematical proof generation with language models.  _NeurIPS 2022_ , abs/2205.12910, 2022.  doi: 10.48550/arXiv.2205.12910.  URL https://doi.org/10.48550/arXiv.2205.12910.
  * Wu et al. (2022) Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy.  Autoformalization with large language models.  _NeurIPS 2022_ , abs/2205.12615, 2022.  doi: 10.48550/arXiv.2205.12615.  URL https://doi.org/10.48550/arXiv.2205.12615.
  * Zheng et al. (2022) Kunhao Zheng, Jesse Michael Han, and Stanislas Polu.  minif2f: a cross-system benchmark for formal olympiad-level mathematics.  In _The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022_. OpenReview.net, 2022.  URL https://openreview.net/forum?id=9ZPegFuFTFv.

##  Appendix A The Lean prover and reasoning styles

We use the Lean interactive theorem prover. The Lean mathematical library
(mathlib) includes most of the standard undergraduate curriculum. Many
advanced results have also been formalised building on mathlib. mathlib is
monolithic by design, ensuring that formalisations of different parts of
mathematics can be combined easily. The presence of this library to use and
also the resulting standardization of terminology makes Lean an attractive
target for autoformalisation.

The latest version of Lean, Lean 4, is a full-fledged programming language
with a fast runtime in addition to being an interactive theorem prover. This
allows a seamless integration of proofs, programs and meta-programs. We use
Lean 3 for one set of experiments and Lean 4 for the other because, at the
time of writing, mathlib was only partially available in Lean 4 (via a partial
binary port). Hence we use Lean 4 where its additional capabilities are
important and Lean 3 where these are not used and the larger library is of
greater value.

Mathematical proofs in the literature usually use _forward reasoning_ , where
a series of conclusions are deduced starting with the hypotheses from previous
conclusions and known results. A notable exception is proof by induction,
where we begin with the goal and reduce to sub-goals for the base case and the
induction step. Reasoning starting with goals is called _backward reasoning_.

In Lean (and similar systems), proofs can use both forward and backward
reasoning. However, backward reasoning allows for much more powerful
automation within the _tactic mode_ , at the cost of readability. Lean has
powerful tactics like rw (applies an equation or if and only if statement) and
apply(tries to match the goal against the conclusion of the lemma being used)
to deal with these.

We illustrate the different styles of reasoning by proving in Lean in various
ways the result $3<7$ using only the results $\forall n\in\mathbb{N},0<n+1$
and $\forall n,m\in\mathbb{N},n\leq m\implies n+1\leq m+1$. In Lean these are
the theorems Nat.zero_lt_succ and Nat.succ_lt_succ. Four proofs (in Lean 4,
which also work in Lean 3) are shown in Figure 4.

⬇

theorem three_lt_seven₁ : 3 < 7 :=

have l₁ : 0 < 4 := Nat.zero_lt_succ 3

have l₂ : 1 < 5 := Nat.succ_lt_succ l₁

have l₃ : 2 < 6 := Nat.succ_lt_succ l₂

Nat.succ_lt_succ l₃

⬇

theorem three_lt_seven₂ : 3 < 7 :=

Nat.succ_lt_succ (

Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.zero_lt_succ 3)))

theorem three_lt_seven₃ : 3 < 7 :=

by repeat (apply Nat.succ_lt_succ)

apply Nat.zero_lt_succ

theorem three_lt_seven₄ : 3 < 7 := by decide

Figure 4: Four proofs of $3<7$ in Lean

The first proof is a typical forward reasoning proof making deductions from
known results and previous deductions. The second proof is simply this in a
more concise form. The third and fourth proof use backward reasoning in tactic
mode. Tactics are powerful algorithms for finding proofs. It is evident that
the above backward proofs are more concise and will be easier for a user to
produce. However, in practice a complex mathematical proof in Lean will have
_mixed_ forward and backward reasoning, with forward reasoning taking the form
of a sequence of lemmas (in the form of have statements) leading to the main
theorem and backward reasoning used in the proof of each lemma.

##  Appendix B Theorem Statement Translation : Further Details

We sketch more details of the various steps in translating sentences.

###  B.1 Full Example prompt

The full prompt for Figure 1 is in Figure 5. As mentioned earlier, no
completion elaborated when we used fixed prompts.

Input text: “If a vector space has dimension ‘2‘ then it is finite
dimensional.” Prompt: ⬇ /– If a vector space has a finite basis, then it is
finite-dimensional. -/  theorem {K : Type u} {V : Type v} [division_ring K]
[add_comm_group V] [module K V] {ι : Type w} [fintype ι] (h : basis ι K V) :
finite_dimensional K V :=  /– A finite dimensional space is nontrivial if it
has positive ‘finrank‘. -/  theorem {K : Type u} {V : Type v} [division_ring
K] [add_comm_group V] [module K V] (h : 0 < finite_dimensional.finrank K V) :
nontrivial V :=  /– A finite dimensional space that is a subsingleton has zero
‘finrank‘. -/  theorem {K : Type u} {V : Type v} [division_ring K]
[add_comm_group V] [module K V] [h : subsingleton V] :
finite_dimensional.finrank K V = 0 :=  /– A vector space has dimension at most
‘1‘ if and only if there is a single vector of which all vectors are
multiples. -/  theorem {K : Type u} {V : Type v} [division_ring K]
[add_comm_group V] [module K V] : module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V),
∃ (r : K), r • v₀ = v :=  /– If a vector space has dimension ‘2‘ then it is
finite dimensional. -/  theorem Codex Completion: ⬇ {K : Type u} {V : Type v}
[division_ring K] [add_comm_group V] [module K V] (h : module.rank K V = 2) :
finite_dimensional K V Post-processed code in Lean 4: ⬇ theorem ∀ {K : Type u}
{V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 :
Module K V],  Module.rank K V = 2 → FiniteDimensional K V Figure 5: Complete
prompt used in Figure 1.

###  B.2 Parsing, translation and auto-correction

Given a Codex completion, we first (attempted to) parse this and extracted
_identifiers_ from the syntax. These were _translated_ and _auto-corrected_
before re-parsing. The translation step is necessary as the prompt data we had
available was in Lean 3, as is most of the data in GitHub on which Codex is
trained. Thus the completions usually use Lean 3/mathlib terminology. Using a
prebuilt dictionary, we translated the Lean 3/mathlib identifiers to those
used by the binary port (binport) of mathlib, with auto-correction attempted
for those that did not have valid translations. Both the dictionary and auto-
correction are based on transformations of two forms: case transformations
(for example camel-case versus snake-case) and dropping or adding segments of
the form is or has.

###  B.3 Selection

If more than one completion was correctly elaborated (which is typical when at
least one completion is elaborated), we selected the best completion by
_voting_. Namely, we first group elaborated completions together into groups
whose members can be proved to be equal using a certain tactic. The tactic we
used is one that slightly extends _reflexivity_ (i.e., _definitional
equality_). The chosen answer was the first member of the largest group. In
practice, as the present tactic for proving equality is weak, in most cases
this simply picked the first completion of Codex that was valid (i.e., that
elaborated).

###  B.4 Sentence similarity

We used Sentence-Similarity library (Reimers & Gurevych, 2019) for calculating
the sentence embeddings of the doc-strings. We used all-mpnet-base-v2 model, a
pretrained transformer model finetuned over 1 Billion sentence pairs from
multiple datasets. This model provided the best quality embeddings among the
hosted models on the library at the time of writing this paper. We computed
the cosine similarity of the sentence-embeddings generated from the input
docstring with the collection of mathlib docstrings and selected Top-K similar
docstrings based on the similarity scores and their corresponding Lean
statements for the example prompts.

###  B.5 Keyword-based prompting

The purpose of input-dependent prompting for theorem statements is to retrieve
a collection of examples that contain all the relevant details to formalise a
given statement, and this is achieved to a large extent using sentence
similarity. However, in optimising for overall similarity, this approach may
leave out smaller details that are nevertheless crucial for formalising the
statement correctly. To address this, we introduce a method of prompting based
on keywords that complements sentence-similarity based retrieval. We used the
YAKE keyword extraction tool (Campos et al., 2018) to extract the keywords
from mathlib and store them in a convenient format. When preparing the prompt
for formalising a sentence, we extract the keywords and retrieve a few
examples for each keyword, in addition to using sentence similarity.

###  B.6 More complex prompts

While our translations were often successful with the docstring-style prompts
we considered, the performance was poor with prompts that contained:

  * •

Complex formulas in LaTeX.

  * •

Certain idioms such as “… the intersection of every $d+1$ of these sets …”

It appears that a major reason for this was the lack of good examples in our
database. Indeed, in the case of proof translation, our prompts did have
complex LaTeX formulas and Codex successfully generated translated input text
with (similar) complex LaTeX formulas.

##  Appendix C Proof Translation Results and Analysis

###  C.1 Evaluation dataset

The following is the full list of theorems.

  1. 1.

_Absolute Value Function is Convex_ (abs_convex): Let
$f:\mathbb{R}\to\mathbb{R}$ be the absolute value function on the real
numbers. Then $f$ is convex.

  2. 2.

_Symmetric Real Matrices have Real Eigenvalues_
(symm_real_mat_real_eigenvalue): Every real symmetric matrix has real
eigenvalues.

  3. 3.

_Schur’s Lemma_ (schur_lemma): Let $V$ and $W$ be vector spaces; and let
$\rho_{V}$ and $\rho_{W}$ be irreducible representations of $G$ on $V$ and $W$
respectively. If $V$ and $W$ are not isomorphic, then there are no nontrivial
representations of $G$ on $V$ and $W$ respectively.

  4. 4.

_$\mathbb{R}^{n}$ is paracompact_ (rn_paracompact): $\mathbb{R}^{n}$ is
paracompact for all $n$.

  5. 5.

_Schur’s Inequality_ (schur_ineq): Let $x,y,z\in\mathbb{R}_{\geq 0}$ be
positive real numbers such that $x\geq y\geq z\geq 0$. Let
$t\in\mathbb{R},t>0$ be a (strictly) positive real number. Then:
$x^{t}(x-y)(x-z)+y^{t}(y-z)(y-x)+z^{t}(z-x)(z-y)\geq 0$.

  6. 6.

_Overflow theorem_ (overflow): Let $F$ be a set of first-order formulas which
has finite models of arbitrarily large size. Then $F$ has an infinite model.

  7. 7.

_Density of Irrational Orbit_ (density_irr_orbit): The fractional parts of the
integer multiples of an irrational number form a dense subset of the unit
interval.

  8. 8.

_Contraction Mapping theorem_ (contraction_mapping): Let $B$ be a Banach
space, $M$ a closed subset of $B$, and $\Phi$ a mapping from $M$ to $M$ such
that for some $k\in[0,1)$,

$\|\Phi(x)-\Phi(y)\|\leq k\|x-y\|$

for any two points $x$ and $y$ in $M$. Then there is a unique point $z$ in $M$
such that $\Phi(z)=z$.

  9. 9.

_Class number of a PID_ (class_num_pid): The class number of a number field
$K$ is 1 if and only if the ring of integers is a PID.

  10. 10.

_Bipartite Graph is two colorable_ (bipartite_iff_two_colorable): Let $G$ be a
graph. Then $G$ is 2-colorable if and only if $G$ is bipartite.

  11. 11.

_$p$ -adic Units_ (padic_units): Given a prime number $p$ and a natural number
$x$, if $x$ is coprime to $p$, then $x$ is a unit in the $p$-adic integers.

  12. 12.

_Nesbitt’s Inequality_ (nesbitt_ineq): Let $a$, $b$ and $c$ be positive real
numbers.Then: $\dfrac{a}{b+c}+\dfrac{b}{a+c}+\dfrac{c}{a+b}\geq\dfrac{3}{2}$

  13. 13.

_Bernoull’s Polynomial Evaluation_ (bernoulli_polynomial_eval): Given a
natural number $n$ and a rational $x$, let $B_{n}(x)$ denote the $n$-th
Bernoulli polynomial evaluated at $x$. Then,

$B_{n}(1+x)=B_{n}(x)+nx^{n-1}$

These theorems involve different types of proving techniques such as proof by
contradiction, induction, algebraic manipulations etc. They belong to
different domains such as topology, algebraic number theory, analysis, group
theory, linear algebra, representation theory and graph theory. They are also
of varying difficulty levels. For the first 11 theorems, we asked Codex for
both Lean theorem statements and proofs. For the remaining 2, we included the
correct Lean theorem statement in the example prompt and asked Codex for the
Lean proof format.

###  C.2 results

This section summarises our main findings in the proof autoformalisation
experiments.

Figure 6: Max scores of the 11 theorems, for the other 2 theorems we included
correct Lean statements in the prompt

The results of evaluation of proof translation are summarised in Figure 6. Out
of the $288$ completions, $22$ (i.e., about one in thirteen) were scored as
$3$.

####  C.2.1 Capabilities shown by Codex

The output proof formats were well structured and Codex was able to break the
full proof into its main steps. For example, in bernoulli_polynomial_eval, the
natural language proof had two major proof statements in a single sentence and
Codex broke it down into the two relevant pieces. Also, for schur_ineq, we
observed that the natural language proof had statements that simply mentioned
that all the terms are non-negative and concluded the proof. Interestingly,
Codex completions had these details formalised as intermediate steps.

While formalising statements, Codex sometimes expanded a definition instead of
using the mathlib definition directly. Interestingly, in a completion for
abs_convex, Codex directly outputted the precise simplified statement that
needed to be proved, possibly taking cues from the natural language proof
provided – it didn’t use the convex_on definition from mathlib and directly
outputted ∀ (x y : ℝ), ∀ (α β : ℝ), α ≥ 0 ∧ β ≥ 0 ∧ α + β = 1 → abs (α * x + β
* y) ≤ (α * abs x + β * abs y) as the theorem statement to be proved. Also,
while formalising the symm_real_mat_real_eigenvalue lemma, some completions
had the hypothesis that $A=A^{T}$ instead of is_symm A. Maybe input-dependent
prompting for proofs could direct Codex to output relevant mathlib definitions
more frequently instead of using their expanded forms.

Codex also utilized contextual mathematical knowledge that was missing in the
theorem statements but present in natural language proofs. For example, while
formalising the proof of symm_real_mat_real_eigenvalue, the statement of the
natural language prompt simply said that every real symmetric matrix has real
eigenvalues. One Codex completion started with a complex eigenvalue, possibly
getting the context right from the natural language proof.

We also observed that Codex generated plausible theorem names, which were in
line with mathlib style.

####  C.2.2 Errors

There were very few instances where the outputs did not follow valid Lean
syntax. For instance, In schur_ineq, Codex completion contained incorrect Lean
expression x ≥ y ≥ z ≥ 0 (copying directly from the natural proof) instead of
the correct Lean expression x ≥ y ∧ y ≥ z ∧ z ≥ 0. There was one instance
where Codex generated a proof format in a different language.

In some cases, we observed that the completion used an undeclared variable in
the proof. For example, it declared t > 0 without introducing t: ℝ.

There were a few instances where proof-steps were mathematically incorrect.
For instance, in abs_convex, Codex didn’t assume $\alpha$ and $\beta$ as
positive numbers, however it used this condition in the proof. It also wrongly
stated the triangle inequality as equality: |α*x + β*y| = α*|x| + β*|y|.

There were also instances where natural language translations were wrong,
although they were mathematically valid statements and valid Lean code. For
example, in schur_lemma, Codex confuses a homomorphism being “nonzero” with a
homomorphism being “nowhere” zero . Also, in some completions, the definition
of “dense” in the density_irr_orbit was used incorrectly. In a proof of the
contraction_mapping, Codex defines a function x to be x(i) := φ (x (i)). This
is wrong since it is using x(i) to define x(i). The correct definition is
inductive : x(0) := x and x(i) := φ (x (i - 1)) for i ≥ 1, and might have been
difficult for Codex to deduce since induction was not explicitly mentioned. In
a few instances, it also mistook absolute value for norm.

There were also cases when Codex got stuck at a particular step and looped
until it completed the 2000 tokens. These repetitions occured in different
forms – frequently applying the same lemma or writing a set of have
statements. At times, the proof was looped in an inductive fashion. For
example, in the contraction_mapping, Codex defined φ (x n) = x n - 1 followed
by have h1 : φ (x 1) = x 0, have h1 : φ (x 2) = x 1, and so on.

Sometimes Codex outputted contradicting proof steps (we report cases not
involving proof of contradiction). As an example, in the generated proof of
schur_lemma, there were two statements, one stating that the kernel is
trivial, and the next one stating the opposite.

inline]add examples for unrelated comments and lean statements inline]give
mathlib style names

####  C.2.3 Other Observations

Hallucinations. We say that Codex hallucinates if the definition/theorem name
generated is not present in mathlib even though the correct definition/theorem
is present in the mathlib. We have observed that hallucination is common. For
example, in few instances while formalising abs_convex,Codex outputs
convex_function instead of convex_on and similar made up definitions/theorem
names that looked realistic but are not present in mathlib.

Deviation from Natural Language Proof. There were very few instances where the
output proof formats deviated from the natural language proofs. When we
included the correct formalised statement to Codex for the rn_paracompact,
Codex merged different proofs from distinct sources, leading to conflicting
notation. Also, Codex formalised the contra-positive version of theorem
statement of schur_lemma given in the natural language proof.

##  Appendix D Complete data and analysis for proof translations

###  D.1 Few-Shot Prompts for different proof formats

In this section, we show the example fixed few-shot prompts for the different
proof formats that we provided to Codex. We designed these prompts using three
theorems – _Power set is closed under intersection_ , _Square of sum_ , _and
Identity of Group is Unique_. For each of these theorems, we used the NL
theorem statements and proofs in raw formats and combined them with the
corresponding Lean proof format. These Lean proof formats have interleaved NL
comments picked from the NL proof. We concatenated the NL theorem statement
and proof that has to be formalised with these example prompts and provided
them to Codex for output.

####  D.1.1 Proof Outline

Following are the example few-shot prompts for the proof outline format.

⬇

/–‘theorem‘

Power Set is Closed under Intersection

Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:

:$\forall A, B \in \powerset S: A \cap B \in \powerset S$

‘proof‘

Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.

{{qed}}

-/

theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈
$\mathcal{P}$ S, (A ∩ B) ∈ $\mathcal{P}$ S :=

begin

– $A$ and $B$ are sets. $A$ and $B$ belong to power set of $S$

assume (A : set α) (hA : A ∈ $\mathcal{P}$ S) (B : set α) (hB : B ∈
$\mathcal{P}$ S),

– Then $A ⊆ S$ and $B ⊆ S$, by power set definition

have h1 : (A ⊆ S) ∧ (B ⊆ S), from sorry,

– Then $(A ∩ B) ⊆ A$, by intersection of set is a subset

have h2 : (A ∩ B) ⊆ A, from sorry,

– Then $(A ∩ B) ⊆ S$, by subset relation is transitive

have h3 : (A ∩ B) ⊆ S, from sorry,

– Hence $(A ∩ B) ∈ $\mathcal{P}$ S$, by power set definition

show (A ∩ B) ∈ $\mathcal{P}$ S, from sorry,

end

/–‘theorem‘

Square of Sum

:$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$

‘proof‘

Follows from the distribution of multiplication over addition:

{{begin-eqn}}

{{eqn | l = \left({x + y}\right)^2

| r = \left({x + y}\right) \cdot \left({x + y}\right)

}}

{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)

| c = Real Multiplication Distributes over Addition

}}

{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y

| c = Real Multiplication Distributes over Addition

}}

{{eqn | r = x^2 + 2xy + y^2

| c =

}}

{{end-eqn}}

{{qed}}

-/

theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2)

begin

– expand the power

calc (x + y)^2 = (x+y)*(x+y) : by sorry

– distributive property of multiplication over addition gives:

… = x*(x+y) + y*(x+y) : by sorry

– applying the above property further gives:

… = x*x + x*y + y*x + y*y : by sorry

– rearranging the terms using commutativity and adding gives:

… = x^2 + 2*x*y + y^2 : by sorry,

end

/–‘theorem‘

Identity of Group is Unique

Let $\struct {G, \circ}$ be a group. Then there is a unique identity element
$e \in G$.

‘proof‘

From Group has Latin Square Property, there exists a unique $x \in G$ such
that:

:$a x = b$

and there exists a unique $y \in G$ such that:

:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:

:$a x = a$

and there exists a unique $y \in G$ such that:

:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.

{{qed}}

-/

theorem group_identity_unique {G : Type*} [group G] : ∃e : G, ∀ a : G, e * a =
a ∧ a * e = a := begin – Group has Latin Square Property have h1 : ∀ a b : G,
∃ x : G, a * x = b, from sorry,

have h2 : ∀ a b : G, ∃y : G, y * a = b, from sorry, – Setting $b=a$, this
becomes: have h3 : ∀ a : G, ∃ x : G, a * x = a, from sorry,

have h4 : ∀ a : G, ∃y : G, y * a = a, from sorry, – These $x$ and $y$ are both
$(1:G)$, by definition of identity element have h5 : ∀ a : G, classical.some
(h3 a) = (1 : G), from sorry, have h6 : ∀ a : G, classical.some (h4 a) = (1 :
G), from sorry, show ∃ e : G, ∀ a : G, e * a = a ∧ a * e = a, from by {

use (1 : G),

have h7 : ∀ e : G, (∀ a : G, e * a = a ∧ a * e = a) → e = 1, from by {

assume (e : G) (h7 : ∀ a : G, e * a = a ∧ a * e = a),

have h8 : ∀ a : G, e = classical.some (h3 a), from sorry,

have h9 : ∀ a : G, e = classical.some (h4 a), from sorry,

show e = (1 : G), from sorry,

},

sorry,

}

end

####  D.1.2 Proof with premises

Following are the example few-shot prompts for the proof outline with premises
format.

⬇

/–‘theorem‘

Power Set is Closed under Intersection

Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:

:$\forall A, B \in \powerset S: A \cap B \in \powerset S$

‘proof‘

Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.

{{qed}}

-/

theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈
$\mathcal{P}$ S, (A ∩ B) ∈ $\mathcal{P}$ S :=

begin

– $A$ and $B$ are sets. $A$ and $B$ belong to power set of $S$

assume (A : set α) (hA : A ∈ $\mathcal{P}$ S) (B : set α) (hB : B ∈
$\mathcal{P}$ S),

– Then $A ⊆ S$ and $B ⊆ S$, by power set definition

have h1 : (A ⊆ S) ∧ (B ⊆ S), from by auto [set.subset_of_mem_powerset,
set.subset_of_mem_powerset],

– Then $(A ∩ B) ⊆ A$, by intersection of set is a subset

have h2 : (A ∩ B) ⊆ A, from by auto [set.inter_subset_left],

– Then $(A ∩ B) ⊆ S$, by subset relation is transitive

have h3 : (A ∩ B) ⊆ S, from by auto [set.subset.trans],

– Hence $(A ∩ B) ∈ $\mathcal{P}$ S$, by power set definition

show (A ∩ B) ∈ $\mathcal{P}$ S, from by auto [set.mem_powerset],

end

/–‘theorem‘

Square of Sum

:$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$

‘proof‘

Follows from the distribution of multiplication over addition:

{{begin-eqn}}

{{eqn | l = \left({x + y}\right)^2

| r = \left({x + y}\right) \cdot \left({x + y}\right)

}}

{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)

| c = Real Multiplication Distributes over Addition

}}

{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y

| c = Real Multiplication Distributes over Addition

}}

{{eqn | r = x^2 + 2xy + y^2

| c =

}}

{{end-eqn}}

{{qed}}

-/

theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2)

begin

– expand the power

calc (x + y)^2 = (x+y)*(x+y) : by auto [sq]

– distributive property of multiplication over addition gives:

… = x*(x+y) + y*(x+y) : by auto [add_mul]

– applying the above property further gives:

… = x*x + x*y + y*x + y*y : by auto [mul_comm, add_mul] using [ring]

– rearranging the terms using commutativity and adding gives:

… = x^2 + 2*x*y + y^2 : by auto [sq, mul_comm] using [ring]

end

/–‘theorem‘

Identity of Group is Unique

Let $\struct {G, \circ}$ be a group. Then there is a unique identity element
$e \in G$.

‘proof‘

From Group has Latin Square Property, there exists a unique $x \in G$ such
that:

:$a x = b$

and there exists a unique $y \in G$ such that:

:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:

:$a x = a$

and there exists a unique $y \in G$ such that:

:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.

{{qed}}

-/

theorem group_identity_unique {G : Type*} [group G] : ∃e : G, ∀ a : G, e * a =
a ∧ a * e = a := begin – Group has Latin Square Property have h1 : ∀ a b : G,
∃ x : G, a * x = b, from by auto using [use (a⁻¹ * b)],

have h2 : ∀ a b : G, ∃y : G, y * a = b, from by auto using [use b * a⁻¹], –
Setting $b=a$, this becomes: have h3 : ∀ a : G, ∃ x : G, a * x = a, from by
auto [h1],

have h4 : ∀ a : G, ∃y : G, y * a = a, from by auto [h2], – These $x$ and $y$
are both $(1:G)$, by definition of identity element have h5 : ∀ a : G,
classical.some (h3 a).exists = (1 : G), from by auto [exists_unique.unique,
h3, classical.some_spec, exists_unique.exists, mul_one], have h6 : ∀ a : G,
classical.some (h4 a).exists = (1 : G), from by auto [exists_unique.unique,
h4, classical.some_spec, exists_unique.exists, one_mul], show ∃ e : G, ∀ a :
G, e * a = a ∧ a * e = a, from by auto [h3, h4, exists_unique.unique,
classical.some_spec, exists_unique.exists] using [use (1 : G)],

end

####  D.1.3 Full proofs

Following are the example few-shot prompts for the full proof format.

⬇

/–‘theorem‘

Power Set is Closed under Intersection

Let $S$ be a set.

Let $\powerset S$ be the power set of $S$.

Then:

:$\forall A, B \in \powerset S: A \cap B \in \powerset S$

‘proof‘

Let $A, B \in \powerset S$.

Then by the definition of power set, $A \subseteq S$ and $B \subseteq S$.

From Intersection is Subset we have that $A \cap B \subseteq A$.

It follows from Subset Relation is Transitive that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and closure is proved.

{{qed}}

-/

theorem power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈
$\mathcal{P}$ S, (A ∩ B) ∈ $\mathcal{P}$ S :=

begin

– $A$ and $B$ are sets. $A$ and $B$ belong to power set of $S$

assume (A : set α) (hA : A ∈ $\mathcal{P}$ S) (B : set α) (hB : B ∈
$\mathcal{P}$ S),

– Then $A ⊆ S$ and $B ⊆ S$, by power set definition

have h1 : (A ⊆ S) ∧ (B ⊆ S), from by {split,apply
set.subset_of_mem_powerset,exact hA,apply set.subset_of_mem_powerset,exact
hB},

– Then $(A ∩ B) ⊆ A$, by intersection of set is a subset

have h2 : (A ∩ B) ⊆ A, from by apply set.inter_subset_left,

– Then $(A ∩ B) ⊆ S$, by subset relation is transitive

have h3 : (A ∩ B) ⊆ S, from by {apply set.subset.trans h2 h1.left},

– Hence $(A ∩ B) ∈ $\mathcal{P}$ S$, by power set definition

show (A ∩ B) ∈ $\mathcal{P}$ S, from by {apply set.mem_powerset h3},

end

/–‘theorem‘

Square of Sum

:$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$

‘proof‘

Follows from the distribution of multiplication over addition:

{{begin-eqn}}

{{eqn | l = \left({x + y}\right)^2

| r = \left({x + y}\right) \cdot \left({x + y}\right)

}}

{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)

| c = Real Multiplication Distributes over Addition

}}

{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y

| c = Real Multiplication Distributes over Addition

}}

{{eqn | r = x^2 + 2xy + y^2

| c =

}}

{{end-eqn}}

{{qed}}

-/

theorem square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2)

begin

– expand the power

calc (x + y)^2 = (x+y)*(x+y) : by rw sq

– distributive property of multiplication over addition gives:

… = x*(x+y) + y*(x+y) : by rw add_mul

– applying the above property further gives:

… = x*x + x*y + y*x + y*y : by {rw [mul_comm x (x+y),mul_comm y (x+y)], rw
[add_mul,add_mul], ring}

– rearranging the terms using commutativity and adding gives:

… = x^2 + 2*x*y + y^2 : by {repeat {rw ← sq}, rw mul_comm y x, ring}

end

/–‘theorem‘

Identity of Group is Unique

Let $\struct {G, \circ}$ be a group. Then there is a unique identity element
$e \in G$.

‘proof‘

From Group has Latin Square Property, there exists a unique $x \in G$ such
that:

:$a x = b$

and there exists a unique $y \in G$ such that:

:$y a = b$

Setting $b = a$, this becomes:

There exists a unique $x \in G$ such that:

:$a x = a$

and there exists a unique $y \in G$ such that:

:$y a = a$

These $x$ and $y$ are both $e$, by definition of identity element.

{{qed}}

-/

theorem group_identity_unique {G : Type*} [group G] : ∃e : G, ∀ a : G, e * a =
a ∧ a * e = a := begin – Group has Latin Square Property have h1 : ∀ a b : G,
∃ x : G, a * x = b, from by {

assume a b : G, use a⁻¹ * b, obviously, },

have h2 : ∀ a b : G, ∃y : G, y * a = b, from by assume a b : G, use b * a⁻¹,
obviously, , – Setting $b=a$, this becomes: have h3 : ∀ a : G, ∃ x : G, a * x
= a, from

assume a : G, h1 a a,

have h4 : ∀ a : G, ∃y : G, y * a = a, from assume a : G, h2 a a, – These $x$
and $y$ are both $(1:G)$, by definition of identity element have h5 : ∀ a : G,
classical.some (h3 a).exists = (1 : G), from assume a :G, exists_unique.unique
(h3 a) (classical.some_spec (exists_unique.exists (h3 a))) (mul_one a), have
h6 : ∀ a : G, classical.some (h4 a).exists = (1 : G), from assume a : G,
exists_unique.unique (h4 a) (classical.some_spec (exists_unique.exists (h4
a))) (one_mul a), show ∃ e : G, ∀ a : G, e * a = a ∧ a * e = a, from by {

use (1 : G),

have h7 : ∀ e : G, (∀ a : G, e * a = a ∧ a * e = a) → e = 1, from by {

assume (e : G) (hident : ∀ a : G, e * a = a ∧ a * e = a),

have h8 : ∀ a : G, e = classical.some (h3 a).exists, from assume (a : G),

exists_unique.unique (h3 a) (hident a).right

(classical.some_spec (exists_unique.exists (h3 a))),

have h9 : ∀ a : G, e = classical.some (h4 a).exists, from assume (a : G),

exists_unique.unique (h4 a) (hident a).left

(classical.some_spec (exists_unique.exists (h4 a))),

show e = (1 : G), from eq.trans (h9 e) (h6 _),

},

exact ⟨by obviously, h7⟩,

}

end

###  D.2 Evaluation Scores

The following tables represent the scores given to the proof format outputs
produced by Codex. The tables on the right represent the scores given to the
output statement (max score = 2). The tables on the left represent the scores
given to the output proof format (max score = 4) (ref. Tables 3 – 13). In the
tables, Full corresponds to _full proof_ , Outline corresponds to _proof
outline_ , and Premises corresponds to _proof outline with premises_. O1, O2
and O3 are the three outputs sampled at each temperature.

We also include tables to show evaluation of the outputs when we included
correct Lean theorem statement in the prompt (ref. Tables 14 – 18).

There are 18 scores in total, 6 for each proof format, out of which there are
3 each for temperatures 0.4 and 0.8 respectively.

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 3 | 2 | 1 | 1 | 1 | 1 | 3
Outline | 2 | 3 | 2 | 3 | 3 | 3 | 3
Premises | 2 | 1 | 1 | 2 | 2 | 1 | 2
Max | 3 | 3 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 2 | 1 | 1 | 1 | 0 | 1 | 2
Outline | 1 | 1 | 0 | 1 | 1 | 0 | 1
Premises | 1 | 0 | 0 | 0 | 0 | 0 | 1
Max | 2 | 1 |

Table 3: abs_convex

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 3 | 3 | 2 | 2 | 1 | 2 | 3
Outline | 3 | 3 | 3 | 2 | 2 | 1 | 3
Premises | 2 | 2 | 2 | 3 | 2 | 1 | 3
Max | 3 | 3 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 2 | 2 | 1 | 1 | 1 | 2 | 2
Outline | 2 | 2 | 2 | 1 | 1 | 2 | 2
Premises | 2 | 2 | 2 | 2 | 1 | 2 | 2
Max | 2 | 2 |

Table 4:  schur_ineq

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 1 | 1 | 2 | 0 | 0 | 2
Outline | 1 | 2 | 3 | 1 | 0 | 1 | 3
Premises | 3 | 1 | 0 | 0 | 2 | 0 | 3
Max | 3 | 2 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 0 | 1 | 0 | 1 | 0 | 1
Outline | 0 | 1 | 1 | 0 | 0 | 1 | 1
Premises | 1 | 1 | 0 | 0 | 1 | 0 | 1
Max | 1 | 1 |

Table 5:  symm_real_mat_real_eigenvalue

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 1 | 0 | 1 | 1 | 0 | 1
Outline | 0 | 1 | 1 | 0 | 0 | 0 | 1
Premises | 1 | 1 | 0 | 0 | 1 | 1 | 1
Max | 1 | 1 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 1 | 0 | 1 | 1 | 0 | 1
Outline | 1 | 0 | 1 | 0 | 1 | 0 | 1
Premises | 1 | 1 | 1 | 1 | 0 | 0 | 1
Max | 1 | 1 |

Table 6:  density_irr_orbit

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 2 | 3 | 2 | 0 | 2 | 0 | 3
Outline | 0 | 3 | 2 | 0 | 0 | 3 | 3
Premises | 1 | 1 | 2 | 1 | 1 | 2 | 2
Max | 3 | 3 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 1 | 1 | 1 | 1 | 1 | 1 | 1
Outline | 1 | 1 | 1 | 1 | 1 | 1 | 1
Premises | 1 | 1 | 1 | 1 | 1 | 1 | 1
Max | 1 | 1 |

Table 7:  contraction_mapping

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 2 | 2 | 2 | 0 | 3 | 0 | 3
Outline | 0 | 0 | 0 | 2 | 2 | 0 | 2
Premises | 3 | 1 | 0 | 0 | 0 | 2 | 3
Max | 3 | 3 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 1 | 1 | 1 | 1 | 1 | 1 | 1
Outline | 1 | 2 | 2 | 2 | 1 | 0 | 2
Premises | 1 | 1 | 1 | 1 | 1 | 1 | 1
Max | 2 | 2 |

Table 8:  schur_lemma

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 2 | 0 | 3 | 0 | 1 | 3
Outline | 0 | 1 | 0 | 0 | 0 | 1 | 1
Premises | 0 | 1 | 1 | 2 | 1 | 2 | 2
Max | 2 | 3 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 2 | 2 | 1 | 1 | 1 | 0 | 2
Outline | 2 | 1 | 0 | 0 | 0 | 2 | 2
Premises | 2 | 0 | 1 | 0 | 0 | 0 | 2
Max | 2 | 2 |

Table 9:  overflow

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 0 | 1 | 0 | 1 | 0 | 1
Outline | 0 | 1 | 1 | 1 | 0 | 0 | 1
Premises | 1 | 0 | 1 | 2 | 0 | 1 | 2
Max | 1 | 2 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 0 | 0 | 0 | 1 | 0 | 1
Outline | 1 | 2 | 1 | 1 | 1 | 0 | 2
Premises | 1 | 1 | 1 | 1 | 0 | 1 | 1
Max | 2 | 1 |

Table 10:  class_num_pid

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 1 | 3 | 0 | 2 | 1 | 1 | 3
Outline | 1 | 1 | 1 | 2 | 0 | 1 | 2
Premises | 1 | 2 | 1 | 2 | 1 | 1 | 2
Max | 3 | 2 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 0 | 0 | 0 | 0 | 0 | 0
Outline | 0 | 0 | 0 | 0 | 0 | 0 | 0
Premises | 0 | 0 | 0 | 0 | 0 | 0 | 0
Max | 0 | 0 |

Table 11:  rn_paracompact

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 1 | 0 | 1 | 2 | 0 | 1 | 2
Outline | 1 | 0 | 1 | 2 | 0 | 0 | 2
Premises | 0 | 1 | 1 | 1 | 0 | 0 | 1
Max | 1 | 2 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 0 | 0 | 1 | 0 | 0 | 1
Outline | 0 | 0 | 0 | 1 | 0 | 0 | 1
Premises | 0 | 0 | 0 | 0 | 0 | 0 | 0
Max | 0 | 1 |

Table 12:  bipartite_iff_two_colorable

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 1 | 2 | 0 | 0 | 0 | 2
Outline | 1 | 1 | 1 | 1 | 1 | 0 | 1
Premises | 2 | 2 | 2 | 0 | 1 | 0 | 2
Max | 2 | 1 |

Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 1 | 2 | 1 | 1 | 0 | 2
Outline | 2 | 2 | 1 | 1 | 1 | 0 | 2
Premises | 1 | 1 | 1 | 0 | 1 | 1 | 1
Max | 2 | 1 |

Table 13: padic_units Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 1 | 1 | 1 | 0 | 1 | 1
Outline | 1 | 3 | 0 | 2 | 0 | 1 | 3
Premises | 1 | 0 | 1 | 0 | 0 | 1 | 1
Max | 3 | 2 |
Table 14:  nesbitt_ineq (Correct Lean theorem statement included in the prompt)  Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 1 | 1 | 0 | 1 | 0 | 2 | 2
Outline | 0 | 1 | 1 | 0 | 3 | 1 | 3
Premises | 1 | 1 | 1 | 2 | 1 | 1 | 2
Max | 1 | 3 |
Table 15:  bernoulli_polynomial_eval (Correct Lean theorem statement included in the prompt) Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 1 | 1 | 1 | 0 | 0 | 1 | 1
Outline | 0 | 1 | 2 | 1 | 1 | 0 | 2
Premises | 1 | 2 | 0 | 0 | 0 | 1 | 2
Max | 2 | 1 |
Table 16:  rn_paracompact (Correct Lean theorem statement included in the prompt) Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 0 | 1 | 1 | 1 | 1 | 1 | 1
Outline | 1 | 0 | 2 | 1 | 1 | 0 | 2
Premises | 0 | 2 | 0 | 1 | 2 | 2 | 2
Max | 2 | 2 |
Table 17: overflow (Correct Lean theorem statement included in the prompt) Format | T=0.4 | T=0.8 | Max
---|---|---|---
| O1 | O2 | O3 | O1 | O2 | O3 |
Full | 1 | 0 | 2 | 1 | 2 | 0 | 2
Outline | 1 | 2 | 0 | 1 | 0 | 2 | 2
Premises | 1 | 1 | 2 | 2 | 1 | 1 | 2
Max | 2 | 2 |
Table 18:  density_irr_orbit (Correct Lean theorem statement included in the
prompt)

###  D.3 Interesting Codex proof outputs

This section contains a few examples that demonstrate some of Codex’s
abilities like inventing realistic theorem names and performing algebraic
manipulations by analogy, as well as the influence of the example prompts on
the output.

####  D.3.1 Proof output whose foundational concepts are not defined in
mathlib

As an experiment, we prompted Codex with a theorem for which the concepts
required to state it were not in mathlib. Codex was forced to invent its own
names for theorems and concepts, and we observed that Codex hints plausible
and realistic names for concepts in synthetic Euclidean geometry that can be
included in mathlib.

_Theorem name_

Diagonals of Rhombus Bisect Each Other at Right Angles

_Theorem statement_

Let $ABCD$ be a rhombus. The diagonals $AC$ and $BD$ of $ABCD$ bisect each
other at right angles.

_Natural Language proof_

By the definition of a rhombus, $AB=AD=BC=DC$.

Without loss of generality, consider the diagonal $BD$.

Thus:

$\triangle ABD$ is an isosceles triangle whose apex is $A$ and whose base is
$BD$.

By Diagonals of Rhombus Bisect Angles, $AC$ bisects $\angle BAD$.

From Bisector of Apex of Isosceles Triangle also Bisects Base, $AC$ bisects
$BD$.

From Bisector of Apex of Isosceles Triangle is Perpendicular to Base, $AC$
bisects $BD$ at right angles.

Hence the result.

$Q.E.D.$

Codex outputs are shown in Figure 7 and Figure 8.

⬇ Output 1 :  theorem diagonals_of_rhombus_bisect_each_other_at_right_angles
(ABCD : rhombus) :  ∀ AC BD ∈ diagonals ABCD, AC.bisects BD ∧ BD.bisects AC ∧
AC.perpendicular BD :=  begin assume (AC : segment) (hAC : AC ∈ diagonals
ABCD) (BD : segment) (hBD : BD ∈ diagonals ABCD),  have : AB = AD ∧ AB = BC ∧
AB = DC, from sorry,  have : ∀ A B C, isosceles_triangle A B C, from sorry,
have : isosceles_triangle A B D, from sorry,  have : AC.bisects $\angle$ BAD,
from sorry,  have : AC.bisects BD, from sorry,  have : AC.perpendicular BD,
from sorry,  show AC.bisects BD ∧ BD.bisects AC ∧ AC.perpendicular BD, from
sorry,  end Figure 7: Codex generates ABCD as a type “rhombus” that is not
present in mathlib. It also generates definitions like “bisects” and
“perpendicular” that are also not formalised in mathlib and uses them
plausibly. Here Codex shows capabilities of composing proofs in line with type
theory. ⬇ Completion 2 :  theorem
diagonals_of_rhombus_bisect_each_other_at_right_angles {A B C D : point}
(h_rhombus : is_rhombus A B C D) :  bisects (segment.mk A C) (segment.mk B D)
∧ bisects (segment.mk B D) (segment.mk A C) :=  begin – By the definition of a
rhombus, $AB = AD = BC = DC$.  have AB_eq_AD_and_BC_eq_DC : (segment.mk A B =
segment.mk A D) ∧ (segment.mk B C = segment.mk D C), from sorry,  – WLOG,
consider the diagonal $BD$.  have BD_eq_DC : segment.mk B D = segment.mk D C,
from sorry,  – Thus: $\triangle ABD$ is an isosceles triangle whose apex is
$A$ and whose base is $BD$.  have isosceles_triangle_ABD :
is_isosceles_triangle A B D, from sorry,  – By Diagonals of Rhombus Bisect
Angles, $AC$ bisects $\angle BAD$.  have AC_bisects_BAD : bisects (segment.mk
A C) (angle.mk B A D), from sorry,  – From Bisector of Apex of Isosceles
Triangle also Bisects Base, $AC$ bisects $BD$.  have AC_bisects_BD : bisects
(segment.mk A C) (segment.mk B D), from sorry,  – From Bisector of Apex of
Isosceles Triangle is Perpendicular to Base, $AC$ bisects $BD$ at right
angles.  have AC_bisects_BD_at_right_angles : bisects_at_right_angles
(segment.mk A C) (segment.mk B D), from sorry,  – Hence the result.  show
bisects (segment.mk A C) (segment.mk B D) ∧ bisects (segment.mk B D)
(segment.mk A C), from sorry,  end Figure 8: Codex “suggested” designing _line
segment_ as a structure _segment_ and treated _point_ as a type, for defining
4 vertices.

####  D.3.2 Effect of example few-shot prompts on Codex output

We show the effect of few-shot prompts with an example of the formalisation of
theorem _Cube of sum_. In one case, we included the theorem _square of sum_ in
the few shot prompts and in the other case we did not. In both of these cases,
we provided the NL proof of _Cube of sum_ using _Binomial Theorem_. We observe
that, in the first case, Codex directly took cues from the _square of sum_
theorem and deviated from the NL proof provided; while in the second case,
Codex translated the NL proof of _Cube of sum_ with important intermediate
steps.

_Theorem statement_ :

$(x+y)^{3}=x^{3}+3x^{2}y+3xy^{2}+y^{3}$

_Natural language proof_ :

Follows directly from the Binomial Theorem:

$\displaystyle\forall n\in Z_{\geq
0}:(x+y)^{n}=\sum_{k\mathop{=}0}^{n}\binom{n}{k}x^{n-k}y^{k}$

putting $n=3$.

$Q.E.D.$

Codex outputs for the two cases are shown in Figure 9 and Figure 10
respectively.

⬇ Completion 1 (including ”Square of Sum” in few shot prompts):  theorem
cube_of_sum (x y : ℝ) : (x + y)^3 = (x^3 + 3*x^2*y + 3*x*y^2 + y^3) :=  begin
calc (x + y)^3 = (x+y)*(x+y)*(x+y) : by sorry … = (x+y)*(x^2 + 2*x*y + y^2) :
by sorry … = x*(x^2 + 2*x*y + y^2) + y*(x^2 + 2*x*y + y^2) : by sorry … =
x*x^2 + x*2*x*y + x*y^2 + y*x^2 + y*2*x*y + y*y^2 : by sorry … = x^3 + 2*x^2*y
+ x*y^2 + x^2*y + 2*x*y^2 + y^3 : by sorry … = x^3 + 3*x^2*y + 3*x*y^2 + y^3 :
by sorry,  end Figure 9: Codex deviated from the natural language proof and
instead outputted the proof outline involving expanding the terms and
manipulating the expressions, possibly taking cues from the _Square of Sum_
prompt. ⬇ Completion 2 (not including ”Square of Sum” in few shot prompts):
theorem cube_of_sum : ∀ x y : ℝ, (x + y)^3 = x^3 + 3 * x^2 * y + 3 * x * y^2 +
y^3 :=  begin assume (x y : ℝ),  have : (x + y)^3 = ∑ k in finset.range 3, (3
choose k) * x^(3 - k) * y^k, from sorry,  have : (x + y)^3 = (3 choose 0) *
x^(3 - 0) * y^0 + (3 choose 1) * x^(3 - 1) * y^1 + (3 choose 2) * x^(3 - 2) *
y^2 + (3 choose 3) * x^(3 - 3) * y^3, from sorry,  have : (x + y)^3 = 1 * x^3
* y^0 + 3 * x^2 * y^1 + 3 * x * y^2 + 1 * x^0 * y^3, from sorry,  have : (x +
y)^3 = x^3 + 3 * x^2 * y + 3 * x * y^2 + y^3, from sorry,  show (x + y)^3 =
x^3 + 3 * x^2 * y + 3 * x * y^2 + y^3, from sorry,  end Figure 10: Codex stuck
to the natural language proof and also added some more intermediate steps
important for formalisation. Although, there is a minor Lean error in ”choose”
definition – it should be 3.choose 2 instead of 3 choose 2.

####  D.3.3 Simple Algebraic Manipulations

We experimented with Codex’s ability to perform algebraic manipulations by
analogy. With a few example prompts, we appended the _square of sum_ NL proof,
its Lean formalisation and the phrase _4th power of Sum_. Codex then outputted
the $4$th, $8$th, ..$16$th power of sum. We observed that for the $4$th power
and $8$th power of the term (x + y), algebraic manipulations and final results
were accurate, however, from $16$th power onwards, Codex outputted partial
expressions and some of these terms were incorrect. We provided the following
prompt to Codex:

⬇

/–‘theorem‘

Euclid’s Theorem

For any [[Definition:Finite Set|finite set]] of [[Definition:Prime
Number|prime numbers]], there exists a [[Definition:Prime Number|prime
number]] not in that [[Definition:Set|set]].

‘proof‘

Let $\mathbb P$ be a [[Definition:Finite Set|finite set]] of
[[Definition:Prime Number|prime numbers]].

Consider the number:

:$\displaystyle n_p = \paren {\prod_{p \mathop \in \mathbb P} p} + 1$

Take any $p_j \in \mathbb P$.

We have that:

: $\displaystyle p_j \divides \prod_{p \mathop \in \mathbb P} p$

Hence:

:$\displaystyle \exists q \in \Z: \prod_{p \mathop \in \mathbb P} p = q p_j$

So:

{{begin-eqn}}

{{eqn | l = n_p

| r = q p_j + 1

| c = [[Division Theorem]]

}}

{{eqn | ll= \leadsto

| l = n_p

| o = \perp

| r = p_j

| c = {{Defof|Coprime Integers}}

}}

{{end-eqn}}

So $p_j \nmid n_p$.

There are two possibilities:

:$(1): \quad n_p$ is [[Definition:Prime Number|prime]], which is not in
$\mathbb P$.

:$(2): \quad n_p$ is [[Definition:Composite Number|composite]].

But from [[Positive Integer Greater than 1 has Prime Divisor]], it must be
divisible by ”some” prime.

That means it is divisible by a prime which is not in $\mathbb P$.

So, in either case, there exists at least one [[Definition:Prime
Number|prime]] which is not in the original set $\mathbb P$ we created.

{{qed}}

-/

euclid_infinitude_primes : {p : ℕ | prime p}.infinite :=

begin

assume (primes : {p | prime p}.finite),

let $\mathbb{P}$ := set.finite.to_finset primes,

let np := $\mathbb{P}$.val.prod + 1,

have hprime_div_prod : ∀ p_j ∈ $\mathbb{P}$, p_j | $\mathbb{P}$.val.prod , from sorry,

have prime_div_rem : ∀ p_j ∈ $\mathbb{P}$, ∃ q, $\mathbb{P}$.val.prod = p_j *
q, from sorry,

have prime_not_div_n_p : ∀ p_j ∈ $\mathbb{P}$, ¬(p_j | np), from sorry,

have prime_not_in_$\mathbb{P}$ : ∃ p, prime p ∧ p ∉ $\mathbb{P}$, from sorry,

show false, by {

rcases prime_not_in_$\mathbb{P}$ with ⟨p, hprime : prime p,
hnot_in_$\mathbb{P}$ : p ∉ $\mathbb{P}$⟩,

have : p ∈ $\mathbb{P}$, by {apply set.mem_to_finset.mpr, exact hprime,},

contradiction, }

end

/–‘theorem‘

Power Set is Closed under Intersection

Let $S$ be a [[Definition:Set|set]].

Let $\powerset S$ be the [[Definition:Power Set|power set]] of $S$.

Then:

:$\forall A, B \in \powerset S: A \cap B \in \powerset S$

‘proof‘

Let $A, B \in \powerset S$.

Then by the definition of [[Definition:Power Set|power set]], $A \subseteq S$
and $B \subseteq S$.

From [[Intersection is Subset]] we have that $A \cap B \subseteq A$.

It follows from [[Subset Relation is Transitive]] that $A \cap B \subseteq S$.

Thus $A \cap B \in \powerset S$ and [[Definition:Closure (Abstract
Algebra)|closure]] is proved.

{{qed}}

-/

power_set_intersection_closed {α : Type*} (S : set α) : ∀ A B ∈ $\mathcal{P}$
S, (A ∩ B) ∈ $\mathcal{P}$ S :=

begin

assume (A : set α) (hA : A ∈ $\mathcal{P}$ S) (B : set α) (hB : B ∈
$\mathcal{P}$ S),

have : (A ⊆ S) ∧ (B ⊆ S), from sorry,

have : (A ∩ B) ⊆ A, from sorry,

have : (A ∩ B) ⊆ S, from sorry,

show (A ∩ B) ∈ $\mathcal{P}$ S, from sorry,

end

/–‘theorem‘

Square of Sum

:$\forall x, y \in \R: \paren {x + y}^2 = x^2 + 2 x y + y^2$

‘proof‘

Follows from [[Real Multiplication Distributes over Addition|the distribution
of multiplication over addition]]:

{{begin-eqn}}

{{eqn | l = \left({x + y}\right)^2

| r = \left({x + y}\right) \cdot \left({x + y}\right)

}}

{{eqn | r = x \cdot \left({x + y}\right) + y \cdot \left({x + y}\right)

| c = [[Real Multiplication Distributes over Addition]]

}}

{{eqn | r = x \cdot x + x \cdot y + y \cdot x + y \cdot y

| c = [[Real Multiplication Distributes over Addition]]

}}

{{eqn | r = x^2 + 2xy + y^2

| c =

}}

{{end-eqn}}

{{qed}}

-/

square_of_sum (x y : ℝ) : (x + y)^2 = (x^2 + 2*x*y + y^2)

begin

calc (x + y)^2 = (x+y)*(x+y) : by sorry

… = x*(x+y) + y*(x+y) : by sorry

… = x*x + x*y + y*x + y*y : by sorry

… = x^2 + 2*x*y + y^2 : by sorry,

end

/–‘theorem‘

4th power of Sum

Codex output is shown in Figure 11.

⬇ :$\forall x, y \in \R: \paren {x + y}^4 = x^4+4 x^3 y+6 x^2 y^2 + 4 x y^3 +y^4$ ‘proof‘  Follows from [[Square of Sum]]:  {{begin-eqn}}  {{eqn | l = \left({x + y}\right)^4  | r = \left({x + y}\right)^2 \cdot \left({x + y}\right)^2  }}  {{eqn | r = \left({x^2 + 2xy + y^2}\right) \cdot \left({x^2 + 2xy + y^2}\right)  | c = [[Square of Sum]]  }}  {{eqn | r = x^4 + 4x^3y + 6x^2y^2 + 4xy^3 + y^4  | c =  }}  {{end-eqn}}  {{qed}}  -/  fourth_power_of_sum (x y : ℝ) : (x + y)^4 = (x^4 + 4*x^3*y + 6*x^2*y^2 + 4*x*y^3 + y^4) :=  begin calc (x + y)^4 = (x + y)^2 * (x + y)^2 : by sorry … = (x^2 + 2*x*y + y^2) * (x^2 + 2*x*y + y^2) : by sorry … = x^4 + 4*x^3*y + 6*x^2*y^2 + 4*x*y^3 + y^4 : by sorry,  end /–‘theorem‘  8th power of Sum :$\forall x, y \in \R: \paren {x + y}^8 = x^8+8 x^7 y+28 x^6 y^2 + 56 x^5 y^3 + 70 x^4 y^4 + 56 x^3 y^5 + 28 x^2 y^6 + 8 x y^7 + y^8$ ‘proof‘  Follows from [[4th power of Sum]]:  {{begin-eqn}}  {{eqn | l = \left({x + y}\right)^8  | r = \left({x + y}\right)^4 \cdot \left({x + y}\right)^4  }}  {{eqn | r = \left({x^4 + 4x^3y + 6x^2y^2 + 4xy^3 + y^4}\right) \cdot \left({x^4 + 4x^3y + 6x^2y^2 + 4xy^3 + y^4}\right)  | c = [[4th power of Sum]]  }}  {{eqn | r = x^8 + 8x^7y + 28x^6y^2 + 56x^5y^3 + 70x^4y^4 + 56x^3y^5 + 28x^2y^6 + 8xy^7 + y^8  | c =  }}  {{end-eqn}}  {{qed}}  -/  eighth_power_of_sum (x y : ℝ) : (x + y)^8 = (x^8 + 8*x^7*y + 28*x^6*y^2 + 56*x^5*y^3 + 70*x^4*y^4 + 56*x^3*y^5 + 28*x^2*y^6 + 8*x*y^7 + y^8) :=  begin calc (x + y)^8 = (x + y)^4 * (x + y)^4 : by sorry … = (x^4 + 4*x^3*y + 6*x^2*y^2 + 4*x*y^3 + y^4) * (x^4 + 4*x^3*y + 6*x^2*y^2 + 4*x*y^3 + y^4) : by sorry … = x^8 + 8*x^7*y + 28*x^6*y^2 + 56*x^5*y^3 + 70*x^4*y^4 + 56*x^3*y^5 + 28*x^2*y^6 + 8*x*y^7 + y^8 : by sorry,  end Figure 11: Codex recognised the pattern and gave the natural proof and the corresponding proof outlines for (x+y)^4, (x+y)^8, etc. For 4th power and 8th power, algebraic manipulations and final results were accurate, however, from 16th power onwards, Codex outputted partial expressions and some of these terms were incorrect.

###  D.4 Theorem-wise analysis

####  D.4.1 Absolute Value Function is Convex

The maximum score awarded was 3 to the full proof and proof outline formats.
An accurate statement was generated for the full proof format. Overall, the
proof structures seemed useful.

Most of the outputs from Codex resembled the natural language proof to a great
extent. Interestingly, in one case, Codex directly outputted the simplified
statement that precisely needed to be proved, possibly taking cues from the
natural language proof provided – it didn’t use the convex_on definition from
mathlib and directly outputted ∀ (x y : ℝ), ∀ (α β : ℝ), α ≥ 0 ∧ β ≥ 0 ∧ α + β
= 1 → abs (α * x + β * y) ≤ (α * abs x + β * abs y) as the theorem statement
to be proved. This is shown in Figure 3. Also, the generated outputs followed
Lean syntax at a decent level. While checking for contamination, we didn’t
find this theorem formalised online.

There were instances where some steps were mathematically incorrect, such as
treating the triangle inequality of absolute function as an equality, wrong
conditions on some variables etc. There were some observations of
hallucination in some outputs, that led to lesser scores.

The best format (full proof) was observed at temperature 0.4 (please refer
Figure 3). Also, the correct Lean statement was not included in the prompt. We
also show another good format (proof outline) at temperature 0.4.

_Theorem statement:_

Let $f:\mathbb{R}\to\mathbb{R}$ be the absolute value function on the real
numbers. Then $f$ is convex.

_Natural language proof:_

Let $x,y\in\mathbb{R}$.

Let $\alpha,\beta\in\mathbb{R}_{\geq 0}$ where $\alpha+\beta=1$.

$\displaystyle f(\alpha x+\beta y)$ $\displaystyle=|\alpha x+\beta y|$
Definition of f $\displaystyle\leq|\alpha x|+|\beta y|$ Triangle Inequality
for Real Numbers $\displaystyle=|\alpha||x|+|\beta||y|$ Absolute Value of
Product $\displaystyle=\alpha|x|+\beta|y|$ Definition of Absolute Value
$\displaystyle=\alpha f(x)+\beta f(y)$ Definition of f

Hence the result by definition of convex real function.

$Q.E.D.$

_Codex Output with Corrections:_

⬇

theorem abs_convex : convex_on abs ℝ (@set.univ $\mathbb{R}$) abs :=

begin

split,

assume (x y :$\mathbb{R}$) (hx : x $\in$ set.univ) (hy : y $\in$ set.univ)

($\alpha$ $\beta$ : $\mathbb{R}$) (h$\alpha$ : $0\leq\alpha$) (h$\beta$ :
$0\leq\beta$) (h$\alpha$$\beta$ : $\alpha$ \+ $\beta$ = 1),

show ( $\alpha$* x + $\beta$ * y $\in$ set.univ), from dec_trivial,

– Let $x, y \in \R$.

assume (x y : ℝ) , (hx : x $\in$ set.univ) (hy : y $\in$ set.univ),

– Let $\alpha, \beta \in \R_{\ge 0}$ where $\alpha + \beta = 1$.

assume (α β : ℝ) (h1 : α ≥ 0) (h2 : β ≥ 0) (h3 : α + β = 1),

– expand the function

calc abs (α*x + β*y) = abs (α*x + β*y) : by sorry refl

– triangle inequality for real numbers gives:

… ≤ abs (α*x) + abs (β*y) : by sorry {apply abs_add}

– absolute value of product gives:

… = abs α * abs x + abs β * abs y : by sorry {rw [abs_mul $\alpha$ x,abs_mul]}

– absolute value of real number gives:

… = α * abs x + β * abs y : by sorry

– expand the function

… = $\alpha$ * abs x + $\beta$ * abs y : by sorry {rw [abs_of_nonneg h1
,abs_of_nonneg h2]}

– hence the result by definition of convex real function

… ≤ α * abs x + β * abs y : by sorry linarith,

end

####  D.4.2 Schur’s Inequality

The maximum score awarded to all the proof formats was 3. From the natural
language proof, we removed mathematical idioms like “without loss of
generality” and “symmetric” since Codex got stuck at trivial steps,
translating these idioms. With a simplified version of the proof, we observed
improvement in all the formats. Statement formalisation by Codex was accurate
in majority of the outputs. While checking for contamination, we didn’t find
this theorem formalised online

Codex completions were aligned with the natural language proof. Interestingly,
there were outputs in which Codex tried to output the essential intermediate
steps that were not present in the natural language proof. These intermediate
steps turned out to be extremely important while completing the generated
proof to correct proof. Outputs followed Lean syntax in majority of cases,
however, there were few cases where minor syntactic errors in expressions were
found.

Major sources of less scores were – outputs getting stuck at some steps and
few instances of hallucinations. For this theorem, there were no mathematical
errors observed.

We show the full proof format at temperature 0.2. Similar formats were also
observed for the 0.4 and 0.8 temperatures. The correct Lean theorem statement
was not included in the prompt.

_Theorem statement:_

Let $x,y,z\in\mathbb{R}_{\geq 0}$ be positive real numbers such that $x\geq
y\geq z\geq 0$.

Let $t\in\mathbb{R},t>0$ be a (strictly) positive real number.

Then:

$x^{t}(x-y)(x-z)+y^{t}(y-z)(y-x)+z^{t}(z-x)(z-y)\geq 0$

_Natural language proof:_

Consider the expression:

$(x-y)(x^{t}(x-z)-y^{t}(y-z))+z^{t}(x-z)(y-z)$

We see that every term in the above is non-negative. So, directly:

$1$: $(x-y)(x^{t}(x-z)-y^{t}(y-z))+z^{t}(x-z)(y-z)\geq 0$

$1$ can be rearranged to Schur’s inequality.

$Q.E.D.$

_Codex Output with Corrections:_

⬇

theorem schur_inequality_short_simpler {x y z t  : ℝ} (hx : x ≥ 0) (hy : y ≥
0) (hz : z ≥ 0) (hxy : x ≥ y) (hyz : y ≥ z) (ht : t > 0) :

x^t * (x - y) * (x - z) + y^t * (y - z) * (y - x) + z^t * (z - x) * (z - y) ≥
0 :=

begin

– Consider the expression:

have h1 : (x - y) * (x^t * (x - z) - y^t * (y - z)) + z^t * (x - z) * (y - z)
≥ 0, from by {

– We see that every term in the above is non-negative. So, directly:

have h2 : (x - y) ≥ 0, from by {rw $\leftarrow$ ge_iff_le at $*$, rw
sub_nonneg, exact hxy},

have h3 : (x^t * (x - z) - y^t * (y - z)) ≥ 0, from by {

have h4 : (x - z) ≥ 0, from by {rw $\leftarrow$ ge_iff_le at $*$,rw
sub_nonneg, exact \hlr{hx\\},} ge_trans hxy hyz},

have h5 : (y - z) ≥ 0, from by {rw $\leftarrow$ ge_iff_le at $*$, rw
sub_nonneg, exact hyz},

have h6 : (x^t * (x - z) - y^t * (y - z)) = (x^t - y^t) * (x - z) + y^t * (x -
y), from by ring,

have h7 : (x^t - y^t) ≥ 0, from by {rw $\leftarrow$ sub_nonneg, exact
pow_le_pow hx ht ge_iff_le at $*$,rw sub_nonneg,rw real.rpow_le_rpow_iff hy
ht},

have h8 : $(x-y)\geq 0$, from by {rw $\leftarrow$ sub_nonneg, exact hxy}, hx
ht,assumption},

have h9 : (x^t - y^t) * (x - z) ≥ 0, from by {apply mul_nonneg, exact h7,
exact h4},

have h10 : y^t * (x - y) ≥ 0,

from by {apply mul_nonneg, exact pow_nonneg

rw ge_iff_le at $*$,

have h_1 : $0\leq t$, linarith,

have h_2 : $t\neq 0$, linarith,

have h_3 : $(0:\mathbb{R})\leq(0:\mathbb{R})$ , linarith,

have h_4 := real.rpow_le_rpow h_3 hy ht, exact h8}, h_1,

rw real.zero_rpow h_2 at h_4, assumption,linarith,},

have h11 : (x^t - y^t) * (x - z) + y^t * (x - y) ≥ 0, from by {apply
add_nonneg, exact h9, exact h10},

show (x^t * (x - z) - y^t * (y - z)) ≥ 0, from by {rw h6, exact h11},

},

have h12 : (x - z) ≥ 0, from by {rw $\leftarrow$ ge_iff_le at $*$,rw
sub_nonneg, exact hx}, ge_trans hxy hyz},

have h13 : (y - z) ≥ 0, from by {rw $\leftarrow$ ge_iff_le at $*$, rw
sub_nonneg, exact hyz},

have h14 : z^t * (x - z) * (y - z) ≥ 0, from by

{apply mul_nonneg, exact pow_nonneg

apply mul_nonneg,

rw ge_iff_le at $*$,

have h_1 : $0\leq t$, linarith,

have h_2 : $t\neq 0$, linarith,

have h_3 : $(0:\mathbb{R})\leq(0:\mathbb{R})$ , linarith,

have h_4 := real.rpow_le_rpow h_3 hz ht, exact h12, exact h13}, h_1,

rw real.zero_rpow h_2 at h_4, assumption, linarith, linarith,},

have h15 : (x - y) * (x^t * (x - z) - y^t * (y - z)) + z^t * (x - z) * (y - z)
≥ 0, from by

{apply add_nonneg,

apply mul_nonneg,

exact h2,

exact h3,

exact h14},

show (x - y) * (x^t * (x - z) - y^t * (y - z)) + z^t * (x - z) * (y - z) ≥ 0,
from by {exact h15},

},

– $(1) can be rearranged to Schur’s inequality.

have h16 : (x - y) * (x^t * (x - z) - y^t * (y - z)) + z^t * (x - z) * (y - z)
= x^t * (x - y) * (x - z) + y^t * (y - z) * (y - x) + z^t * (z - x) * (z - y),
from by ring,

show x^t * (x - y) * (x - z) + y^t * (y - z) * (y - x) + z^t * (z - x) * (z -
y) ≥ 0, from by {rw $\leftarrow$ h16, exact h1},

end

####  D.4.3 Nesbitt’s Inequality

A proof outline format stood out with the score of 3 as compared to 1 for
other formats.

Major sources of less scores were inability to translate Latex expressions,
mathematical errors pertaining to inequalities and simple algebraic
manipulations, and getting stuck at trivial steps. Since the natural language
proof followed a backward reasoning pattern, it might have been harder for
Codex to align the forward style format provided in the few-shot prompts to
this setting. While checking for contamination, we didn’t find this theorem
formalised online

_Theorem statement:_

Let $a$, $b$ and $c$ be positive real numbers.

Then:

$\dfrac{a}{b+c}+\dfrac{b}{a+c}+\dfrac{c}{a+b}\geq\dfrac{3}{2}$

_Natural language proof:_

$\frac{a}{b+c}+\frac{b}{a+c}+\frac{c}{a+b}\geq\dfrac{3}{2}$

$\Rightarrow\frac{a+b+c}{b+c}+\frac{a+b+c}{a+c}+\frac{a+b+c}{a+b}\geq\frac{9}{2}$
by adding $3$

$\Rightarrow\frac{a+b+c}{b+c}+\frac{a+b+c}{a+c}+\frac{a+b+c}{a+b}\geq\frac{9(a+b+c)}{(b+c)+(a+c)+(a+b)}$
as $\dfrac{a+b+c}{(b+c)+(a+c)+(a+b)}=\dfrac{1}{2}$

$\Rightarrow\frac{\frac{1}{b+c}+\frac{1}{a+c}+\frac{1}{a+b}}{3}\geq\frac{3}{(b+c)+(a+c)+(a+b)}$
dividing by $3(a+b+c)$

These are the arithmetic mean and the harmonic mean of $\dfrac{1}{b+c}$,
$\dfrac{1}{a+c}$ and $\dfrac{1}{a+b}$.

From Arithmetic Mean is Never Less than Harmonic Mean the last inequality is
true.

Thus Nesbitt’s Inequality holds.

$Q.E.D$

The best proof format (proof outline) was observed at temperature 0.4. We
included the correct Lean statement in the prompt.

_Codex Output_

⬇

theorem nesbitt_inequality {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
: (a / (b + c)) + (b / (a + c)) + (c / (a + b)) ≥ (3 / 2) :=

begin

– $\dfrac a {b + c} + \dfrac b {a + c} + \dfrac c {a + b}$

have h1 : (a / (b + c)) + (b / (a + c)) + (c / (a + b)) ≥ (3 / 2), from sorry,

– adding $3$

have h2 : (a / (b + c)) + (b / (a + c)) + (c / (a + b)) + 3 ≥ (3 / 2) + 3,
from sorry,

– as $\dfrac {a + b + c} {\paren {b + c} + \paren {a + c} + \paren {a + b} } =
\dfrac 1 2$

have h3 : (a / (b + c)) + (b / (a + c)) + (c / (a + b)) + 3 ≥ (9 * (a + b +
c)) / ((b + c) + (a + c) + (a + b)), from sorry,

– dividing by $3 \paren {a + b + c}$

have h4 : ((a / (b + c)) + (b / (a + c)) + (c / (a + b)) + 3) / (3 * (a + b +
c)) ≥ ((9 * (a + b + c)) / ((b + c) + (a + c) + (a + b))) / (3 * (a + b + c)),
from sorry,

– $\dfrac {\frac 1 {b + c} + \frac 1 {a + c} + \frac 1 {a + b} } 3$

have h5 : ((a / (b + c)) + (b / (a + c)) + (c / (a + b)) + 3) / (3 * (a + b +
c)) ≥ (1 / (b + c) + 1 / (a + c) + 1 / (a + b)) / 3, from sorry,

– $\dfrac 3 {\paren {b + c} + \paren {a + c} + \paren {a + b} }$

have h6 : ((a / (b + c)) + (b / (a + c)) + (c / (a + b)) + 3) / (3 * (a + b +
c)) ≥ 3 / ((b + c) + (a + c) + (a + b)), from sorry,

– These are the arithmetic mean and the harmonic mean of $\dfrac 1 {b + c}$,
$\dfrac 1 {a + c}$ and $\dfrac 1 {a + b}$.

– From Arithmetic Mean is Never Less than Harmonic Mean the last inequality is
true.

have h7 : ((a / (b + c)) + (b / (a + c)) + (c / (a + b)) + 3) / (3 * (a + b +
c)) ≥ 3 / ((b + c) + (a + c) + (a + b)), from sorry,

– Thus Nesbitt’s Inequality holds.

show (a / (b + c)) + (b / (a + c)) + (c / (a + b)) ≥ (3 / 2), from sorry,

end

####  D.4.4 Overflow theorem

The Overflow theorem is a standard application of the Compactness theorem from
first-order logic. While the proof is fairly short and easy for a human to
comprehend, there are a number of difficulties in translating the informal
natural language proof to a formal one:

  1. 1.

Phrases such as “arbitrarily large” are difficult for the model to directly
cast into symbolic notation such as $\forall n\in\mathbb{N},\exists
m\in\mathbb{N},m>n\implies\ldots$.

  2. 2.

Expressions that make use of informal mathematical notation such as $\ldots$
are difficult for the model to make precise.

  3. 3.

The notions of “finite” and “infinite” are quite subtle for the model.

As the proof is fairly short, the outlines were sometimes too sparse and
inadequate. Full proofs seemed be better overall, and proofs with premises
were a close second. The _Compactness theorem_ , a crucial ingredient in the
proof, is occasionally captured in the premises of auto. The overall
performance seemed to improve at higher temperatures, especially $0.8$.

When given the correct statement, the quality of some of the definitions in
the proof went up slightly. Although the proof outlines and outlines with
premises were slightly better in this setting, the quality of full proofs went
down.

_Theorem statement:_

Let $F$ be a set of first-order formulas which has finite models of
arbitrarily large size.

Then $F$ has an infinite model.

_Natural language proof:_

For each $n$, let $\mathbf{A}_{n}$ be the formula:

$\exists x_{1}\exists x_{2}\ldots\exists x_{n}:\\{x_{1}\neq x_{2}\land
x_{1}\neq x_{3}\land\ldots\land x_{n-1}\neq x_{n}\\}$

Then $\mathbf{A}_{i}$ is true in a structure $\AA$ iff $\AA$ has at least $n$
elements.

Take:

$\Gamma:=F\cup\bigcup_{i\mathop{=}1}^{\infty}A_{i}$

Since $F$ has models of arbitrarily large size, every finite subset of
$\Gamma$ is satisfiable.

From the Compactness Theorem, $\Gamma$ is satisfiable in some model
$\mathbf{M}$.

But since $\mathbf{M}\models A_{i}$ for each $i$, $\mathbf{M}$ must be
infinite.

So $F$ has an infinite model.

$Q.E.D.$

_Codex Output_ (Full proof, Temperature 0.8)

⬇

theorem overflow_theorem (F : set FOL) : finite_models → infinite_model F :=

begin

– Assume $F$ has finite models of arbitrarily large size

assume h1 : finite_models F,

– Let $F$ be a set of first-order formulas which has finite models of
arbitrarily large size.

assume h2 : ∀ n, (∃ m : model, m ∈ P F ∧ card m ≥ n),

– Then $F$ has an infinite model.

have h3 : infinite_model F, from

begin

– define $\mathbf A_n$

let A_n := {x_1, x_2, x_1 ≠ x_2},

– $\mathbf A_i$ is true in a structure $\AA$ iff $\AA$ has at least $n$
elements.

have h4 := by {

assume i,

assume m : model,

assume hm : m ∈ P F ∧ card m ≥ i,

have h5 := and.right hm,

have h6 := classical.some (h2 i),

have h7 : m ∈ P F ∧ card m ≥ n ↔ card m > n, from

by { split, assume h, from h, assume h, from ⟨and.left hm, by {rw [←
not_le],exact h}⟩},

have h8 := h6.right h7,

have h9 : and.left h6 → ∃ A, A ⊆ F ∧ m ⊆ A, from

by { simp, assume h, use {m}, split, from and.left hm, from
set.singleton_subset _, },

have h10 := h9 (and.left h6),

have h11 := classical.some_spec h10,

exact h11.left,

},

– Take: $$ \Gamma := F \cup \bigcup_{i \mathop = 1}^\infty A_i $$

let Γ := F ∪ (Union A_n),

– Since $F$ has models of arbitrarily large size, every finite subset of
$\Gamma$ is satisfiable.

have h5 : finite_models (finite_subset Γ), from

begin

– By ‘finite_models‘, every finite subset of $F$ is satisfiable.

have h6 : finite_models (finite_subset F), from by

apply (finite_models_finite_subset F),

– So consider a finite subset $X$ of $\Gamma$

assume X : set FOL,

assume hX : X ⊆ Γ ∧ finite X,

– Notice that if $X$ contains finitely many of $\mathbf A_n$, then $X$ has a
model.

have h7 : finite (X ∩ A_n), from by {

apply set.finite.inter (nat → set FOL) _ _ _ _ (set.finite_setof FOL A_n)

(set.countable_finite x (X ∩ A_n)), },

have h8 : finite_models (X ∪ (X ∩ A_n)), from by {

apply finite_models_union, split, exact h6 (X ∩ F), exact h7, },

– Hence: $$X \cup \left(X \cap \bigcup_{i \mathop = 1}^\infty A_i\right)$$

– By distributivity of union over union, we have that:

– $$X \cup \left(X \cap \bigcup_{i \mathop = 1}^\infty A_i\right)$$

– $$= X \cup \left(\bigcup_{i \mathop = 1}^\infty \left(X \cap
A_i\right)\right)$$

have h9 : finite_models (X ∪ (Union $ λ i : ℕ, X ∩ A_i)), from by apply
finite_models_union X,

– Nevertheless, we have that:

have h10 : (X ∩ A_n) ∪ Union (X ∩ A_n) = A_n, from

begin

apply set.eq_union_left, intro i,

{ apply set.disjoint_left,

apply (set.disjoint_singleton_right_of_not_mem FOL X),

assume h,

have h : i ∈ X ∧ i ∈ A_n, from h.right,

have h11 := h.right,

exact (h10 i).right (and.right h11),

},

end,

– $$X \cup \left(\bigcup_{i \mathop = 1}^\infty \left(X \cap
A_i\right)\right)$$

– So this is just $X$.

have h11 := h9 X,

– We know that $X$ has a model, since $X$ contains finitely many of $\mathbf
A_n$.

have h12 : finite_models X, from by {apply subset_union_right X, exact
h10.symm, exact h11},

have h13 := and.left hX,

have h14 := h12 h13,

– So $F$ has finite models.

exact h14,

end,

– From the Compactness Theorem, $\Gamma$ is satisfiable in some model
$\mathbf{M}$.

have h6 := compactness_theorem Γ h5,

– But since $\mathbf{M} \models A_i$ for each $i$, $\mathbf{M}$ must be
infinite.

have h7 := by {

assume i,

have h8 := and.right h6,

have h9 := and.right h8,

have h10 := h9 A_i,

have h11 := by {

have h12 := set.mem_Union.mp h10,

have h13 := and.right h12,

have h14 := and.right h13,

have h15 := h4 m i,

have h16 := h15.left,

have h17 := h16 m,

have h18 := and.right h17,

exact h18,

},

have h12 := set.not_empty_iff_exists_mem.mp h11,

have h13 := h12,

have h14 := classical.some_spec h13,

have h15 := set.countable_finite x m,

have h16 := card_le_of_subset h15.left h14.left,

have h17 := h15.right h16,

have h18 := nat.succ_pos i,

exact h17 (nat.succ_pos i),

},

– So $F$ has an infinite model.

exact h7,

end,

– Hence $F$ has an infinite model.

exact h3,

end

####  D.4.5 Contraction mapping theorem

The formalisation of the statement scored 2 on average. Codex got most of the
details right, and faltered mostly by taking the wrong interval for $k$. Also,
mathlib uses a few instances to represent a Banach space, however Codex
hallucinated and used banach_space instead. Both full proofs and proof oulines
performed well. The best score was 3, an example of which is shown below (the
proof is the same as the one generated by Codex, we used LaTeXinstead of
Unicode due to erroneous display of certain Unicode characters). While this
theorem is similar to a theorem in mathlib, the proofs are very different: the
mathlib proof assumes the existence of a Cauchy sequence, while ours
constructs the Cauchy sequence.

This proof was a bit challenging. It required Codex to use induction both
implicitly and explicitly, and to appropriately translate the $\cdots$
notation. Codex was somewhat successful in the former, however mostly failed
with the latter. A marked improvement in performance was observed with adding
comments, however increasing temperature did not make much of a difference.
Codex had some difficulty with formalising convergence.

_Theorem statement:_

Let $B$ be a Banach space, $M$ a closed subset of $B$, and $\Phi$ a mapping
from $M$ to $M$ such that for some $k\in[0,1)$,

$\|\Phi(x)-\Phi(y)\|\leq k\|x-y\|$

_Natural language proof:_

for any two points $x$ and $y$ in $M$. Then there is a unique point $z$ in $M$
such that $\Phi(z)=z$.

Choose some $x_{0}$ in $M$. Define a sequence $\left\\{x_{i}\right\\}$ by
setting $x_{i+1}=\Phi\left(x_{i}\right)$, for $i\in\mathbb{N}$. Then for any
$n$,

$x_{n}=x_{0}+\left(x_{1}-x_{0}\right)+\left(x_{2}-x_{1}\right)+\cdots+\left(x_{n}-x_{n-1}\right)$

Also, for $i\geq 1$

$\left\|x_{i+1}-x_{i}\right\|\leq k\left\|x_{i}-x_{i-1}\right\|\text{, }$

and by induction we easily show that

$\left\|x_{i+1}-x_{i}\right\|\leq k^{i}\left\|x_{1}-x_{0}\right\|$

Because $|k|<1,\sum_{i=1}^{\infty}k^{i}$ converges, which implies that
$\sum_{i=1}^{\infty}\left\|x_{i+1}-x_{i}\right\|$ converges. By the
Weirerstrass M test, $\sum_{i=1}^{\infty}\left(x_{i+1}-x_{i}\right)$ converges
in $B$, and hence $\lim_{n\rightarrow\infty}x_{n}$ exists. Let $z$ be this
limit. Since $M$ is closed and $x_{n}\in M$ for each $n,z\in M$. Also,
$x_{n+1}=\Phi\left(x_{n}\right)$, and so (from the definition of limit)

$\lim_{n\rightarrow\infty}\Phi\left(x_{n}\right)=\lim_{n\rightarrow\infty}x_{n+1}=z$

Further, for any $n$,

$\displaystyle\|\Phi(z)-z\|$
$\displaystyle=\left\|\Phi(z)-\Phi\left(x_{n}\right)+\Phi\left(x_{n}\right)-z\right\|$
$\displaystyle\leq
k\left\|z-x_{n}\right\|+\left\|\Phi\left(x_{n}\right)-z\right\|$

Since the limit of the right side as $n\rightarrow\infty$ is zero, and the
left side is independent of $n$, it follows that the left side is zero for
every $n$, and so $z$ is a fixed point for $\Phi$.

To prove uniqueness, suppose that there are two fixed points, say $x$ and $y$.
Then

$f(x)=x,f(y)=y$

and so

$|x-y|=|f(x)-f(y)|\leq k|x-y|$

where $0<k<1$. This is only possible if $x=y$.

$Q.E.D$

Following is one of the best scored outputs (proof outline, temperature 0.8,
score 3).

_Codex Output_

theorem contraction_mapping (B : Type*) [banach_space B]

$(\mathrm{M}:$ set B) [is_closed
$\mathrm{M}](\phi:\mathrm{M}\rightarrow\mathrm{M})$

$(\mathrm{h}1:\forall\mathrm{x}\mathrm{y}\in\mathrm{M},\|\phi\mathrm{x}-\phi\mathrm{y}\|\leq\mathrm{k}*(\|\mathrm{x}-\mathrm{y}\|))$

(hk : $\mathrm{k}<1$ ) :

$\exists!\mathrm{z}\in\mathrm{M},\phi\mathrm{z}=\mathrm{z}:=$

begin

– – choose some $x_{0}$ in $M$. choose (x0:B) hx0 using M.nonempty,

– – Define a sequence $\left\\{x_{i}\right\\}$ by setting
$x_{i+1}=\Phi\left(x_{i}\right)$, for $i\in\mathbb{N}$.

let $\mathrm{xn}:=\lambda\mathrm{n}:\mathbb{N},\phi^{[1]}\mathrm{x}0$,

– – Then for any $n$,

$-x_{n}=x_{0}+\left(x_{1}-x_{0}\right)+\left(x_{2}-x_{1}\right)+\cdots+\left(x_{n}-x_{n-1}\right)$

have h3: $\forall\mathrm{n}:\mathbb{N}$, xn
$\mathrm{n}=\mathrm{x}0+(\mathrm{x}1-\mathrm{x}0)+(\mathrm{x}2-\mathrm{x}1)+\cdots+(\mathrm{xn}\mathrm{n}-\mathrm{xn}(\mathrm{n}-1))$,
from sorry,

– – Also, for $i\geq 1$

$--\left\|x_{i+1}-x_{i}\right\|\leq k||x_{i}-x_{i-1}\|$

have h4 : $\forall(\mathrm{i}:\mathbb{N})($ hi :
$1\leq\mathrm{i}),\|\mathrm{xn}(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}\|\leq\mathrm{k}*\|\mathrm{xn}\mathrm{i}-\mathrm{xn}(\mathrm{i}-1)\|$,
from sorry,

– – and by induction we easily show that

$-\left\|x_{i+1}-x_{i}\right\|\leq k^{i}||x_{1}-x_{0}\|$

have h5 : $\forall(\mathrm{i}:\mathbb{N})($ hi :
$1\leq\mathrm{i}),\|\mathrm{xn}(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}\|\leq(\mathrm{k}\wedge\mathrm{i})*\|\mathrm{xn}1-\mathrm{xn}0\|$,
from sorry,

– – Because $|k|<1,\sum_{i=1}^{\infty}k^{i}$ converges,

have $\mathrm{h}6:$ abs $\mathrm{k}<1$, from sorry,

have h7 : tendsto
$\left(\lambda\mathrm{i}:\mathbb{N},\mathrm{k}^{\wedge}\mathrm{i}\right)$
at_top $(\mathcal{N}1)$, from sorry,

have $\mathrm{h}7$ : tendsto
$(\lambda\mathrm{i}:\mathbb{N},(\mathrm{k}\wedge\mathrm{i})*\overline{\|}\mathrm{xn}1-\mathrm{xn}0\|)$
at_top $(\mathcal{N}(\|\mathrm{xn}1-\mathrm{xn}0\|))$, from sorry, have h8:
tendsto $(\lambda\mathrm{i}:\mathbb{N},\|\mathrm{xn}(\mathrm{i}+1)$ \- xn i
$\|)$ at_top $(\mathcal{N}(\|\mathrm{xn}1-\mathrm{xn}0\|))$, from sorry,

– – which implies that $\sum_{i=1}^{\infty}\left\|x_{i+1}-x_{i}\right\|$
converges.

have h9 : tendsto
$(\lambda\mathrm{i}:\mathbb{N},\Sigma\mathrm{j}\leq\mathrm{i},\|\mathrm{xn}(\mathrm{j}+1)-\mathrm{xn}\mathrm{j}\|)$
at_top
$\left(\mathcal{N}\left(\sum\mathrm{i},\|\mathrm{xn}(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}\|\right)\right)$,
from sorry,

– – By the Weirerstrass M test,
$\sum_{i=1}^{\infty}\left(x_{i+1}-x_{i}\right)$ converges in $B$, have h10:
$\sum\mathrm{i},\|\mathrm{xn}(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}\|<\infty$,
from sorry,

have h11 : tendsto
$\left(\lambda\mathrm{i}:\mathbb{N},\left(\sum\mathrm{j}\leq\mathrm{i},\mathrm{xn}(\mathrm{j}+1)-\mathrm{xn}\mathrm{j}\right)\right)$
at_top
$\left(\mathcal{N}\left(\sum\mathrm{i},\mathrm{xn}(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}\right)\right)$,
from sorry,

– – and hence $\lim_{n\rightarrow\infty}x_{n}$ exists.

have h12 : $\sum\mathrm{i}$, xn
$(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}=\mathrm{xn}1-\mathrm{xn}0+\sum\mathrm{i}>0$,
xn $(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}$, from sorry, have h13 :
$\lim(\lambda\mathrm{i}:\mathbb{N}$, xn
$(\mathrm{i}+1)-\mathrm{xn}\mathrm{i})=0$, from sorry, have h14 :
$\lim\left(\lambda\mathrm{i}:\mathbb{N},\sum\mathrm{j}\leq\mathrm{i}\right.$,
xn $\left.(\mathrm{j}+1)-\mathrm{xn}\mathrm{j}\right)=\sum\mathrm{i}$, xn
$(\mathrm{i}+1)-\mathrm{xn}\mathrm{i}$, from sorry, have h15 :
$\lim(\lambda\mathrm{i}:\mathbb{N},\Sigma\mathrm{j}\leq\mathrm{i}$, xn
$(\mathrm{j}+1))-\lim\left(\lambda\mathrm{i}:\mathbb{N},\sum\mathrm{j}\leq\mathrm{i},\mathrm{xn}\mathrm{j}\right)=\lim\left(\lambda\mathrm{i}:\mathbb{N},\left(\sum\mathrm{j}\leq\mathrm{i},\mathrm{xn}(\mathrm{j}\right.\right.$
$+1)-\mathrm{xn}\mathrm{j})$ ), from sorry,

have h16 : $\lim(\lambda\mathrm{i}:\mathbb{N},\Sigma\mathrm{j}\leq\mathrm{i}$,
xn
$(\mathrm{j}+1))=\lim(\lambda\mathrm{i}:\mathbb{N},\Sigma\mathrm{j}\leq\mathrm{i},\mathrm{xn}\mathrm{j})$,
from sorry, have h17 $:\lim(\lambda\mathrm{i}:\mathbb{N}$, xn
$(\mathrm{i}+1))=\lim(\lambda\mathrm{i}:\mathbb{N}$, xn i), from sorry,

– – Let $z$ be this limit.

let $z:=\lim(\lambda\mathrm{i}:\mathbb{N}$, xn i),

– – Since $M$ is closed and $x_{n}\in M$ for each $n,z\in M$.

have h18 : $\forall\mathrm{i}:\mathbb{N}$, xn i $\in\mathrm{M}$, from sorry,

have h19 : z $\in$ M, from sorry,

– – Also, $x_{n+1}=\Phi\left(x_{n}\right)$

have h20 : $\forall\mathrm{i}:\mathbb{N}$, xn $(\mathrm{i}+1)=\phi($ xn i),
from sorry,

– – and so (from the definition of limit)

–
$\lim_{n\rightarrow\infty}\Phi\left(x_{n}\right)=\lim_{n\rightarrow\infty}x_{n+1}=z$

have h21 :
$\lim(\lambda\mathrm{i}:\mathbb{N},\phi(\mathrm{xn}\mathrm{i}))=\mathrm{z}$,
from sorry, - Further, for any $n$,

have h22:
$\forall(\mathrm{n}:\mathbb{N}),\|\phi\mathrm{z}-\mathrm{z}\|\leq\mathrm{k}*\|\mathrm{z}-\mathrm{xn}\mathrm{n}\|+\|\phi(\mathrm{xn}\mathrm{n})-\mathrm{z}\|$,
from sorry,

$-\|\Phi(z)-z\|\leq k||z-x_{n}\|+\|\Phi\left(x_{n}\right)-z\|$

– – Since the limit of the right side as $n\rightarrow\infty$ is zero,

have
$\mathrm{h}23:\lim(\lambda(\mathrm{n}:\mathbb{N}),((\mathrm{k}*\|\mathrm{z}-\mathrm{xn}\mathrm{n}\|)+\|\phi(\mathrm{xn}\mathrm{n})-\mathrm{z}\|))=0$,
from sorry,

\- and the left side is independent of $n$, it follows that the left side is
zero for every $n$,

have h24 :
$\forall(\mathrm{n}:\mathbb{N}),(\|\phi\mathrm{z}-\mathrm{z}\|\leq((\mathrm{k}*\|\mathrm{z}-\mathrm{xn}\mathrm{n}\|)+\|\phi(\mathrm{xn}\mathrm{n})-\mathrm{z}\|))$,
from sorry,

have h25:
$\forall(\mathrm{n}:\mathbb{N}),(\|\phi\mathrm{z}-\mathrm{z}\|\leq((\mathrm{k}*\|\mathrm{z}-\mathrm{xn}\mathrm{n}\|)+\|\phi(\mathrm{xn}\mathrm{n})-\mathrm{z}\|))$,
from sorry,

have h26:
$\forall(\mathrm{n}:\mathbb{N}),(\|\phi\mathrm{z}-\mathrm{z}\|\leq(((\mathrm{k}*\|\mathrm{z}-\mathrm{xn}\mathrm{n}\|)+\|\phi(\mathrm{xn}\mathrm{n})-\mathrm{z}\|)-0))$,
from sorry,

have h27 : $\forall(\mathrm{n}:\mathbb{N}),(\|\phi\mathrm{z}-\mathrm{z}\|\leq
0)$, from sorry, have h28 : $\|\phi\mathrm{z}-\mathrm{z}\|=0$, from sorry,

end

####  D.4.6 $\mathbb{R}^{n}$ is paracompact

The formalisation of $\mathbb{R}^{n}$ in the statement by Codex was almost
always inaccurate. The closest it got to defining $\mathbb{R}^{n}$ accurately
was fin n $\to\mathbb{R}$; however, this is not the standard mathlib
implementation.

The proof is a standard (lengthy) forward reasoning proof. On average, proofs
scored 1 due to the difficulty Codex faced in defining the subcover,
repetition and hallucination.

One of the best proofs (score of 3) occurs at temperature 0.4, in the proof
section. In this proof, Codex was able to accurately translate the Latex
expressions for closure and set difference. It got most of the outline
correct, and only missed out on the defined cover being a subcover.