Towards a Mathematics Formalisation Assistant using Large Language Models
Authors: Ayush Agrawal
Siddhartha Gadgil
Navin Goyal
Ashvni Narayanan
Anand Tadipatri
Venue: Submitted to ICLR 2023 (2023)
Keywords: Large Language Models
Mathematics Formalisation

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. 

Under review as a conference paper at ICLR 2023
TOWARDS A MATHEMATICS FORMALISATION ASSIS- TANT USING LARGE LANGUAGE MODELS
Anonymous authors Paper under double-blind review
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 program. It thriving activity today, however formalisation remains cumbersome. 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 the- orem statements. For proofs quantitative analysis is infeasible and 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 new prompting strategy Codex can formalise these proofs in natural language with at least one out of twelve Codex completion being easy repair into a complete proof. This is surprising as essentially no aligned data exists for formalised mathematics, partic- ularly for proofs. These results suggest that large language models are promising avenue towards fully or partially automating formalisation.
INTRODUCTION
Mathematics (definitions, theorems, proofs, remarks) as found in books and papers is written in semi-formal style combining natural language with formal language in specialized notation. We re- fer to the language of this style of writing mathematics as natural language or NI.. Formalisation of mathematics consists of writing mathematics in a formal language that can then checked and ma- nipulated 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. For- malisation is done with the help of proof assistants. A proof assistant consists of formal language in which mathematical statements can be encoded along with a piece of software that assists in writ- ing and checking proofs in the formal language up to the foundational axioms. See under Prompt in Figure [ 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 auto- matically results in much higher degree of confidence in the correctness of proofs. Formalisation promises to open up new possibilities in mathematical exposition, teaching, research and collabo- ration (Massot. 2021 Buzzard 2022); in addition, it can facilitate automated proof discovery, e.g.
(ample et al. 2022).
Formalisation of mathematics today poses barrier to entry because of the need to learn to use proof assistants; it 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 Jattmmilutoa turning a piece of mathematics in natural language into formalised one. An autoformalisation tool that speeds-up formalisation 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. is a natural language understanding problem for the language of mathematics. While the language of mathematics is stylized compared to natural language in

---

Under review as a conference paper at ICLR 2023
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 (02T).
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 for- mal mathematics. Autoformalisation implicitly includes semantic search in the formalised library. Autoformalisation of proofs 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 tacties in formal proofs.
In this paper we worked with Lean, popular proof assistant with two actively used versions: Lean 3) (de Moura et al. 2015) and Lean4 (de Moura Ullrich] (02T]. 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 def- initions 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 form similar to docstrings of mathlib to theorems (in Lean 4), and (2) translating (outlines of) NL proof's Lean proofs (in Lean 3). The latest version of Lean, Lean 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 auteformalisation. 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 significant fraction of undergrad mathemat- ics 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 al., 2022) 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 doc- string close in sentence similarity metric 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-procsssing.
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, larger scale
2

---

Under review as a conference paper at ICLR 2023
study was infeasible.) The theorem statements are 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 much longer than typical theorem statement and we didn't tt 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 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, 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 auto- formalisation. 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.
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 We conclude in Section S
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 pars- ing is the task of translating a natural language utterance into a logical form. Tasks are normally restricted specific domains and the logical forms come from domain-specifie language ranging from first-order logic to regular expressions, e.g. (Kamath & Das 2019 Hahn et al. (022).
Large Language Models and mathematics. The advent of transformer- based large language mod- els (LLMs) for natural languages, e.g. (Devlin et al. 20188] Brown et al. [2020), has brought about a change in natural language processing. This is largely fueled by the remarkable ability of LLMMs to achieve good performance on a diverse set of tasks, ranging from translation to solving math word problems, via few-shot demonstrations 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. -ain 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 unit tests and other metrics.
Specifically, I.LMs applied to code, e.g. (Chen et al., 2021 Fried 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-00) 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 autoformalisationn was coined in Wang et al. (0018), the problem itself has long history; see Wang et al. 22020) Autoformalisation can be thought of semantic
3

---

Under review as a conference paper at ICLR 2023
parsing for the domain of mathematics. Mathematics is far larger and sophisticated domain than most domains considered in semantic parsing.
Wang et al. (020)) applied deep learning-base -based methods to autoformalisation by treating it as lan- guage 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 metries 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 math- ematical competitions (Zheng al., 2022). These problems use only elementary concepts. Their quantitative studies are for fixed few-shot prompts. While 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 fixed-prompi autoformalisation tool for Lean based on Codex.
AUTOFORMALISING THEOREM STATEMENTS
Here we discuss autoformalisation of theorem statements.
3.1 EVALUATION DATASETS
We used three test 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 frag- ments (including names and formulas not in ы5TX 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) areas well- represented by mathlib, such as undergraduate--eve 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 every vecior 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 state- ments 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 ring our third dataset had its (false) converse every ring a field.
3.2 TECHNIQUES
We used Codex 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-pros post-processed completions as described below. Figure I is an example of a prompt, the initial result (with one completion shown) and the result after prot-proessiing We remark that this example needs prompt engineering, as we see Section 3.3
Prompt engineering, Given 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 and keyword matching. 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.
Post processing. Lean 4 code is compiled in two phases: a parser converts a string into a Syntax object, and an elaborator converts Syntax object into a type- expression. The elaboration step is a much stricter analogue of type-checking in a strongly-typed language. It is roughly formal analogue of supplying all the implicit details in an NI. theorem statement. Lean 4 is unique among
4

---

Under review as a conference paper at ICLR 2023
Input text: "If vector space has dimension '2' then it is finite dimensional."
Prompt:
f-- It's vector space has finise basis, then is finite -iimmnsionallll.....
theoren (R: u} (V: v) (division_rsae XI [|add_com__aroup (modaie v. (L:Typo [rintyps seasis Sainsta_cinneee cinencionn
space thooren (8)s Type u} Type vi (divd se ring KI [add__con__gree_e V] (moduis & medicc..rakk X.V tro VJ. V dor VJ, (2: X0. tn
and
single
multiples...
vector space
dimensional. -
theorem
Codex Completion:
(K:Type (V: Type fdivission ri [add comn, group (nodule (J finl du mena lonal
Post-processed code in Lean 4:
() 1 theoren (K: Type (y:type v) linet: DivisleaRing [inst_ AddCommrooup
Module V..
Hodulo.rank X 2 Pinitebineacioaal
Example of a prompt, the initial result and the result after post-processing. Part of the prompt was clided to save space; full prompt appears in Appendix B.I
Figure 1:
proof assistants being implemented Lean and providing an interpreter API, which facilitates implementation.
We parsed the Codex completions, translated from Lean 3 to Lean 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 strong filter.
3.3 RESULTS
We tested the effects of the prompt engineering and post-processing well as the final quality of translations for the datasets described in Section
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
We summarize the number of statements that were elaborated for each of the three sets of statements in [ For each set, we considered results with fixed prompts (those used by Lean Chat) and 4 prompts chosen by sentence similarity. For each of these greedily (i.c., temperature and completion) and those obtained by choosing several completions temperature 0.8 with filtering and selection. We made three runs for each configuration, and the result reported is the median. We also ran configuration with the Codex recommended default temperature 0.2 and with fixed prompts. The results of this 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: particular 23 the 29 statements were elaborated with prompt engineering and selection.
we considered answers chosen
We see in the next section that elaboration is a good proxy measure for accuracy. Thus, we can justify the claims made in
The example Figure | 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 different level of abstraction (e.g., modules versus vector spaces) from that of mathlib. We also that larger number of examples did lead to more sentences being elaborated, but the effect was not strong enough to quantify robustly.
5

---

Under review as a conference paper at ICLR 2023
heorems
Silly Statements
False Statements
Fixed
Input-dependent
Fixed
Input-dependent
Fixed
Input-dependent
Greedy
20 (18)
21
(21)
28
15 (16)
23
Filtered
29
29
24
Table Numbers of elaborated statements; numbers 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
32
30
All wrong
3
Table 2: Correctness of elaborated statements
Correctness of elaboration. Next, we analysed how often completions that were successfully elab- orated were correct. In the case where more than one completion was elaborated, considered both whether the chosen completion was correct and whether any the elaborated completions correct.
For each the three sets, we considered a configuration with high temperature and prompt engineer- ing log-spent speecfiiiilllly
considered the configuration with the highest number of elaborated 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, 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 good proxy measure.
AUTOFORMALISATION OF PROOFS
As discussed in Sec. 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 very rare for the language model to output 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 ProolWiki, university courses etc., of varying proof technique, domain and difficulty level. We carefully checked if similar proof is already formalised in Lean (in mathlib elsewhere on the internet). While in some cases 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 NI 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 in Section C.I
1. Absolute Value Function is Convex cabs_convex): Let f : R. R be the absolute value function on the real numbers. Then f is convex.
2. Schur's Lemma (schur lemma): Let V and W be vector spaces; and let pv and Pw be irreducible representations of on V and W respectively. If and W are not isomorphic, then there nontrivial representations of G on V and W respectively.

---

Under review as a conference paper at ICLR 2023
3. Schur's Inequality (schur ineq): Let z, y. Ryo be positive real numbers such that
x 2223 y 2 2 0, Let R, be a (strictly) positive real number. Then: x'(r - (x y'y 2)(y 2) + 22 x) y)
4. Contraction Mapping theorem (cont (contraction racttacciin an ng): Let B be a Banach space, M closed subset of B, and + mapping from M to M such that for some k E [0, 1), [xx) ( -. kl| yl for any two points I and in M. Then there is unique point
z in M such that (2)
"thoeem"
Power Set Closed under Intersection
Lat SSS be
Ler 5 pooweeset S$ the power set SSS.
ppowenet 'eap jin |powenet S$
"pooff"
Let SA, Vin powerset
definition
(uiisetog (eap (sallwtto AS
(subsesee
Intersection Salset
It follows from Subset Relation is Transilive that SA ycup Vsubbutty SS.
This SA 'eap inn ppoweeet SS and clocare proved. {(ged)
theoren power set F incersect Fan, osed [ set (et.
and
power
aesumm (A set (hik E () o) (bi E P.8).
Then SA 5S and 3D C. S3, power not defiitiion
5)
by tippppyyp set.eusser_st www..enoeeeeeeteeeeeccc hAapp-- wwt__poooass...c.oooooo
2ct.cubsos__
h.).
Then StA m (8 AS, by intersection of net subrer
have h2 (A (13) C A. trom by apply set.inter seaee__sbt_eeeeeeeeee lett.
StA.
88, subset relation tranttivv
trom by {spply set.ebeeet.trae
Elieet))
Hence 11 P SS. power art defnitine
show (t. B) E P S. from (apply pet.men_owwerst n3).
Figure One of the examples in the prompt for the tull-prof-wiithh-ommets format
Proof formats. We experimented with several formal proof formats; all formats use forward rea- soning (see Appendix A for more on forward vs. backward reasoning). Proof formats differ in their ease of translation by language model and in their utility to 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 placeholder for the intermediate proofs. Although an outline contains far less information than 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 detail: each proof step listed along with a list of premises from which it can be deduced. This is done by introducing fictitious new Lean tactic auto that takes as arguments the list of theorems that go into proof along with an optional list of Lean tacties that may be helpful.
Proofs at each level detail can be used as is or combined with comments (each step preceded by a comment explaining that step). This results in total of six formats. For example, see the formal proof Figure 2]
Prompts. We designed few-shot prompts (one for each format) for 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 be found in Section B.
7

---

Under review as a conference paper at ICLR 2023
Hyperparameters. We initially considered four temperatures O, 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, queried Codex with prompt consisting of example natural language proofs and the corresponding step-wise Lean proofs in the appropri- ate format, followed by the natural language proof to be translated. For evaluation, manually inspected the generated outputs via the following grading scheme.
Theorem statement formalisation: O if the output is incorrect; 1 if the output is somewhat correct; 2 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 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 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 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.
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 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 formalise proofs, while the results 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 to 2.
Capabilities shown by Codex. In schur sechu_inee the natural language proof had statements that simply mentioned that all the terms are non non-negative and concluded the proof. Interestingly, Codex completions had these details formalised as intermediate steps.
Codex sometimes expanded definition instead of using the mathlib definition directly; for example, A = AT instead of is_symm A. Codex also generated plausible theorem names, which were line with mathlib style.
Errors in completions. Occasionally the completion had invalid Lean syntax, e.g., x 2 y 2
> (copied directly from the natural proof) instead of the valid Lean syntax 2 y A y >
A 2 > 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 > 0 without introducing t: R.
There were few instances where proof-steps were syntactically correct but mathematically incor- rect, for instance stating ja*x + Bayl ax |x| B+ lyl instead of the triangle inequality.
Sometimes natural language translations statements and valid Lean code. For example, in |schhrrrreeee Temma] Codex confuses a homo- morphism being "non-zero" with homomorphism being "nowhere zero". In proof of the
wrong, although they
mathematically valid
8

---

Under review as a conference paper at ICLR 2023
Cheoren convexx Do Ri Vit a 2 begin
3
assune (x y: R) 3: :3) c. 2
expund the absotune value Function
absutt nonney nonneg (mai) Seft (abo.noneeg
[abs,nonneg X00
appl the mingle lnequality
have h3 alsa (ar 8 als (cx x) abs (P Cxro apply abs_add,
abs
@ abc rcomby
abo_ y) Evact
apply
defenttion
have 55 abs (or x y) alss X B 2lo y. Exem by ix sasssste www.ssss. oonnanc b1.1ofs at E.4.
Ee aos sonneg hi hiLnghtiett
exaet biy
appls the definition of atsolltte value fincciion
have 100::b abs (ar xx= 9) 93 abs 2 abs from by IW abs of nonneg blingh
Figure 3: Correction of Codex completion of Absolute Value Function is Convex. The text high- lighted in red be deleted and the text highlighted in green and underlined is be added.
cont ract ieiiiinnnnnn man_mapping Codex defines a sequence x to be s(1) == (()())), instead of the in- ductive definition: ==(0) := ==0 and w(i + 1) := ((x(1)).
Sometimes the Codex completion contained contradicting proof steps (even in cases not involving proof of contradiction). As example, in generated proof of _emburr__mmmmm___ there were two statements, one stating that the kernel of a homomorphism is trivial, and the next one stating the opposite.
Hallucinations. Codex sometimes output names that looked realistic but are not present in mathlib, e.g. convex fotpe/ffneiiiioooo ion instead of convex_ooo
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.
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 ETEX formulas and of some mathematical idioms. An additional database of prompts targeting these could address this. Further, we can make use of Lean's casily extensible syntax 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 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 complete proofs, can serve good starting point for proof search. This could result an autoformalisation system that is closer to being autonomous.

---

Under review as a conference paper at ICLR 2023
REFERENCES
Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhari- wal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agar- wal, 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 McCan- dlish, 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-Ties Lin (eds.), Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurlPS 2020, December 6-12, 2020, virtual, 2020. URL /RR/ttpss///rrccedinggss newrpisss.
Abstract. html
Kevin Buzzard. What is the point of computers? question for pure mathematicians. In In- ternational Congress of Mathematicians, 2022. URL
11598.pdl pdf
Ricardo Campos, Vitor 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.
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 Bavar- ian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plap- pert, 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, Pe- ter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojeiech Zaremba. Evaluating large language models trained on code. CoRR, abs/2107.03374, 2021. URL htttts://aaxii..oot/
abs/2107.03374
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 Interna- tional Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, vol- ume 12699 of Lecture Notes in Computer Science, pp. 625 Springer, 2021. doi: 10.1007/ 978-3-0300 778-3-030-79876-5) 37. URL https: /oii www. / 1007
37
Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doom, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middel- dorp (eds.), Automated Deduction CADE-25 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in URL
Computer Science pp. 378.388. Springer, 2015. doi: 10.
https::/doi. org/10 1007/978 319 21 6_26
Jacob Devlin, Ming- Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding, 2018. URL https://arxiv.ors
3bs/1810.04807
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 /ttp::/:s//ax
abs/ /204. 05999
Mohan Ganesalingam. The Language of Mathematics A Linguistic and Philosophical Inves- rigation, volume 7805 of Lecture Notes in Computer Science. Springer, 2013. ISBN 978- 3-642-37011-3. doi:
URL
578-3-642-37012-
10

---

Under review as a conference paper at ICLR 2023
Christopher Hahn, Frederik Schmitt, Julia J Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. Formal specifications from natural language. arXiv preprint arXiv:2266.01662, 2022.
Naman Jain, Skanda Vaidyanath, Arun Iyer, Nagarajan Natarajan, Suresh Parthasarathy, Sriram Ra- jamani, and Rahul Sharma. Jigsaw: Large language models meet program synthesis. In Proceed- ings 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: 3510203
10.1145//51000333511222 URL
org/10 1145
Aishwarya Kamath and Rajarshi Das. A survey on semantic parsing. In 1st Conference on Auto- mated Knowledge Base Construction, AKBC 2019, Amherst, MA, USA, May 20-22, 2019, 2019. doi: 10.24432/C5WC7D, URL
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.1 1491, 2022. doi: 10.48550/arxiw.2205.. 22t..22225..1911... URL https://
doi ori.o.g/10. 485.0/.4555/aaa 2tt./5500aa..v222...11111.
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 lan- guage models. NeurIPS 2022, abs/2206. 14858. 2022. doi: 10448550/rXi..2226.668
URL
4855048555iii.0 2206. 14858
Yujia Li, David H. Choi, Junyoung Chung, Nate Kushman, Julian Schritwieser,, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy. Cy- prien de Masson d' dutumm, 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-Ileeel code generation with alphacode. CoRR, abw/2203.008 2022. doi: 10448500axxxv22233.7711.. 0ttp:/111.45555//iii1//// 2203 07814
URL 1ttp://ppp///o....o///0005555///
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 pro- cessing, 2021. URL/https:// http://////wxwwooo//////////////
13586
Patrick Massot. Why formalize mathematics.
2021. URL http::t/////// //www/ imo. seiiversite-parae paree-paaaasaayyyssssssssssaaaaa saclay.clssooo fr/ htt/////msstfiiicom wwwlse/exxxssiion.. /wwtioooo/www//iio....ee. why
Eormalize.pdE
Nils Reimers and Iryna Gurevych. Sentence-bert: Sentence embeddings using siamese bert-
networks. Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, 11 2019. URL httl:tttp//axii.....
1908 10084
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, vol-
ume 12236 of Lecture Notes in Computer Science, pp. 3-20. Springer. 2020. doi: 10.1007/ 378-3-030-53511--.1 URL pattps:///olie wwt.orggl///o 000.0.1077999 3- 3-030-5318---1
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 URL
Computer Science, pp. htttp:://obt orriioorg/aee 1007 -00---3331111911----1-11--------
Springer. 2018. 10. 900-96881222
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.
11

---

Under review as a conference paper at ICLR 2023
Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoe Le, Ed Chi, Sharan Narang, Aakanksha Chowdh- ery, and Denny Zhou, consistnn improves chain thought reasoning in language models, 2022. URLLttts:://artt
abs hbw.//22...1.... 111711
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: /ttpppss//aaxi...oo wttp://ww.w///b///211.1.o. 11903
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models. NewrIPS 2022, abs/2205.12910, 2022. doi: 10.48550/arXiv.2205.. 12100. URL
2205 12910
Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Chris- tian Szegedy. Autoformalization with large language models. NewrIPS 2022, abs/2205. 2022. doi: 10.48550/arxx..2225..22
URL atttp:://ad..orr/o..888838
2205 12615
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: cross-system benchmark for formal olympiad-level mathematics. The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net, 2022. URL
https://cpenzeview net/ forum? ?id= 92Peg FFTFv
12

---

Under review as a conference paper at ICLR 2023
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 is full-fledged programming language with fast runtime in addition to being an interactive theorem prover. This allows a seamless integration of proofs, programs and meta-programs. We use Lean for one set of experiments and Lean for the other because, at the time of writing. mathlib was only partially available in Lean 4 (via partial binary port). Hence we use Lean where its additional capabilities are important and Lean where these are not used and the larger library is of greater value.
Mathematical proofs the literature usually use forward reasoning, where series of conclusions 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 and the induction step. Reasoning starting with goals is called backward reasoning.
In Lean (and similar systems), proof' can use both forward and backward reasoning. However, backward reasoning allows for much more powerful automation within the tactic mode, the cost of readability. Lean has powerful tactics like rw (applies an equation or if and only if statement) and 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 < using only the results Vn E N, 0 n + and Vn, m N, n < m = n < m In Lean these are the theorems Nat zero_ _ot__t____ succc and Nat succ www__uucctttteee lt_succ. Four proofs (in Lean which also work in Lean are shown in Figure
theorem three_1r _t_ seven
< :=
theorem three_it, _t__eveng 3 < :=
have 11 0 < 4 :=
Nat.suce_it, cauucclltssuceeee
Nat.zero_lt_suee
Nat. sauuc_lt_ssuee sut_ slaatsuucc__e wwwssuueee..eeeeeeeeeeeeeeeeeeee suce (Nat.zcro_lt_suee 3)
have 12 : 1 Nat Nat.sscc_lt_succ 11
;=
have 1a : 2 2 6 :=
theorem three_it_seven 3 < i=
Nat.succ_lt_suce 1 pat.succ_lt_sune
by repeat (apply
apply Nat.zero_lt_sune
theorem by decide
3 < :-
Figure 4: Four proofs of < 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 more concise form. The third and fourth proof use backward reasoning in tactic mode. Tactics are powerful algorithms for finding proofs. evident that the above backward proofs more concise and will be easier for However, in practice complex mathematical proof in Lean will have mixed forward and backward reasoning, with forward reasoning taking the form of sequence of lemmas (in the form of have statements) leading to the main theorem and ward reasoning used in the proof of each lemma.
to produce.
13

---

Under review as a conference paper at ICLR 2023
B THEOREM STATEMENT TRANSLATION FURTHER DETAILS
We sketch more details of the various steps in translating sentences.
B. FULL EXAMPLE PROMPT
The full prompt for Figure is in Figure S As mentioned earlier, no completion elaborated when we used fixed prompts.
Input text: "If vector space has dimension '2' then it finite dimensional."
Prompt:
/-- If vector space has finite basis, then is tiite-dimensional..
theorem { Type u} {V: Type v} [division liiggiinnnnnnnnneeeeeee x] codd group v| [module
K vI (c: Type w) [fintype i] (h basis K v): finite winite_dimensioon K
1-- A finite dimensional space is nontrivial it has positive 'finrank'./ theorem {x: Type u} [V:Type v) [division_ ring X] [add_ group V] [module
K v] (h: :0:00 < finite dimensional.finnanl K V): nontrivial
1-- A finite dimensional space that is a subsingletoon has zero 'finrank' theorem {k: Type u} (v: [V:Ty] Type v fdivision_ring X] K vI [h: subsingleton vI wwwitiennnniii htw.teeeddmmmmsiiml.ll...i.e.ee. K =
v| [module
vector space has dimension most vectors are multiples. -/
only if there single vector which
thoorem {x: Typc u} (v: Type v) ldividion_ ring X] [add___cnn_rrouppppp V] [module modulc.rank KV + (vo v). (v v), (r :)) vo
1-- If vector space dimension then is finite dimensional.
theorem
Codex Completion:
{K: Type ut (v: Type v} [division_ring K] cocdd__oom_grouppp v] [module K v] (h :module.rank K = :): finite_dimensional K
Post-processed code in Lean 4:
theorem Type u} (y: v} [inst: wivissonninniii. [inst_1: AddCommGrcup finst_ miiintt2:dddlee Module K v}.
Module.rank K = = PiniteDimensionaal K
Figure 5: Complete prompt used in Figure
B.2 PARSING, TRANSLATION AND AUTO CORRECTION
Given Codex completion, we first (attempted to) parse this and extracted identifiers from the syn- tax. These were translated and auto-corrected before re- re-parsing. The translation step is necessary as the prompt data we had available was Lean 3, as most of the data in GitHub on which Codex is trained. Thus the completions usually use Lean 3/mathlib terminology. Using prebuilt dictionary, we translated the Lean 3/mathlib identifiers to those used by the binary port (binport) of mathlib, with auto-comen cotr-correctin attempted for those that did not have valid translations. Both the dictionary and auto-correction are based on transformations two forms: case transformations (for example camel-case versus snake-case) and dropping adding segments of the form is or has.
14

---

Under review as a conference paper at ICLR 2023
B.3 SELECTION
If more than one completion was correctly elaborated (which is typical when at least one comple- tion is elaborated), we selected the best completion by voting. Namely, first group elaborated completions together into groups whose members can be proved to be equal using a certain tactic. The tactic used one that slightly extends reffexivity (i.e., definitional equality). The chosen answer was the first member of the largest group. In practice, as the present tactic for proving equal- ity is weak, most cases this simply picked the first completion of Codex that was valid (i.e., that elaborated).
B.4 SENTENCE SIMILARITY
We used Sentence-Similarig library (Reimers & Gurevych, 2019) for calculating the sentence em- beddings of the doc-strings. We used fil-mpnet-base-- model, pretrained transformer model finetuned over Billion sentence pairs from multiple datasets This model provided the best quality embeddings among the hosted models on the library the time of writing this paper. We computed the cosine similarity of the sentence-embedding generated from the input docstring with the collec- tion of mathlib docstrings and selected Top-K K similar docstrings based the similarity scores and their corresponding Lean statements for the example prompts.
B.5 KEYWORD-BASHH 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 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 extract the keywords from mathlib and store them in 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.
2018) to
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 L5TpX.
Certain idioms such as "... the intersection of every d 1 of these sets..."
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 ИЛІК formulas and Codex successfully generated translated input text with (similar) complex ВТІК formulas.
15

---

Under review as a conference paper at ICLR 2023
C PROOF TRANSLATION RESULTS AND ANALYSIS
C.I EVALUATION DATASET
The following is the full list of theorems.
1. Absolute Value Function is Convex (abs_convex): Let f IR - IR be the absolute value function on the real numbers. Then f is convex.
2. Symmetric Real Matrices have Real Eigenvalues (symm real mat real nat_rree__eieeeeaaeaeeaaaaaaaaaa eigenvalue): Every real symmetric matrix has real cigenvalues.
3. Schur's 's Lemma [achur_lenna leemaa: Let V and W be vector spaces; and let pv and fw 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. IR" is paracompact (rn (rn_paraccompact)) I is paracompact for all n.
5. Schur's 's Inqquality (schur (schur_inea)) ineq): Let I, y: 2 E Rz0 be positive real numbers such that
x # y 2 0. Lett R,t> 0 be (strictly) positive real number. Then: x' (x-
2) カ 1
x) 2' (=-22=)))) 2=(2 - y) 2 0.
6. Overflow theorem (cverflow) Let F be models of arbitrarily large size. Then F has an infinite model.
of first-order formulas which has finite
7. Density of Irrational Orbit (density: striitttt__r_rrree irr__oritt:: The fractional parts of the integer multiples of an irrational number form a dense subset of the unit interval.
8. Contraction Mapping theorem (contract ract ion mapping): Let be a Banach space, M closed subset of B, and & a mapping from M to M such that for some h E [0. 1),
| ( < k||x yll
for any points and y in M. Then there is unique point in M such that ((2)
9. Class number of a PID) acllassnum___ [p The class number of a number field is
and only if the ring of integers is PID.
10. Bipartite Graph is two colorable
Let G be a graph.
Then G is 2-colorable if and only if G is bipartite.
11. p-adic Units (padic_uniten) coprime to p, then x is unit in the p-adic integers.
Given a prime number p and natural number if x is
12. Nesbilt's Inequality (nesbitt_ines) Let a, b and be positive real numbers.Then
b a a-
a-b
13. Bernoull's Polynomial Evaluation (bernoul 1 Mirooulli_PPo pil_oolyomiaal __eval): Given a natural number n and rational x, let B, (x) denote the n-th Bernoulli polynomial evaluated at x. Then,
B (1 + x) = B,(()) nx
These theorems involve different types of proving techniques such as proof by contradiction, in- duction, 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 theo- rem 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 main findings in the proof autoformalisation experiments. The results of evaluation proof translation are summarised in Figure Out the 288 completions, 22 (i.c., about one in thirteen) were scored 3.
C.2.1 CAPABILITIES SHOWN CODEX
The output proof formats were well structured and Codex was able to break the full proof into its main steps. For example, in bernoullill polynomial eval the natural language proof had two major proof statements in single sentence and Codex broke down into the two relevant pieces. Also, for sschu_urieee
observed that the natural language proof had statements that
16

---

Under review as a conference paper at ICLR 2023
Full
Outline
Premises
3
abs, _onvee
m p_paraccmpact
cass num pid
symm real mat
schur lemma
schur Ineq
density ifr orbit
contraction ma
overflow
padic units
bipartite iff two
For Proofs (Max scores of 0.4 and 0.8)
Figure 6: Max scores of the 11 theorems, for the other 2 theorems we included correct Lean state- ments in the prompt
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 definition instead of using the math- lib definition directly. Interestingly, the precise simplified statement that needed to be proved, possibly taking cues from the natural language proof provided it didn't 't use the convex on definition from mathlib and directly out- putted V (x y R), A (a $ R), a
completion for _onve_c Codex directly outputted
+ abs 3 y) < (a abs x 8 abs y) as the theorem statement to be proved. Also, while formalising the symm real mat real eigenvalue lemma, some completions had the hypothe- sis that A = A 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.
3
x
Codex also utilized contextual mathematical knowledge that was missing in the theorem state- ments but present in natural language proofs. For example, while formalising the proof of symm @ymmmreeal_o @asil_mt__re____e real_eel_____ aasal_eigenn eigenvalue] the statement of the natural language prompt simply said that every real symmetric matrix has real eigenvalues. One Codex completion started with a com- plex eigenvalue, possibly getting the context right from the natural language proof.
We also observed that Codex generated plausible theorem names, which were 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
y > 0 (copying
directly from the natural proof) instead of the correct Lean expression x 2 A y 2 A 2 2 0. There one instance where Codex generated proof format in different language.
In some cases, we observed that the completion used an undeclared variable in the proof. For example, it declared t without introducing R.
There were few instances where proof-steps were mathematically incorrect. For instance, in abs_convex Codex didn't assume and as positive numbers, however used this condition
17

---

Under review as a conference paper at ICLR 2023
in the proof. It also wrongly stated the triangle inequality equality: lasx Bayl 3+ lyl.
There were also instances where natural language translations wrong, although they were math- ematically valid statements and valid Lean code. For example, in Safschhr__eeee Lemma Codex confuses homomorphism being "nonzero" with homomorphism being "nowhere" completions, the definition of "dense" in the the iirr___rr__rri____________
Also, in some
orbit werbitwws was used incorrectly. In a proof
of the contract wetrractttoonaapaeeee mam_mpppigg Codex defines function x be (i) :- 9 (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) = o ix (i
) for 2 1, and might have been difficult for Codex deduce since induction was not explicitly mentioned. In 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 set of have statements. At times, the proof was looped in an inductive fashion. For exam- ple, in rattcoonnaatiimmaapplla
Codex defined y n)
followed by have h1
y (x 1) x O, have h1
(x 2) x 1, and so on.
Sometimes Codex outputted contradicting proof steps (we report cases not involving proof of con- tradiction). an example, in the generated proof of achur lemaa there were two statements, one stating that the kernel is trivial and the next one stating the opposite.
C.2.3 OTHER OBSERVATIONS
Hallucinations. We say that Codex hallucinates if the definition//heerrem 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_ convex_funct function instead convex_on and similar made up defi- nitions/theorem names that looked realistic but 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 included the correct formalised state- ment to Codex for the ja__par pappaaaapapccs. Codex merged different proofs from distinct sources, leading to confticting notation. Also, Codex formalised the contra- pontra-positive version of theorem state- ment of scchrrr 1eruna given in the natural language proof.
18

---

Under review as a conference paper at ICLR 2023
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 shw-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 Unique. For each these theorems, we used the NL theorem statements and proofs in 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.
/- "thhhorrmmm
Power Set is Closed under Intersection
Let $SS be a set.
Let S s'powerset S$ be the power set of SSS.
Then:
$ (forrll A, B \in ppoweerst S: A /epp B \in 'powerset S$
'proof"
Let SA, \in spowerset SS.
Then by the definition of power set, SA \subseteq SS and $B |suhseteq SS. From Intersection is Subset we have that $A ceap B \subseteq A$. It follows from Subset Relation is Transitive that SA (cap \subseteq SS.
Thus $A ceap B \in \powerset S$ closure proved. {qqdd}}
theorem htwpmmppwwrreeeiitttcrcccooooooo ( :V.D: PS
begin
SA8 and SBS are sets. SA$ and SBS belong to power set of SS$
assume (A set a) (hA A E P 9) (B set a) (hB B E P S),
Then SA C S$ and $B C S$ power definition
have h1 (& C
(3 C S), from sorry.
Then S(A n B) AS, by intersection set subset
have h2 (A n 1B) C A, from sorry.
Then S/A n B) SS, by subset relation is transitive
have h3: (A B)
from, sorry,
Hence S(A B) E SS, by power set definition
s show (A B) E P S, from sorry,
end
'theorem' Square of Sum
$ fforrall x, Vin |R: \paren
"proof"
Follows from the distribution of multiplication over addition: { [begin-eqn))
[[eqn | (eft((( + (iihtt)2
r= \lcft((xf + (right) (edot \left((x + y
11
[egn == /edot [efft( y) Arghtt y ccdot (left((x + y rightt
cc Real Multiplication Distributes over Addition
}}
[[eqn] r= \cdot x ccdot + ccdot /cdot
c= Real Multiplication Distributes Addition
11
{(eqn |==2++2X] 2 c==
11 [[end-eqn))
19

---

Under review as a conference paper at ICLR 2023
([ged))
theorem square_of_sune (x))) bogin
expand the power
cale y)2 (x+)) : by sorry
distributive property of multiplication over addition gives:
(x+)) + (x+x)) by sozzy
applying the above property further gives:
... x x x + y by sorry
rearranging the terms using commutativiry and adding gives:
x y
y 2 by sorry,
end
"theoremm
Identity of Group is Unique
Let 5 sttruc {G. (eire $$ a group. Then there is a unique identity element Se /in GS. 'proof"
From Group has Latin Square Property, there exists unique Sx \in GS such that: :Sa b$
and there exists unique Sy \in G$ such that:
:Sy a b$
Setting $b = aS, this becomes: There exists unique Sx iin GS such that:
x a$
and there exists a unique Sy \in G$ such that:
:Sy = These SxS and Sy$ are both $cS, by definition of identity element. [[ged)]
theorem groop_identity_umme
Type*) [group Va:
a
begin
Group has Latin Square Property
have Y b: G, 3 x: G, a bb from sorry, have h2: a b: G, By:.yy =b from sorry,
Setring Sb a8, this becomes: have a E =xaa from sorry,
have h4: Va: Ely: a = from sorry,
These Sx5 and SyS are both 8/1 GJS, by definition of identity element
have h5 Ya:G, classical.soe a) (1: G), from sorry, have h6 a: G, classical.some (h4 a) (1: G), from sorry,
show 3! el :le:G.Va:G.e
fromby (
(I:G),
have h7: b7: (h7 B ===a).
frommby {
assume have t
(b3 a), from sorry,
have claaasicaa...................... (h4 a), from sorry,
show :), from sorry,
).
sorry,
end
20

---

Under review as a conference paper at ICLR 2023
D.1.2 PROOF WITH PREMISES
Following are the example few-shot prompts for the proof outline with premises format.
/-- --hhthhrrem'
Power Set is Closed under Intersection
Let SSS be set.
Let plowerset S$ be the power set of SS$.
Then:
fSrforall (in \powerset S: ccpp \in Apowerset S$
'proof"
Let SA, B \in 'poweeret SS.
Then by the definition of power set, SA !subseteg S$ and $B \subseteg SS.
From Intersection is Subset have that $A 'epp |subseteq AS. follows from Subset Relation Transitive that $A 'cap B |subsetog SS.
Thus SA capp iin spowerset SS and closure is proved.
{{gdd}}
theorem wwwppooee__ee_iteerettioooo
{a: Type*) : (
begin
$AS and SB$ are sets, SA$ and $B$ belong to power set of SS$
assume set a) (hA A S) (3 set a) (hB B S). Then S4 C SS and SB S8, by power set definition
have h1 h 9) A (8 8), from by auto [set.subset_of wtw.uubsetttoommeeepeeeeeeeree
set.subset_of Laaeeett_______________ mem_powersee
Then $(4 r B) C A$, by intersection of set is subset
have h2 (A B) A. from by auto [set.inter subset_
Then S(A B) SS, by subset relation transitive
have h3 (A B) C S, from by auto [set.sbbset.rrass)
Hence S(A n B) P SS, by power set definition
show (AΠ B) E P 5. from by auto [sct.men_
end
/- "theorem'
Square of Sum
: foforal x, y \in |R: \parre xx+))==x2+2xyx>
"proof'
Follows from distribution of multiplication over addition: (begin-cqn))
{{egn = /eeft(fx y) Aright)22
r== (lef((( (rihht) /edot (left((x + y (right)
}}
[[eqn r r= /odot (lef((( + y) (right) + y \edot \left((x + y) rrihtt)
c= Real Multiplication Distributes over Addition
H1
{(egn r= /.doo /edot y +y /cdot x + \edot
c= Real Multiplication Distributes over Addition
[eegn x==x2+2xy
c==
[end-eqn])
theorem square_of_suse (xy::) RR: yx
=x (x)
begin
expand the power
cale (x y) (x+y) by auto [sq]
distributive property of multiplication over addition gives:
xx*x)) + (x(xty) by auto [add_mul]
applying the above property further gives:
= =x*x + x + xxx + y by auto [mul_cee add_mull using [zing]
rearronging the terms using commutativity and adding gives:
x + x x
+ 2 by auto [sq, mul _com]] us ng [ring]
21

---

Under review as a conference paper at ICLR 2023
end
'thcorem"
Identity of Group is Unique
Let St,tuuct {G, (cire]$ be group. Then there is unique identity element Se \in GS.
"proof"
From Group Latin Square Property, there exists unique Sx in such that:
:a = b$
and there exists unique Sy (in G$ such that:
-y
Setting $h aš, this becomes:
There exists a unique Sx iin GS such that:
Sa = aS
and there exists unique Sy /in G$ such that:
:yy a
These SxS and Sy$ are both SeS, by definition identity element.
{{god))
-/
Choorem wwwepggrroppdaeeee wttpopppptttitttyuuuuuuuuu {o: Type*) [group
begin
Group has Latin Square Property
have h1 a.ab: B! x:
b, from by auto using [use -1 b)]. from by auto using [use b * = "1.
have h2 aababaa G.
Setting $b = aS this becomes:
have h3 V a G, 31 G x= a. from by auto [h1], have h4 v a: 3l = from by auto [h2].
These Sx5 and SyS are s(/ G)S, by definition of identity element
have h5 : V G, c assi pasicallsn cal.some (h3 axtsxists =1:G), from by auto [exista_uni que.un qqee, h3, classical.scmss caacc...... _scme_spec, exi sts_unisunnge que.exists,
mul one].
have : a: classical.som (h4 a)exists =1 G), from by auto
(exists unique.unique, h4, classical.scme spec, exists_urrereeeeeee uutttssuuiuuuueiits... one mal]
3l Tale:;,yaaGG.r = = from by auto [h3, h4, wwwsts_ unique.uniqe, classical.some_eeee spec, www.sts_uiqque.oo..... using (use (1: G)],
end
22

---

Under review as a conference paper at ICLR 2023
D.1.3 FULL PROOFS
Following are the example few-shot prompts for the full proof format.
1---theorem
Power Set is Closed under Intersection
Let SSS be set.
Let plowerset S$ be the power set of SS$.
Then:
fSrforall (in \powerset S: ccpp \in Apowerset S$
'proof"
Let SA, B \in 'poweeret SS.
Then by the definition of power set, SA !subseteg S$ and $B \subseteg SS.
From Intersection is Subset have that $A 'epp |subseteq AS. follows from Subset Relation Transitive that $A 'cap B |subsetog SS. Thus SA capp iin spowerset SS and closure is proved.
{{gdd}}
theorem wwwppooee__eetiteerrttiiooooo
(a: Type*) (.:e:.a)
begin
$AS and SB$ are sets, SA$ and $B$ belong to power set of SS$
assume
a) (hA A S) (3 set a) (hB S). Then $4 C SS and SB S8, by power set definition
have h1::::00 C 8) A (8 9), from by {sp1 t
hA,apply
h8),
Then S1A n B) C AS, by intersection of sei is subser
have h2 (A B) A. from by apply
suu_terr__ubst...._e_____ left,
Then S(A B) SS, by subset relation transitive
have h3 (A B) C S, from by (apply set.subset.trans h2 h1.left).
Hence S(A n B) P SS, by power set definition
show (AΠ B) E P 5. from by {apply pct.men_powerset h3),
end
/- "theorem'
Square of Sum
: foforal x, y \in |R: \parre (x+y)2=x2+2xyx=
"proof'
Follows from distribution of multiplication over addition: (begin-cqn))
{{egn = /eeft(fx y) Aright)22
r== (lef((( (rihht) /edot (left((x (right)
}}
[[eqn r r= /odot (lef((( + y) (right) + y \edot \left((x + y) rright)
c= Real Multiplication Distributes over Addition
H1
{(egn r= /.doo /edot y +y /cdot x + \edot
c= Real Multiplication Distributes over Addition
[eegn
x==x2+ 2xy
c==
[end-eqn])
theorem square_of_suse y::::) (42
begin
expand the power
cale (x y) (x+x) by
distributive property of multiplication over addition gives:
xx*x))))++++++ + (yc+tt)+*((**+)))) yx(x+y) by Iw mul
applying the above property further gives:
= x + x*y + xxx y by {zw [mul__comm x (x+y)mul (x+y)), rw
[idd_mml,add_mm. 11, ring.
rearranging the using commutativity and adding gives:
23

---

Under review as a conference paper at ICLR 2023
...=x'2+ 2 y2 (repeat (Ew c- sq). mul comn x, ring)
end
"thhhhhorem
Identity of Group is Unique
Let St,rtrutt {G, {eire)$ be group. Then there unique identity element Se \in GS.
"proof"
From Group has Latin Square Property, there exists a unique Sx /in GS such that: :Sa = b$
and there exists unique Sy iin G$ such that:
:S h$
Setting Sb a&, this becomes: There exists unique Sx i GS such that: :a = aS
and there exists unique Sy (in G$ such that:
:y
These Sx$ and Sy$ are both ScS, by definition identity element.
{{ged}}
theorem wwwpmgrrouuideeee gropppiieentity_mmiiu {G: Type*) [group
a
begin
Group has Latin Square Property
have h1 V b E!x:
from by
assume b G, use a ebviously, }.
have h2 V
:ly: ab from by {
assume b G, use a ebviously, h.
Setting aS. this becomes:
have h3 V G, 31 x G, x from assume a G, h1
have h4 V a G. Rl
a from
h2
-- These Sx5 and SyS are both $(1: G)Š, by definition of identity element have h5 VaaaaaG.. classical.some (h3 a)exiits (1 G), from assume :G,
sulsts_uniquue.niqque (h3 a) sps (mul_one a),
(h3 a)))
have h6 1 a G, classical.some (h4 axxistts ceiists_unique.uiit a a|(classical.some__seee (exists_ utt.isss_niieeexxittttt.. (h4 a)))
from assume a:G.
(one_mul
show Nlowlee:Gyy (1; Ve:
assume aa from by
have 3ares....o...eeccssaccl....... (h3 a)xixsss,, from assume (a G),
hiiita_jmmggceunniggg///3/////11 a)riigh
(classical.commsspee((ssssss wttp:iisstssmmmuuueeiiittttesste (h3 a))),
have h9g. (h4 a)xssss,,, from assume (a G).
exists www.:uu...iuuuuuuuuuuuuu. ahiia) a).left
(classical.some tng. show == (1: G), from eqaaans (h9 c) (h6_).
(h4 a))),
exact (by obviously, h7),
end
D.2 EVALUATION SCORES
The following tables represent the scores given 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 4) (ref. Tables B 13
24

---

Under review as a conference paper at ICLR 2023
In the tables, Full corresponds to full proof, Outline corresponds to proof outline, and Premises corresponds to proof outline with premises. 01, 02 and 03 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 each for temperatures 0.4 and 0.8 respectively.
Format
T=0.4
T=0.8
Max
Format
T=0.4
T=0.8
Max
01
02
03
01
02
03
O1
O2
03
01
02
03
Full
2
1
1
1
Full
2
Outline
2
3
2
3
3
3
Outline
1
Premises
2
1
2
2
1
Premises
1
0
0
0
0
0
1
Max
3
3
Max
Table 3: abs convex
Format
T=0.4
T=0,8
Max
Format
T=0.4
T-0,8
Max
01
02
03
01
02
03
O1
02
03
01
Q2
03
Full
3
3
2
2
Full
2
Outline
3
3
2
1
Outline
2
2
2
Premises
2
2
2
3
2
1
Premises
2
2
2
2
2
2
Max
3
3
Max
Table schur ineq
Format
T=0.4
T=0,8
Max
Format
T=0.4
T=0.8
Max
01
02
03
01
02
03
01
02
03
01
02
03
Full
1
1
0
0
Full
0
Outline
2
3
0
1
Outline
Premises
3
0
0
2
0
Premises
0
0
0
Max
3
2
Max
Table 5:
symm zeal nat real eigenvalue
Format
T=0.4
T=0.8
Max
Format
T=0.4
TE0.8
Max
01
02
03
01
02
03
01
02
03
01
02
03
Full
0
1
0
1
0
Full
0
0
0
Outline
0
Outline
Premises
1
0
1
1
Premises
Max
Max
Table 6: density Sensity_irr_orbrr
Format
T=0.4
T=0,8
Max
Format
T=0.4
T=0.8
Max
01
02
03
01
0
03
01
Q2
03
01
Q2
03
Full
2
3
2
0
2
0
Full
Outline
3
2
0
3
Outline
Premises
2
1
2
Premises
Max
3
3
Max
Table 7: contraction i
25

---

Under review as a conference paper at ICLR 2023
Format
T=0.4
T=0.8
Max
Format
T=0.4
1-0.8
Max
01
02
03
01
02
03
01
02
03
01
02
03
Full
2
2
3
0
Full
Outline
0
2
0
Outline
2
Premises
3
1
0
0
2
Premises
1
Max
3
3
Max
Table 8: Bschr_loome
Format
T=0.4
T=0.8
Max
Format
T=0.4
T=0.8
Max
01
02
03
01
02
03
01
02
03
01
02
03
Full
2
0
0
1
Full
2
Outline
0
0
1
Outline
0
2
2
Premises
0
1
1
2
2
2
Premises
2
0
0
0
0
2
Max
2
3
Max
Table 9:
overtlow
Format
T=0.4
T=0.8
Max
Format
T=0.4
T=0,8
Max
01
02
03
0l
02
03
02
03
O2
03
Full
0
0
1
0
1
0
Full
0
0
0
0
0
1
Outline
0
1
1
0
0
Outline
1
1
0
2
Premises
0
Premises
Max
1
2
Max
Table 10:
class num pidd
Format
T=0.4
T=0.8
Max
Format
T=0.4
T=0.8
Max
01
02
03
01
02
03
01
02
03
01
02
03
Full
3
0
2
1
I
Full
0
0
0
0
0
0
Outline
1
1
2
0
1
Outline
0
0
(
Premises
2
1
2
1
Premises
0
Max
3
2
Max
Table 11:
rn_ papaaccoppccttt
D.3 INTERESTING CODEX PROOF OUTPUTS
This section contains few examples that demonstrate some of Codex's abilities like inventing realistic theorem names and performing algebraic manipulations by analogy, well as the influence of the example prompts on the output.
D.3.1 PROOF OUTPUT WHOSE FOUNDATIONAL CONCEPTS ARE NOT DEFINED MATHLIB
As an experiment, we prompted Codex with a theorem for which the concepts required to state were mathlib. Codex was forced invent its own names for theorems and concepts. and 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 rhombus. The diagonals AC and BD of ABCD bisect each other right angles.
Natural Language proof
By the definition of rhombus, AB AD BC DC.
26

---

Under review as a conference paper at ICLR 2023
Format
T=0.4
T=0.8
Max
Format
T-0.4
T
Max
01
02
03
01
02
03
01
02
03
01
02
03
Full
0
1
2
0
1
Full
0
Outline
0
Outline
Premises
1
1
0
0
Premises
0
0
0
Max
2
Max
Table 12:
bipartite iff two www__ooooaalleooooo
Format
T=0.4
T=0.8
Max
Format
T=0.4
T=0.8
Max
01
02
03
01
02
03
01
02
03
01
02
03
Full
0
1
2
0
0
0
Full
0
2
1
0
2
Outline
1
1
1
0
Outline
2
Premises
2
2
0
Premises
1
Max
2
Max
Table 13:
padic_ units
Format
T=0.4
T=0,8
Max
01
02
03
01
02
O3
Full
0
1
Outline
1
3
2
0
3
Premises
1
0
Max
Table 14:
nesbi tt it__tiin ing
(Corrctt Lean theorem statement included in the prompt)
Format
T=0.4
T=0,8
Max
01
02
03
01
02
03
Full
1
1
1
0
2
Outline
0
3
Premises
1
2
2
Max
3
Table 15:
bernoulli poa.onliiipplyyommmiammmmmm (Correct Lean theorem statement included in the
prompt)
Format
T=0.4
T=0.8
Max
01
02
03
01
02
O3
Full
1
1
0
0
Outline
0
1
2
Premises
2
0
0
2
Max
2
Table 16: #n paracompact (Correct Lean theorem statement included in the prompt)
Format
T=0.4
T=0.8
Max
01
02
03
01
02
03
Full
0
1
1
Outline
1
0
1
1
2
Premises
0
2
1
2
2
Max
Table 17: overflow (Correct Lean theorem statement included in the prompt)
Without loss of generality, consider the diagonal BD.
Thus:
27

---

Under review as a conference paper at ICLR 2023
Format
T=0.4
0
Max
01
02
03
01
02
03
Full
0
1
2
2
Outline
2
Premises
1
2
1
2
Max
2
2
Table 18:
orbit
(Correct Lean theorem statement included in the prompt)
AABD is an isosceles triangle whose apex is A and whose base is BD.
By Diagonals of Rhombus Bisect Angles, AC bisects ZBAD.
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 and Figure 8
Output 1
theorem
(ABCD
rhombus):
V BD E diagonals ABCD, AC.bisett BD BD.bisects AC AC.perpenoicular
:0
begin
assume (AC segment) (hAC: A diagonale ABCD) (BD segment) (hBD: E
diagonals ABCD),
have :A = AD A AB = A AB DC, from sorry,
have V iscaceles laareeeees_triiinllleeeeeee A C, from sorry,
have _.osselcss_trianglee D, from sorry,
have ww..ssccs BAD, from sorry,
have : :Cb.iscctssss BD, from sorry.
have AC:perpendiculle BD, from sorry,
show ACbisects BD BDbbisecs AC AC.errpendicular cular BD, from sorry, end
Figure 7: Codex generates ABCD type "rhombus" that is not present in mathlib. It also gener- ates 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.
D.3.2 EFFECT 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 In case, included the theorem square of sum in the few shot prompts and in the other case we did not. In both these cases, we provided the NL proof of Cube of sum using Binomial Theorem. We observe that, the first case, Codex directly took 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:
(a .) = 8 3u2y + 3ry 3
Natural language proof:
Follows directly from the Binomial Theorem:
28

---

Under review as a conference paper at ICLR 2023
Complation 2:
theorem of ____o__rror_____bb_e____________ beeet_eechhottheeeeeeee htgg (A B C
D D:point nt (h_ rhrrhomuus: i is_rhombus A H.C. n):
bisects (segment.mk A C) (segment.mk D) A bisects (segment.mk B D)
(segment.nkk C)
begin
By the definition of rhombus, SAB AD BC DCS.
have [B__e__A__and__________
(segment.mk A B segment.mk A D) A (segment.mk C= segmentt..k D from sorry.
WLOG, consider the diagonal SBDS.
have BD_e $D_eg_DC: segment.mk B = segment.nk D C, from sorry,
Thus: Striangl ABD$ is an isosceles triangle whose apex SAS and whose base is SBDS.
have iscsceles_trrange
__DD is ss_ssocceeessss ststtcelessttrrnnlglooo A from sorry. By Diagonals of Rhombus Bisect Angles, SACS bisects 5 angle BAD
have AC Dc_bisectts BAD bisects (segment .kk A C) (angle.mk A D), from sorzy, From Bisector of Apex of Isosceles Triangle also Bisects Base, SAC$ bisects $BD$. have AC_bi sectassecs,, eesect__Htte __h:: bi sect (segment.mg .mk A C) (segment.mg B D), from sorry, From Bisector of Apex of Isosceles Triangle is Perpendicular to Base, SAC8 bisects SBDS at
right angles.
have AC bisects ED
right angles bisects at right rightt_tggeeeeeeeeeeee (segment.nk A C) (segment.mk B D), from sorry,
Hence the result.
show bisects (sogment.mk (segment.mk D) bisects (segment.mk B D) (segment.nk A C), from sorry,
end
Figure 8: Codex "suggested" designing line segment as structure segment and treated point type, for defining 4 vertices.
Completion 1 (including "Square of Sum" in few shot prompts):
theorem cube_of_aum (x 3 + begin
cale (dl sorry
:y sorzy
-222:22222222233211222222222233 sorry
x y y y sorry
sorry
... + 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.
Vn E Zzo : (a + y)t
11 Σ 0
x"
k
putting = 3. Q.E.D.
Codex outputs for the cases shown in Figure 9 and Figure 10 respectively.
29

---

Under review as a conference paper at ICLR 2023
Complation (not including "Square of Sum" in few shot prompta): theorem cube_of_aum
y
begin
assume (x R)
have: (x y)3 k in 3
k)) from sorry,
have: (x+ choose 0) chooss x3 1) +)*y'++
choose 2) x'(3 -
",, from sorry,
y33,
have: (x+ xx3 x33"" + y"3, from sorry, y2+y33, from
have: (x++))=x3+3**2*
from sorry,
show (x+
+'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 instead of choose 2.
D.3.3 SIMPLE ALGEBRAIC MANIPULATIONS
We experimented with Codex's 's ability perform algebraic manipulations by analogy. With 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 4th, 8th, ..16th power of sum. We observed that for the 4th power and Sth power of the term (x y), algebraic manipulations and final results were accurate, however, from 16th power onwards, Codex outputted partial expressions and some of these terms were incorrect. We provided the following prompt to Codex:
--- --httooorom
Euclid's Theorem
For any [Deéinnition:Fintt, Set Set finite set]] of [[Definition:Priin Number/prine numbers] there exists a [[Definition:Prime Number/prime number]] not in that [eeefirrtioon:Se:ssset]]]]] 'prooi"
Let 9\mathbb P$ be a IIDetinition:Finite Set set/finite set of I [iDefinition:Prinn Nunber|prime numbers]].
Consider the number:
:Sdiisplasstyle n_p \paren (pprod[(p Amathop Ain Amathbb P) p) + 1s
Take any $p_1 \in \mathbb p$.
We have that:
shdisplaystyle p_j \divides \prod_ \mathop Vin \rathbb P) p$
Hence:
:Syiisplaystyle texists q Vin \z; \prod Amathop Vin Amathbb P) p
q P_$$
So:
[(begin-eqn)) [(egn
1 n_p
p_j
c [IDivision Thecrem]
1)
[(een
11 Aleadsto
1 n_P
C Aperp
r P-j
c [(Defof Coprime Integers))
}}
[[end-eqn))
so $p_j \nmid p_p$.
There are two possisilities:
(1) Aquad p_p$ is B [[Definition:Primm Number/prine ), which is not
in Smathbb P$.
(2): Aquad p_p$
[[Definitionn:omplll Number corposite]].
30

---

Under review as a conference paper at ICLR 2023
But from [[Positive Integer Greater than has Prime Divisor]], it must be divisible by " some'' prime.
That means it is divisible by prime which is not in &mmathbb Ps. so, in cither case, there cxists at least one [DDefinition:Prime Nunber/prime]] which is not in the original set 8'mathbb P$ we created.
[{ged])
-/
(p N prime pl plinninite
begin
assume (primes : tp prime p).finite), primes,
let :- tos.fiiiieetoffiie
1, have hprime div div_prod V p_j P, p_j F.val.pros from sorry, have prime div_ sorry,
let :- P.val.
V P_i E.P,P q, P.val.pros p.j g, from
have prime_not_div
A p_j E P, ( np), from sorry, P. primo p D F. from sorry,
have prime_not_in__ show false, by rcases prime_not_in_1 with (p, hprime prime P. hnot_in_ P : P $ P), have p E P, by (apply foimstt_finntttnne exact hprime, ) contradiction,
enc
/--'theoren'
Power Set is Closed under Intersection
Let $3$ be [DDefinition:Set set]].
Let S\powerset S$ be the (obererition:Power power set]] of sss.
Then:
fS\forall A, B Vin \powerset S: A Acap B Vin \powerset s$ "proof"
Let $A, в Vin \powerset s$.
Then by the definition of [[Definition Set power set]], $A Asubseteq s$ and $B \subseteq s$.
From [[Intersection is Subset]] we have that SA \eap \subseteg AS. It follows from [[Subset Relation is Transitive]] that $A Acap B Nsubseteq $$.
Thus $A \cap Ain \powerset and [[eerinition:Clouure (Abstract Algebra) [closure]] proved. ((ged))
-/
(a Type*) set a) A
s, (A P s
begin
assume (A set a) (hA : A E 8) (B : set a) (hB : B B P S)
have (A 5) (B C S), from sorry,
have (A
A, from sorry,
have (A n BJ C S, from sorry.
show (A n B) E p S, from sorry,
enc
/-- ttherrem" Square of Sum
:frforall x, y Vin AR: \paren (x + y)" = x + 2 22
'proof'
Follows from [[Real Multiplication Distributes distribution of miltiplication over addition]]: [(begin-cqn))
Addition the
((egn 1 = \left (1x + y) //rrgght) "2
r \left ([x \right)) Nodot \ieft ((x Aright))
})
(feen I r x \edot Aleft ((x y)rrghh)) \odot (1eft( Wiiiggt))
c [|Real Multiplication Distributes over Addition
11
31

---

Under review as a conference paper at ICLR 2023
(een
Vedot x Aedot y y Aodot y Acdot c [[Real Multiplication Distributes over Addition]]
}}
[(ogn
r = x + 2xy y
c
})
[(end-eqn)}
([gea))
-/
square_ of sum (x y R) (x y) " (x'2 2+x+y 22))
begin
cale (x y) '2 (x+y) * (xty) : by sorry
- x (x+y) + (++x) : by scrry
= x4x x*y + yox y*y by sorry
x 2*x*y y by scrry,
end
--- 'theorem'
4th power of Sum
Codex output shown in Figure
D.4 THEOREM-WISE ANALYSIS
D.4.1 ABSOLUTE VALUE FUNCTION CONVEX
The maximum score awarded was the full proof and proof outline formats. An accurate state- ment was generated for the full proof format. Overall, the proof structures seemed useful.
Most of the outputs from Codex resembled the natural language proof great extent. Inter- estingly, 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 it use the convex_on definition from mathlib and directly outputted y (x y R), (a
A 3 > + abs (a x 8 y) S (a abs x B 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 't find this theorem formalised online.
[R,
A & 8
There were instances where 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.
steps were mathematically incorrect, such as treating the triangle
The best format (full proof) was observed at temperature 0.4 (please refer Figure 3) correct Lean statement not included in the prompt. We also show another good format (proof outline) at temperature 0.4.
Also, the
Theorem statement:
Let f R -
be the absolute value function on the real numbers. Then f is convex.
Natural language proof:
Let x, E R.
Let a, B E Rzo where B 1.
f(ax By)
laxx + Byl
Definition of f Triangle Inequality for Real Numbers Absolute Value of Product Definition of Absolute Value Definition of f
< |azel + |8yl
|ai||ar| + |,81vv]
=a/z] + Blyl
= + B
Hence the result by definition of convex real function.
32

---

Under review as a conference paper at ICLR 2023
:ororalll x, y Vin AR: Aparen 4)14 x x y+6 x
y22 + x y"3 +y"4s
'proof'
Follows from [[Square of Sum] [ibegin-egn|
Heen 1 (1x \/igghh)) "4
r ([x W/riggh) 2 Aedot Aleft ((x +
"/righh))2 22
}}
[[eqn \left (1x"2 2xy 2 (right)) Aodot \left ((x22
2xy + (r2ggrigh))
c [[Square of Sum]]
}}
Heen
4 4x + 2x 4xy"3 4
cc=
11 [(end-egn]] ([ged))
-/
fourth power_ sum
sum (x y [] : (x y) (x"4 + 4xx"3xy
2+x"2 2 + 4xxxy"3 3 + y == begin
cale (x 4)
+)) 22 (x 2) by sorry
(x"2 2+xxy + 222) (x 2+xxy 2 by sorry
...
= x 4*x + 6+x 2+x 4 + 4 by sorry,
end
/--otheorem'
8th power of Sun
:$\forall x, y Vin AR: \paren ix yl = xx88 x7 y+28 x-6
y"2 + 56 x y33 + x 4 + 56 x y 28 x 6-6 8
y"7 y
'proof'
Pollows from [[4th power of sum]l: [(begin-ecn]]
[eeq 1 (1x + \right)) "8
1 (1eft Whigghh) "4 Aedot \left ((x
W/riight> 1)
Hegg r = Aleft(1x*) + 4x + 2x + 4xy + Aright)))) \left ((x + 4x"3y 6x 4xy"3 Arighthhh
Aodot
1 c [[4th power of Sum]]
1)
Heeg I r = x'8 + 8x + 28x "6"2 + 56x" 70x" 36 28x 2 8xy 7 + c
}) [end-egnn] ([ged))
-/
eighth_power__e power_os____...oo.eeeeoo_..oe.oe sum (x y R) 7) (x"8 8-x"7ay
28*x 6xy 2 + 56*x 5xy"3 70*x"4*2 + 56xx"3xy 28*x"2xy"
B*xxy 7 8) := begin
cale (x "8"8-
"4
y) by sorry
... (x"4
3+y 6xx"2xy
4+xxy"3 4) * (x"4 +
3+y 6*x 2+y 4xxxy"3 + 4) : by sorry
= x + 84x 7 + 28xx"6xy"2
5xyx3 + 70
56"x"3xy + 28xx 8xxxy"7 + y"8 by sorry.
end
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 poyer onwards, Codex outputted partial expressions and some of these terms were incorrect.
Figure 11:

---

Under review as a conference paper at ICLR 2023
Q.E.D.
Codex Output with Corrections:
theorem abs_convex convex_on abs R (dset univ R) abs
begin
split,
assume 1x y (R) (ax x set. univ) (ay y E set,
(a B []] (ha 0 (c) (h3 : 03 B) (hag a 3 1),
show
a+ X 3 E set. univ), irom dec.trivial,
-- Let $x, Vin \RS.
assume y R) (hx
unt.) (hy y univ),
Let flalpha, Ibeta Vin \R_ 015 where Slalpha + (beta = 16. assume (a $ R) (hl a 2 0) (h2 B 2 0) (h3 : a + 8 1),
expand the function cale abs (a*x 8xy) abs (a*x 8zy) by sorry refl
triangle inequality for real numbers gives:
S abs (a*x) + abs (8xy) : by sorry fapply abs add -- absolute value of product gives:
abs abs rw [abs_mul x, abs_muul]]
abs 8 abs y by sorry
absolute value real number gives: a abs x 8 abs y by sorry expand the function ... abs rabs_of_nonne, hl ofs_.of_nonneg h2]]
y
sorry
hence the result by definition convex real function
S a * abs x + * abs : 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 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 '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 expressions were found.
Major sources of less scores were outputs getting stuck some steps and few instances of hallu- cinations. For this theorem, there were no mathematical errors observed.
We show the full proof format 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 E Rz0 be positive real numbers such that 2 0.
Let t E R, 0 be (strictly) positive real number.
Then:
x' - y) 2) s'Vv 2)(2 +)) (1==)2===-->)))))(()0001)00))1)) -oe 20
Natural language proof:
34

---

Under review as a conference paper at ICLR 2023
Consider the expression:
(a - yx= - ()) v - 2)) + 2 - 2) - 2)
We see that every term in the above is non-negative. So, directly:
1: (ar (x 2) v'(y =]) >'(x =) 2)
1 can be rearranged to Schur's inequality.
Q.E.D.
Codex Output with Corrections:
thoorem schur_
simpler {x y 2
t R] (hx : x 2 0) (hy
: y 2 0) (hz : z
0) tbxy : x 2 y) (hyz
: y
2 2)
(ht : t > 0)
t (x - y) (x z) y' (y 2) (y
x)
z't (2 x)
(z y) 2
begin
Consider the expression:
have h1 (x - y) (x"t (x 2) - ytt (y 2)) zt (x 2)
(y - z) 2 0, from by
Nefe see that every term in the above is non-negative. So,
directly:
have h2 (x y) 2 0, from by (zw
ge.itf_le at *, rw sub nob_nnnneg, exact hxyl,
have h3 (x"t (x z) y't (y 2)] 2 0, from by {
have h4 (x 2) 2 0, from by (rw
ge.iff_le at rw sub Lub_nonnegy exact \hIr(hx)),) ge.trans hxy hyz),
have h5 : (y 2) 2 0, from by (rw
ge iff at *, rw sub_nonneg, exact hyz),
have h6 (x"t (x - 2) yt ly - 2)) = (x"t y"t) (x
+ yt (x y), from by ring,
have h7 (x"t t)t 2 0, from by [rw subnnnnngg, exact
pow_ e_pow hx
ht ge iff 1 at 8, rw sub nonneg, TW real rpow l rpow iff by ht
have h8 : (x 0) > U, from by {ew + sub sub nonneg, exact ht, assumptii mompttoon
hxy
have h9 (x"t t) (x 2) 2 from by (apply mul nonneg,
exact h7, exact h4),
have h10 : y't (x - y) 2 0,
from by (apply mul_nonneg, exact powlnonned
ge.iff.le
have 1 0 t, linarith,
have h.2 t + linarith,
have h.3 (0: IR) (0: R) linarith,
have h.4 := real. rpow le.r_le_rpox h_3 hy ht, exact h8), h_1, EW real, zero.rpow h.2 at h.4, assumpt ion, linarith, /
have hll (x't - t"t) (x 2) y't (x y) 0, from by (apply add nonneg, exact h9, exact h10),
show (x"t (x 2) - y't (y 2)] 2 0, from by (ew h6, exact h1l,,
b
have h12 (x 2) 2 0, from by (rw
ge le 8, s, sub_nonneg, exact bx), ge trans bxy hyz
have h13 (y 2) Z 0, from by (zw
ge-lff_le at *, rw sub nobnnon exact hyz),
have h14 2"t * (apply mul nonneg, exact pow.nonneg apply mul.ncnneg,
(x z) (y 2) > 0, from by
ge iff Te 8,
35

---

Under review as a conference paper at ICLR 2023
have h.1 0 linarith,
have + 0, linarith,
have h.3 (0: R) (0:R). linarith,
ht, exact h12, exact h13), ww real zero_rpow h.2 at h_4, assumption, linarith, linarith, b
have h :- real. rpow le rpow
have h15 (x - y) (x"t * (x 2) y ly 2)) + z't (X
2) * 2) 0, from by (apply add nonneg,
apply mul_ncnneg,
exact h2, exact h3,
exact h141, show y) (x't (x y't (y 2)) z't
(y z) 2 0, from by (exact h15),
((1) can be rearranged to Schur's inequality.
have h16 (x y) (x't (x - 2) - y
(y - z)) z"t (x z)
(y
x't (x y) -x 2) y
ly x) z
(z x) (z y), from by zing,
show x x (x y) (x - 2) y't ty - 2) (y
x) + z22 (2
x) (2 y) 2 0, from by frw - h16, exact h1),
end
D.4.3 NESBITT'S INEQUALITY
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 per- taining to inequalities and simple algebraic manipulations, and getting stuck at trivial steps. Since the natural language proof followed backward reasoning pattern, 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 't find this theorem formalised online
Theorem statement:
Let a, and be positive real numbers.
Then:
+ b 3 2
b b a a a a
Natural language proof:
+ b + atb 2
bic
atc
+ atbte +
atdie + atbte >
by adding 3
bic atc
+ atbte + atc bic
atoie + atbtc 2
9(atb+c) (o+)))
atb+c
as (b (b+c) + (a+b)
dividing by 3(a + b bb
(b=o)
1
These are the arithmetic mean and the harmonic mean of b a c
and
a a
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.
36

---

Under review as a conference paper at ICLR 2023
Codex Outuu
theorem deabitt_inequalie < <) (a / (b + c)) - (b / (a c)) + (c (a =b) 2 (3 / 2) :-
{a c : Bj (ha 0 (hb : < b) (he 0
begin
-- S\drrac a (b + cJ + Adfrac b la + cl Idfrac
e la + bl$
have h1 (a (b + e)) (b / (a + e)) (c / (a b)) (3 2),
from sorry,
adding $3$
have h2 (a / (b + c)) + (b / (a + c)) + (c / (a + b)) + 3 2 (3 / 2) +
3, from serry,
as $ldfrac (a +
c) (pparen (b c) + ppren + c) Aparen fa
+ =b } = Idfrac
25
have h3 : (a / (b + c))
+ (b (b/ (a + c)) + (c / (a + b)) + 3 2 (9 * (a
b + c)) / ((b + c) (a c) + (a + b)), from sorry,
dividing by $3 lparen
b
have h4 : ((a (bbb/bb/ (b c) + + (a c)] + (c
b)) 3) x
(a + b + c)) 2 ((9 ( c)) ((b + c)
(a c) + (a b))) /
x3* (a +bb + +)), from sorry,
Slofrac (ifrac 1 (b + c] Ifrac [a c + \frac 1 {a b) } 38
have hs (ta / (b + +))
(b (a e)] + (e /
b)) + 31 (3
b c)) 2 (1 / (b +)+ +1/ ta c) +1 (a + b)) 3, from
sorry,
-- Sidfrac 3 ('paren {b + c) + lparen (a + c] + \paren (a + b) 35
have h6 ((a / (b + c)) + (b (a c)) + (c / (a b)) + 3) / (3 +a+ b c)) / ((b + c) + (a c) (a + b)), from scrry,
These are the arithmetic mean and the harmonic mean of Sidfrac {b + c)$, $ldfrac 1 fa + ci$ and $ldfrac 1 fa + big.
From Arithmetic Mean is Never Less than Harmonic Mean the last inequality is true.
have h7 : (a / (b + c)) (b / (a e)) + (c / (a b)) + 3) (3 *
(a + b + c)) 2 3 / ((b + c) + (a + c) (a + b)), from scrry, -- Thus Nesbitt's Inequalian lity holds.
show (a / (b c)) + (b (a c)) (c / (a + b)) 2 (3 / 2), from sorry,
end
D.4.4 OVERELOW THEOREM
The Overflow theorem is standard application of the Compactness theorem from first-order logic. While the proof is fairly short and easy for human to comprehend, there are number of difficulties in translating the informal natural language proof to formal one:
1. Phrases such as "arbitrarily large" are difficult for the model to directly cast into symbolic notation such Vn E N, 3m N, m > = ....
2. Expressions that make use of informal mathematical notation such as ... are difficult for the model to make precise.
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, 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 set of first-order formulas which has finite models of arbitrarily large size.
Then F has an infinite model.
Natural language proof:
37

---

Under review as a conference paper at ICLR 2023
For each let A, be the formula:
Br,3r2 ... Ar, : { # 22 A D1 * 23 .... xn-1 # xn
Then A, true structure À iff À has least n elements.
Take:
3
T UAA A
Since F has models of arbitrarily large size, every finite subset of I is satisfiable.
From the Compactness Theorem, I' is satisfiable in some model M.
But since M |= A, for each i, M must be infinite.
So F has an infinite model.
Q.F.D.
Codex Outpur (Full proof, Temperature 0.8)
theorem overflow_theoree (F : set FOL) finite_models + infinite_model begin
Assume $Fş has finite models of arbitrarily large size
assume h1 finite_models F,
-- Let $F$ be set of first-order formulas which has finite models of arbitrarily large size.
assume h2
n, m : model, E F card m 2 n), -- Then $F$ has an infinite model.
have h3 infinite_model F, from begin
define ilmttbb A_n$
let A_n := (x_l, x_2, x_1 # x_2),
mlmathbe A_i$ is true in a structure $\AAS iff $1AAS has at least $n$ elements. have h4 by assume i,
assume m model,
assume hm : m E P F A card m 2 i,
have h5 right hm,
have h6 := classical.some (h2 i),
have h7 m C card m 2 a 4> card m F, from by split, assume h, from h, assume h, from land.left hm, by frw [t not_le), exact ht),, have h8 h6. right h7,
have h9 and. by simp, assume h, use (m), split, from and.left hm, from set. set.siigglton_suubett _ hr have h10 h9 lefd h6), have hll classical. somea..ssommeeee spec h10, exact hl1. left,
+ 3 A, A & from
b,
Take: $$ (Gamma :- F. loup \bigcup_ (1 \mathop - 1) 1]aiinfy Ali ss let r :- F U (Union A_n),
Since $F$ has models of arbitrarily large size, every finite subset of GiGammas is satisfiable.
have h5 finite_models sfisete_subset С), from begin
every finite subset of $F$ is satisfiable. have h6 finite_models (finite_subset F), from by apply Liniite_oddel__fnitee....
By 'finite
F),
-- So consider a finite subset $X$ of $ assume X set FOl,
assume hx : P finite X,
38

---

have h14 := h12 h13, -- So $F$ has finite models. exact h14, end, Under review as a conference paper at ICLR 2023
Notice that if SX$ contains finitely many of 1mmttbf A ns,, then ex$ has model.
have h7 finite (x n A from by {
apply finite, wiiiiiiiintterrrr.eeeeeiiiiieeee inter (nat + sot FOL) fett FOL A_n)
(sst.coontable_fiinte
(X A_n)), b,
have h8 finite_models (X U (X n A_n),, from by
apply sasre_models__mme
split, exact h6 (X n F), exact h7, h Hence: 4$x lcup \ieft (X leap vbigeup_ /1 lmathop = 2/ lintty
A 1 A
By distributivity of union over union, have that:
-- $8x lcup lleft (X leap \bigeup_ (1 \mathop 1) linffyyy
A Airrgght
-- $$= X (eup Wlfft (bbigeup /1 kmathop = 1) linfit (1eft \cap
A Arlggihh) (right)
mniit_mmoeels (X U (Union A : N, X A from by apply finite_meet tette_moddls_unioe X,
have h9
-- Neverthhless, we have that:
have h10 (X n An) Union (X n A_)) A.n, from
begin
apply set. set.eequuioon_ee apply set.
intro i, apply set.disjjint_leff,,
right_ cettttoooottttttoeeeeeee not_men men FCL X),
have h: : A A, from h.right have hll :- h. h.right
exact (h10 i) right (and. right h11),
b enc,
$$X lepp (left (bbigeup_fs /1 Imathop 13 Vinfty \left (X lepp A Arlgighh) (right) $5 -- So this is just sxs. have h11 h9 X,
We know that $XS has model, since sxs contains finitely many of $\mathbf A_n$. have h12 finite_models x, from by (apply subset_union_righ x, exact h10. symm, exact hill. and.leff hx,
have h13
From the Compactness Theorem, $ $\Gammas is satisfiable some model (Mm)
have h6 := cowpactness_
tatrssemehermmmmm I h5, But since $ flmathdf (M) \models A for each $is, $ (M)5 infinite.
have h7 := by
assume 1,
have h8 and. right h6,
have h9 and. right h8, A_i, have hll :- by {
have h10
have h12 := mem upp h10,
have h13 = right h12,
have h14 := right h13,
have = h4 i,
have h16 = hi5.left,
have h17 = h16
have h18 = right h17,
exact h18,
},
have h12 i= set wot__ott_ppyyy iff exists__issmssee hll,
have h13 h12, have h14 classical spec h13,
39

---

Under review as a conference paper at ICLR 2023
have h15 set. countable finite my
have h16 card_le_of_subae h15.left h14. h14.left,
have h17 : h15.right h16,
have h18 : nat nat. 1,
exact h17 (nat.succ_pos i),
}
So $Fş has an infinite model.
exact h7,
end,
Hence $F$ nas 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 few instances represent a Banach space, however Codex hallucinated and used banach.space instead. Both full proofs and proof oulines performed well. The best score was an example of which shown below (the proof is the same as the one generated by Codex, we used ETTxXinttead of Unicode due to erroneous display of certain Unicode characters). While this theorem similar theorem in mathlib, the proofs are very different: the mathlib proof assumes the existence of Cauchy sequence, while ours constructs the Cauchy sequence.
This proof was bit challenging. It required Codex to use induction both implicitly and explicitly, and to appropriately translate the ... notation. Codex was somewhat successful in the former, however mostly failed with the latter. A marked improvement in performance 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 closed subset of B, and & mapping from M to M such that for some & E [0, 1),
[ - +(v)ll S k|[ yll
Natural language proof:
for any two points and in M. Then there is a unique point in M such that ((2) = z. Choose some To in M. Define a sequence {a;} by setting li+1 (a:),, for E N. Then for any n,
Fnn = xp + (x) xo) + (x2 - x1) + ... + (xin xn-1)
Also, for 221
|0 xill S ||: 1.1.
and by induction we easily show that
| x:ll S |||| xoll
Because [k| < 1 ks converges, which implies that E || - x; converges. By the Weirerstrass M test, 2i=1 (I:+1 vx) converges in B, and hence limm Vn exists. Let be this limit. Since M is closed and Hn E M for each n, = E M. Also, Fn-1 = (I.).. and so (from the definition of limit)
lim (Ix) lim In+1 = Z 2-000
n=+00
40

---

Under review as a conference paper at ICLR 2023
Further, for any n,
[ =|| (1)
② (.n) 2| I || Fna || + 2 (I,) - z||
4 (xx)
Since the limit of the right side as n - oo is zero, and the left side is independent of n, it follows that the left side is zero for every n, and so is fixed point for Tb
To prove uniqueness, suppose that there are two fixed points, say and y. Then
= = I. f(y)
and so
x- y [f(x)- f(y)) S k/2 yl where 0 < 1. This is only possible if y
Q.F.D
Following one of the best scored outputs (proof outline, temperature 0.8, score 3).
Codex Output
theorem contraction mapping (B Type** [banach space B]
(M : set B) fis closed ( M + M)
(h1 Vxy E M, ||xx Φyyl s k ([[x yll)
(hk: k < <)):
Blz M, oz 2:
begin
choose some 2o in M. choose (x0:B) hxO using M.nonempty,
Define sequence {2i} by setting #+41 = (z:), for E N.
let xn An N, x1xx,
Then for any n,
-I, 2g + (2) mo) + (x'2 11) + + (xn In-1)
have h3: Vn : N. xn x0 + (xl x0) + (x2 x1) + + (xnn - xnn(n 1)), from sorry,
Also, for i
- -||0:+1 zıll S k||=; [ xi-1ll have h4: A(i: N)( hi: i), [[xn[i 1)- xnil| < k ||xni xn(i 1)]], from sorry,
-nd by induction we easily show that
- ||æ041 - =xal $ kl[[2s æoll
have h5 v(i : ( hi : 1 $ i), [|xm(i + 1) - xnil| S (k A) * ||xm] - xnO], from sorry,
Because k| 1, Σm k converges,
have h6 : abs k < from sorry,
have h7 tendsto (Xi N, k^i) at_top (N1), from sorry,
have h7 tendsto (Xi N, (k i) [[xm1 xnOll) top (N[[]]n] xnol))), from sorry, have h8:
tendsto (Ai: : N, [ix + 1) xn []) at_top ([)xm=-x00]) xn0l)), from sorry,
which implies that Σ | æ2|/ converges.
have h9 : tendsto (Xi N, Σj < i, [|xn(j + 1) xnjil) at top (N iE, ||xm(i + 1) - xmill)). from sorry.
41

---

Under review as a conference paper at ICLR 2023
-- By the Weirerstrass M test, Ei=1 (I++1 zz) converges in B, have h10: Σi, | +
xnil| < oo, from sorry,
have h1l tendsto (Ai: (i S i, + xnj)) at-p (W ( ii + xni)), from sorry,
and hence nim Zn exists.
have h12 Ei xn (i+ 1) xni = xml - xn0 + Ei > 0. xn (i + 1) xni, from sorry,
have h13 lim Ai N. xn (i +1+ xmi) = 0, from sonry, have h14 lim (Ai N. Eisi,
xn 11+1) xni) = Li xn (1) xni, from sorry. have h15 : (Am NJ S i, xn
G+ 1)) lim (Ai: J i,xj) lim (Xi: N, ( xn(j +1) xnj) ), from sorry,
have h16 : (im N, Σj < i, xn (j + 1)) = lim N, Σj & i, i,x)) from sorry, have h17 limm(i: N, xn (i (i+ 1)) lim N, xn i), from sorry,
-eLet 2 be this limit.
let lim Ai N. xn i),
-- Since M closed and Fn E M for each n, 2 E M.
have h18 Vi N. xn mie E M, from sorry,
have h19: z E M, from sorry,
Also, Tn+1 4 (Ix))
have h20 vi: N, xn + 1) = o( xn i), from sorry,
-- and so (from the definition of limit)
-im + (xr)) = lim -im #n++1 =
have h21 lim(Ai: N, ((xni) = 2, from sorry, Further, for any
have h22: v(n N), |løz z|| S * ||z xnn|| + [|x(xnn) - z|I. from sorry,
(2) = S k||2 - -2,11 + 1 (Ix)) 2||
Since the limit of the right side as n + oc zero,
have h23 lim (A(n N), ((k= * ||z xmnll) + (lo(xmn) zl)) = 0, from sorry, and the left side is independent of n, it follows that the left side is zero for every n,
have h24 V(n N), (loz z|l S ((k || - xnn|]) + [[((xmn) - =4])), from sorry,
have h25: V(n: : N), (lløz z/l Σ ((k ||z [|zz-xni) xmn]l) [|ő(xnn) =2])), from sorry,
have h26: V(n: : N), (lløz - z|l Σ (((k * ||z xnn|]) + [lø(xnn) - -zl) - 0)), from sorry,
have h27 : V(n N), (l0z z|| 0), from sorry, have h28 ||şo z|| 0. from sorry,
end
D.4.6 RR IS PARACOMPACT
The formalisation of R" in the statement by Codex was almost always inaccurate. The closest got to defining R= accurately was fin n E;; however, this is not the standard mathlib implemen- tation.
The proof is standard (lengthy) forward reasoning proof. On average, proofs scored 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 the defined cover being subcover.
42

---

Under review as a conference paper at ICLR 2023
This theorem does not exist eemma in mathlib, however, it might exist instance. This is not a case of contamination, since the proofs are very different the one in mathlib is dependent on properties of emetric', space,
space, while proof is an explicit construction.
We also gave the correct Lean statement to Codex and evaluated its proof output. Overall the per- formance was worse than before. Codex exchanged norm with absolute value, and had shorter outline than before.
Theorem statement:
IR is paracompact for all n.
Natural language proof:
Let A an open covering of R".
We now construct locally finite open refinement C of A that covers R". First, define collection of pen balls. Let Bo = o, and for each n E N. let Bm denote the ball radius m centered at O.
Given m, set Bm is compact in In by the Heine-Borel theorem, choose finitely many elements of A that cover Bn, and intersect each one with the open set R \ Bm--1- and let Cm denote this collection of open sets (each open subset of an element of A). So C U C. is open refinement A.
Note that C covers R" since for any R", there is smallest E N such that B,, (namely, some m where ||= S m [||=]|++1), and so x is an element of Cm-
Now collection C is locally finite since for given many elements of C, namely those elements collection Cj U C2 .... Cm- So C is locally finite open refinement A that covers R", hence R² paracompact.
IR" neighhorhood B,, intersects only finitely
Q.E.D.
Codex Output The following is the best scored proof:
theorem on cn_paracompact [n: N} paracompact (R'n):=
begin
Let S (athcal(A) be open covering of $ (mmathbb(RR 's.
assume A: set (set (I"r.)),
assume hA : _is_open_covee A,
We now construct a locally finite open refinement Smmthhaal C)S of mathhhal that covers $ "mathbb([]] 'nS.
First, define collection of pen balls.
Let $B.0 \phiS, and for each iin \mathb (N}S, let SB.n$ denote the bull of radius SmS centered at 0.
1et B: B:N sct (I = m, ball m
1et B0: set (K"n) 0,
have hB0
from rfl.
have N. Bm m, from by (assume m m:N, rf1],
Given SmS, set SiBar(B_m S is compact in (mmthbb((R) 'nS by the feine-Bored theorem, have hBm v V N, is__opa (clesure (B m)), from by {
assume n: N.
zW h2,
apply caspacctattc.../ closure.
apply is_compact_bal,,
so choose finitely many elements (ammahhal(AA that cover SyBarr Baar[Bmm) B.m) and intersect each one with the open set S mathbbbR) R)"" "ssemmiuu Barr B_rr[_((m mm- 1)}s,
have h1 V m : N, Cm set (set (R'n)), finite Cm A (Uo Cm) = (closure (B m)) (set.compl
(closure (B (m 1))) from by {
N,
have h2: Cm set (set (R'n),, finite Cm A (Uo Cm) = closure (B m), fromby zw h2,
apply hA,
apply hRm,
43

---

Under review as a conference paper at ICLR 2023
have h3: Cm: set (set (R'n)), finite Cm A (Uo Cm) set.compl (closure (B 1)))
from by
have h4 A Bm: set (R'n), 1s_open (set.compl Bm), from by {
assume Bm : set (R'n),
apply is_opennccmpppeeeeeeeeeeeee compl,
apply laloyis_openne haepoii___oss__eeeee
apply is_open_ballle }.
zw hB,
apply hA,
apply h4,
use Cm (1 (set.cooml (closure (3 (m I))),
split.
apply finite.inter,
applyy h2.left,
apply h3.left,
2W ww.set.inter_comp__sso
ewh2.right, rwh3.right,
2w "wset.ccmml_compl
rwhR zw set.comp1_compl.
h20,
zw set.inter_empeee
rw set.union_empptyy
and 8 (C) denote this collection of open sets (each open subset of element of $ \mmathca(AASS).
let C:N- set (set (R')) m,, classical.some (h1 m)xxisss,
have hC : m : N, C m= classical.som (h1 m).exists, from by (assume m N, rfl),
have hCm V m: N, finite (C,), from by {
assume m:: N. zw hc,
apply (cl (classion cal .some_apec (h1 1)ex }.
have hCm2 V N, (Uo (C) = (c' osure (8)) n (set.compl (closure (8 (m 1)))), from by assume N, zw hc,
apply (slassical.some.e...... spec (h1 m)xxists)...tttttt
So 8mmaahcaa(( (iigcup_ (N (mathea((C)mmb is open refinement of \mathcal{A]S..
let C_union: set (set (R²r:) (C (range (nat.succ))), have hC_union: : c_ f_union = Up (C (range (nat.succ))), from rfl,
have hC__nion2 V m: N, C m e C_union, from by {
assume M,
zw hC_union,
apply use
iff,
split,
apply nat.mem_range
nw hc,
zw www.etmmem_innee image of men,
zw wwnattsucc__et ____d____a__ one, nwt.aaddd_com comm,
have hC_ hC__nion3:_. V.:. assumo m: M.
from by {
assume c: set (R'n),
he: TN hC,
zw set.mem bunionnnnnnnn iff at he, reases he with (r.bm,hc). set.mem. image_oc
44

---

Under review as a conference paper at ICLR 2023
rcases he with (A.mm2,to).
use
split,
zw hm., apply hA, he,
apply set.inter__ubset__
have "iC_union:1
3A A. a C A, from by {
set (RRn), assume CLunion,
nw hC_union at hc, nw aet.mem_bunnon_ifff. he,
reases he with (r.,mm,ho). he,
zw set.mem aatmmee__maae___eeee reases he with (cm,hm2,hec.
eww hC at he,
www www.seeettbteeeeeeeee ieweennnnnionniiiiicmomo at he,
reases he with (m.2.h33.hc).
ew hm2 hm3,
have hm4 m m m2, from nat.egg_of_aucc__e__.o. hm3, ww hm4 at hc, zw set.mem image of men at he,
rcases he with (A.hm5,te).
use
split,
ew hm5,
apply hA, he,
apply gett.inter_subst____e
}.
have hC_union5: tts__ooo__reffineenee c_union A, fromby {
apply is open_ref_nnment.inte
apply hc_union4,
apply hC_union3,
Note that S mathcal { C)S covers $ matthb [R] 'nS since for any 8x Vin \mathbb R3-
end -NNedds more than 2000 tokens
D.4.7 SYMMETRIC REAL MATRICES HAVE REAL EIGENVALUES
The formalisation of the statements scored I and 0 on average. Proof outlines and proof with premises did the best. Codex could deduce that the eigenvalues must be complex-valued, to be- gin with. could also deduce the definitions of symmetric matrices and eigenvalues. However, had trouble formalising the statement in mathlib style, probably since eigenvalues are defined in more generality for endomorphisms, instead matrices. There were also some hallucinations.
The proof is mostly calculation based. Codex created good outline, and could deduce the correct meaning of (complex conjugate). Sometimes there were repetitions and irrelevant statements. For example, statements such have h1 v 0 and have h2 tively at times. Codex was also unable to ascribe the correct type to expressions of different kinds appearing in the same statement for R and b C, Codex would output either bo (incor- rect) or a b.
appear consecu-
(correct but would require additional changes further) instead of (a C)
This theorem uncontaminated as far as we know the theorem statement might exist in mathlib in different and generalized manner, however, the particular statement and proof given to Codex does not exist in mathlib.
Theorem statement:
Every real symmetric matrix has real eigenvalues.
Natural language proof:
45

---

Under review as a conference paper at ICLR 2023
bi is complex number, its complex conjugate is defined = bi. We have 28 = (a + bi) (a bi) = a² + b², , so 2 is always a nonnegative real number (and equals 0 only when 2 = 0 It is also true that if w, 2 complex numbers, then we 102.
Recall that if
With this mind, suppose that À is a (possibly complex) eigenvalue the real symmetric matrix A. Thus there is nonzero vector v, also with complex entries, such that Av Av. By taking the complex conjugate of both sides, and noting that A = A since A has real entries, we get Av
Av = AV = Av. Then, using that A
A.
v Av (Av) = ((V-v)
V Av (Av) (TV)* Ā(V.
Since O, we have V v #0. 0. Thus X A, which means À E E
Q.E.D
Codex Ouiput
Following one of the best scored outputs (proof with premises, temperature 0.4):
Codex Output
haveeee_aaveeeeeeeeeeeeeeeeeeeee genveaaaa ues: A matriix R n, symmetric + V. ss_ a_eigenva Tue A ia_rea begin
theorem real
Suppose that $ Jambdaa is (possibly complex) eigenvalue of the real symmetric matrix SAS.
(A matrix R (hA symmetric A) (A: C) (h): is eigenva lue A).
Thus there a nonzero vector mathh/(()) also with complex entries, such that SA \mathbf(v)= /ambbaa mmathbf(v]..
lambda
have h1 (v: matriim C 1), v
from by auto [hA],
By taking the complex conjugate both sides, and noting that S (.bar(A =AS since SA$ has real entries, get Svvvrrlnee (A \mathhf(v) = laambdda (mathbf(v] (v}} (Rightarrow A
"overline (\mathbf([]] =>bbr(( .lambda) \overline mathhf(v) (vrhhb((v)) v
have h2 v (v:mattrs C 1), v - = A. A (v.con :) A.conj (v.con j), from begin
Suppose that Sv$ is nonzero vector with complex entries, and SA \mathbf(y) = Alambdaa {mathb((v]S.
assume (v matrix n 1) (hv v * 0) =
By taking the complex conjugate of both sides, and noting that 8 (ba((A]=AA since SAS has real
entries, we get overlinee \mathhb(vv }= =\overlieee (nverline(llamblle lammbaa \mathbf(v) |Rightarrow A
"nveriin((/mathh(((f (mathb((v)) =\bur(' (abbbb((aaaaa (lambda) Noverline (mathhf(v) have h4 vv.conj A.conj. v.conj, from
\overline
begin
-- ovverlnee [mathbf(v))= Mambda [nathbf(v]} RRigharrow A
lambaa))))
lambdd) \overline \mathbf(v)
have : v.conj -.co... from by auto [hA, h3, conj_mul_comm
[onj_ee__o__e__cor_l wt__e__onnnl_ooooooeooeee mul_comm]
show A v.conj X.conj v.conj. from h5, end,
show A (v.conj) A.cojj (v.conj), from h4, end.
Then, using that SA (7)(S)=AS.
have h5: (v: mamaarii C 1), v 0 - A v Xconj, from begin
Suppose that Sv$ is nonzero vector with complex entries, and SA mmahhbfv))<\anble maathbf(v3..
assume (v (v:matris matrix C n 1) (hv A
Then, using that SA =AS.
have h7 A from begin
SA $A==A)AA$
have h8 :...ransppese =A from by auto [hA, symmetric_teanspose
$A17)=AS
have Atranapeeee A, from by auto [hA, symmetri
46

---

Under review as a conference paper at ICLR 2023
(T) (aaatbbff///xvvvriiinn ( (nathbftv)) (7H))aaaaian (wnurhbbfl)))=/mmmmdba overlliee (nmathbft
S\overline (onrr/iie((mmmh((((r)))))))) A
Addtt (mathbf(r>)
have h10 (V.con * v == (v.co v, from by auto [h6,
mul
_a__assscc mu__emm)
S,,oerline (ymathine ((7) \mathbf( [(A (
mmathbf[r) bark (lambda) \overline (arthhf()) ([7)
mm /ark Jaabdaa H (vvrrline mathh/ {v}} Acdor (mathbf(v)]5
have h11 (v.con))...aaaspoos
A (A.conj v.conj).tzanspore * v, from by auto
[19, h2, 16, mui assoc].
Since 8mmathb((v] \neq \mathbf(0)s (0)8, have overline (m /odor \mathbf(y) \neq
0S. Thus (ammbda=/bar (aaaadaaaaaaaaaaaaa
(ammdda S., which means S Ilaabbda \in (mathb((R)
have h12 A= j. from by out Ihv, h10, h 111, mul mul_left_inj].
show À j. from h12.
end.
show A.conj, from h7, end,
Thus Salaamda Vin \mathbf( R)SS show is_real X, from by auto [h1, h5], end
D.4.8 CLASS NUMBER OF A PID
The formalisation of the statement got average score of O. Proof with premises performed the best. The statement was relatively easy to formalise. The only problem occuring sometimes was that Codex could not identify that PID stands for principal ideal domain.
The proof is relatively short and majorly based on unfolding of definitions. Codex deduced that the statement has an if and only if implementation and hence split it. It got the outline of the proof right frequently, which could easily be completed to a full proof.
While this theorem is present in mathlib, the NL proof provided to Codex very different from the proof in mathlib, and is minimally contaminated.
Theorem statement:
The class number of a number field is if and only if the ring of integers is a PID.
Natural language proof:
Let R be the ring of integers corresponding to K. If R is PID, then, by definition, the class group is trivial, hence it has class number 1.
Conversely, has class number 1 ,all ideals of are principal, hence R PID.
Q.E.D
Codex Output
Following is the best scored output (proof with premises, temperature 0.8)
Codex Output
theorem class fllas_nnubberr one itt pid (K: Type*) [discrete fieidX]:
number k= ++ is pid (xing of integers K) ==
begin
-- Let SRS be the ring of integers corresponding SKS.
assume cing_of_inteseeeeeeeeeeeeenennee
K,
If SRS a PID, then, by definition, the
class group is trivial, hence it has class number $1 S have h1 : hR,
show is is_pid hR, from by auto [is_pid],
have h2 class_number 1
show class_number from by auto [cl [class_number_of_00
47

---

Under review as a conference paper at ICLR 2023
show class_number k= hegga/uunnet...lllaaaaaadccoooo.
K), from by auto [h1, h2).
Conversely, if SRS has class number 1, all ideals of SRS are principal, hence SRS is PID .
have h3 class ass_uurberbrrrrre ==
show class class_number K 1, from by auto [class_numbers
have ae is is_pprsccpppps....ee 1acl____ea__ ideal hR,
show is is_priiiiiaal_ieeeeeee h8, from by auto [class_numbr__priniipplll
have :5:1s:: :isissppde hR,
show is pid hR, from by auto [is_pid].
show class_number == = + is_pid 11.. K), from by auto [h3, h5).
end
D.4.9 EVALUATION OF BERNOULLI POLYNOMIALS
For this lemma, Codex was given the correct statement, and had to work out the proof. However, did not perform very well. While demonstrates an understanding of types, seems have problem with translating the LateX formulac for (K). We also noticed that it applied strong induc- tion, as was needed, sometimes faltered. The proof also had bit of backward style element,
which it easily managed to convert into forward style. On average, it scored with better scores at temperature 0.8.
This theorem is not present in mathlib, and is uncontaminated.
Theorem statement:
Given natural number n and rational v, let (x) denote the n-th Bernoulli polynomial evaluated x. Then,
Ba x) Bx)x) + nx"
Natural language proof:
We apply strong induction on n. So, for all m < d, we have By (1 x)) = Bm( + mm and we want to show that
Ba + x) Ba(x) + d=
Multiplying both sides by + 1, and using the fact that, for all E N. Ek=o (x (1 1)x (where B₁ is the k-th Bernoulli number), get that
(d+1)
(d + 1)(1 2)aa (d 1)2
la 1-
The conclusion then follows easily.
Q.E.D
Codex Output
Following is the best scored output (proof outline, temperature 0.8)
Codex Output
theoreebberoulll_evall _ee__oo_________________ee add (n NN) Q
[polynomiaL.eernoulll n)eval (1 + x)= (polyyommi wtw.lyyromal..rroullllll.. n)ve x+n x"(n 1)
begin
We apply strong induction on SnS. So, for all 8m <, dS, we have
assume h1 (V' N. m 5,
48

---

Under review as a conference paper at ICLR 2023
(eoLynomial..eemoollll mee
m).eval (
(ttpa//oooooooooilaaaaaaaaaaaaaa m). *x'mm
D))
we want to show that
show www.yyynnia....r.nuol
n)oval (I-xX/=ooolyooooaaaaerroooollll n)vval x * x'(n
1), from begin
need to use the equation:
sum [1 0) ((k) [k+ / \choose 1) =.I +) X3$
have h2 : (V k N. polynomial.c ((k 1)) x
polynomial.sum (List.range (k + +))
(A IN). (poLynomial.C (((k + choose 1) (poLynomial.berroull 1))) * x"1)), from
sorry,
Multiplying both sides by Sd + 1S, and using the fact that, for all S1 Vin (mathb((N)S, (kmmm (1) {1 I \choooe k) B B ([+ X we get that
have h3 (polyyomial.. ((n 1)) (polynomial.C 1 xxvvaalx
(pelynomial.C ((n 1)) evaleval x
polynomial.sum (List.raig (n +1)
(A (1 : N), (polynomial.C (((n + 1) choose 1))) (polynomial. "x"(1 - 1)))
.eval x, from scrry,
The conclusion then follows easily. show (ed] ynomi al be bbernoul1 1i n).eval (1 x) (pol ynomia wwrmmial.bberooo bernoull n).eval x x
(' 1), from serry, end.
end
D.4.10 THE FRACTIONAL PARTS OF THE INTEGER MULTIPLES OF AN IRRATIONAL NUMBER FORM A DENSE SUBSET OF THE UNIT INTERVAL
This theorem proved to be partieularly difficult for Codex to formalise. The basic constructions the proof and statement such as the set of fractional parts of integer multiples of an irrational number were common stumbling blocks.
The first part the proof involving showing that the fractional parts of distinct multiples of an irrational number distinct a fact that can be succintly stated and proved in conventional math- ematical notation but can be quite long when expanded out in full. Some of the full proofs often ran of tokens before reaching the rest of the proof. However, full proofs were still better overall in this case. The performance in both temperatures was comparable.
Another common error in the definitions of limit points and dense sets.
We also experimented with adding a correct statement and an extra example prompt from a related area (the Sandwich theorem). Both modifications resulted in improvement, suggesting that input- dependent prompting can improve results of proof autoformalisation as well (though presently not feasible).
One of the better proof outputs (given below) was an outline at temperature 0.4. (for formatting reasons, 3: is rendered 1).
Theorem statement:
The fractional parts of the integer multiples of irrational number form dense subset of the unit interval
Natural language proof: Let a be an irrational number. Then for distinct i,j e E, we must have {ia} # {ja]. If this were not true, then
ia | = { = {ja} = ja - [ja],
lix lixl-Lja- E Q Hence,
which yields the false statement
S = {[ia} e 2}
an infinite subset of [0, 1).
49

---

Under review as a conference paper at ICLR 2023
By the Bolzano-Weierstrae Weierstrass theorem, S has a limit point in [o. 1]. One can thus find pairs of elements of S that are arbitrarily close. Since (the absolute value of) the difference of any two elements of S is also an element of S, it follows that 0 is a limit point of S.
To show that S is dense in [0, 1], consider y E [0, 1). and > 0. Then by selecting æ E S such that {x) < (which exists as 0 is limit point), and N such that N {x) S y < (N + 1) {x), we get:
y - {NaHl <. Q.E.D.
Codex Output
theorem irrational orbit density (a : R) (h1 : n is rational a) dense_set Ir Bi:: Σ, = i+al i=
begin
-Leet $lappha be an irrational number. Then for distinct $i, J lin \mathbb(Z)s, we must have $\11 \alphal) \negl(j salphal/5.
--If this were not true, then $1 talpha-tlfloor 1 \alphalrfloor \alphal/=\/1 \alphalj=j \alpha-\ifloor 3 yields the false statement $halphael.free @alphalrfloor-1211
which
j
(i-}} \in \mathbb(0)5.
have h2 : a + 1*a := sorry,
have h3 V (1 j 2), i + i+a * j+a, from sorry,
have h4 V (1 j 2), i i
(i+a j+a), from sorry,
Hence
let 8 :- (r | a (1 : Z), r- i
C [r | 3 (i : Z), = ixal, from subset.rett 8, have h6 S ir 3 (i Z), r isal, from set. sut.subset... antisymm h5 h5,
have h5 : S
Consider $y (in[0,1]s, and Stepsilon>0S. Then by selecting $x Vin ss such that s1exi/<eep (which exists as $0$ is a limit
point), and SN$ such that SN (odot1 Vleq y< (N+1) \odot (x)
get: $1y-\(N xili<lepsilonS.
have h7 : V ly : R) (E), y E Ice + E 0 + 3 x x A (N Z
) tN* (x - x) Syyys < ((++1) - x) A NNx (x x) y E, from sorzy,
$5$ has a limit point in $10, 119.
have h8 : A (y : R), y E icc 0 + 3 (x : R), x XESA dist x 6, from sorry,
One can thus find pairs of elements of $S$ that are arbitrarily close.
have h9 : V (u R), yy, y E s A dist u S dist u y, from sorry,
have h10 V (y : R) (E), y E Icc 0 + te>t + 3 x E A dist x < <,, from sorry,
Since (the absolute value of) the difference of any two elements of $5$ is also an element of $s8, it follows that 80$ is a limit point of Sss.
have hil A y : R), x x
3 x', x' EESS (a Σ) set.range (A (n Zi, ia Σ),, n* (x y) x', from sorry,
E A AESAyES
have h12 V (y R) (e), y E Ice 0 - ee>0 + + x E S dist x < from sorry,
By the Bolzano-weierstrass theorem, $S$ has limit point in $10, 118. have h13 V (y R), E Ice 1 + (x R), x x A dist x <
from sorry,
have h14 V (y R) (8), y Ice 0 E,, from sorry,
X A dist x y
-- It follows that $0$ is a limit point of $5$. have h15 A (y R) (8), y lea 0 8
3 x EESA A dist x y
< E, from sorry,
50

---

Under review as a conference paper at ICLR 2023
sorry,
end
D.4.11 SCHUR'S LEMMA
The formalised statement was reasonably accurate in most cases, usually missing only few minor details. In some cases, the original statement and are not isomorphic, then there are no nontrivial representations of G V and W respectively was translated in the contrapositive as (f : -> R) (hé + 0) V n.
Some common emrors were using commutative groups instead of groups, getting the notion of representation wrong, and adding several extra assumptions.
Another common mistake that occurred in the statement as well as proofs was spelling out certain definitions such as G-equivariant maps and the kernel of homomorphism - in more detail than needed.
The proof itself is a fairly easy one that follows directly from the observation that the kernel and image of module homomorphism are themselves sub-modules of the domain and codomain spectively. Consequently, the model has done a fairly good job with formalising this theorem frequently getting score of 3 the proofs. The proof variants with comments often better structured than their undocumented counterparts.
Schur's lemma is stated in mathlib, though at extremely high level of generality, so chances of contamination from this are minimal. However, we found a standalone Lean repository containing proof of Schur's lemma, which is possible source of contamination. We believe that since the proof is spread across multiple files and is built on definitions introduced within the repository, direct copying of the proof is unlikely.
Theorem statement:
Let V and W be vector spaces; and pV and pw be irreducible representations of G V and W respectively. If V and W are not isomorphic, then there are no nontrivial representations of G on V and W respectively.
Natural language proof:
Suppose f is a nonzero G-linear map from V to W. We will prove that V and W are isomorphic. Let V be the kernel, null space, of in V. the subspace of all in V for which fz 0. (It is easy to check that this is subspace.) By the assumption that f is G-linear, for every in G and choice of in V'. (ev (g)) (z)) = (g) (f()) = (pw (g)) (0)
But saying that f (pv (z)( is the same as saying that pv pv (x) is in the null space of f V + W. So V is stable under the action of G: it is subrepresentation. Since by assumption V is irreducible, V' must be zero; so is injective.
By an identical argument we will show f also surjective; since ((vv (x))
(Pw())) (f(z)), we can conclude that for arbitrary choice of f(x) in the image of f. PW (g) sends f(x) somewhere else in the image of f: in particular it sends it to the image of (g)g)). So the image of f(z) is subspace W' of W stable under the action of G, so is subrepresentation and f must be zero or surjective. By assumption it is not zero, so it is surjective, in which case is an isomorphism.
Q.E.D.
Codex Output
theorem schurs_ _emma [G Type+} (V W Type*) [group G] [add_comm
V] [add_ Bal___comm__o__eeee W] [vector_space C v] [vector_sppe pppce C Wi [nodule C
[module C G W] [irreducible V] [irreducible [C] f
(f
begin
-- Suppose $1$ is nonzero $G$ fcs-linear map from $V$ to sMs We will prove that $VS and SwS are isomrrpicc. assume hl 0,
51

---

Under review as a conference paper at ICLR 2023
have hla f * 0, from show f * O,, from by auto [b1, zero_ smul] using [linear_map wat.aap.aapaaro..._
have hib f + 0, from show f * 0, from by auto [h1, smul_zero] using cataar__aaamappee....
Let SVn (primem subspace of all $xš $V9 for which $f x=0$. (It is easy to check that this is subspace.)
the kernel, null space, of $58 in sVs, the
let V' : set V := ker f, have h2 V S V, from by auto
map www.pappppeeuueeeeeeee
By the assumption that $E$ is sGS-linear, for every $g$ in SGS and choice of sx$ in $V ('rrmm)))),
flieft (\left (Arho_ V(g) (right) (x) (right)= (Arho W(g) \right) (f (\rbo_ (g) \right (g x) = 0, from by auto
have h3 V g : G, V x [linear_map,nn meraap.mmm..ee ker] using [linear_man sattarr_aaaaap_saaae
E V
have h4 : V g : G, A x : V, x E V + (g x) = 0, from by auto [h3] using [Linear_map.map_ii
But saying that sflleft (Arho_ Vig) (x) (right) is the same saying that $irho_V(g) (x) is in the null space of $f: \rightarrov ws.
have h5 V ggg G, x v, E W using [iinear map. map_mmapllll linear map
E v from by auto Ih3, map.map. map_ zerol,
5o (Vriiie is stable under the action of $68; it is a subrepresentation.
have h6 subrepresentation V V', from subrepresentation.nts mk! (h5 ),
have h7 : is subsouudeeee G V' v, from is js_submodule..t (h5 : _,,
-- Since by assumption SV$ is irreducible, $V (prrime) must be zero; so $1$ is injective.
have h8 : irredueible G ' + V (linear_map. ker f), from by auto (frreducible.irrr_ee. irrleiirrr_ee_ee,_ hia, h1b] using wweer__ap.maa_aa00..
have h9 : irreducibll 6 (V') + (V*) (0), from by auto
hla, hib, h8, 1inear_map. wea.mpppee_e___err using [1inesr_map.mp__err]ll..
[irredacible.
have h10 irreducible (V') 7 (V") (0), from by auto [h9, h6,
irreducible Baapecibee_ubbeppeeettttttoooo
have h11 irreducible G (V') (V") = (0), from by auto [h10,
srreciiiblesuubrppreeeett
have h12
0, from by auto [h11],
By an identical argument we will show $5$ is also surjectivey have h13 linear_map range f C W, from by auto [1inear_map. wwwarrannnnett..reeerre
have h14 linear aamner__mp.rrae range S W, from by auto [h13, wtw.perrrrre__eee__eeeet
have h15 V G, V V, x linear_map www.aaa.a.a........ f + g x E 1anear_map. f, from by auto [1inear_map. mem_range, using (1inear_map.map__e_
have h16 subrepresentation G W (linear_map. range f), from subxepresentationn.nk (h15 : :>,,
have h17 is submodule G (linear camtear_mpp..e range f) W, from is su_sumdddule..t (h15 :),
since $
flleft (Nleft (thho_(gg) \right) (x) \right)=)left (1r ((g) \right) (f s, we can conclude that for arbitrary choice of $f $ in the image of $ f, \rg)_ sends (x somewhere else in the image of $f; in particular it sends it to the image of $1rho_ (g) x$.
have h18 : V ggg G, Vv vv: : V, v E linear_maan paparr_map.. range f + V
linear_ saai__aap.ree range E, from by auto [linear map mem_range, linear map. sampmmppsuuu.. smul] using [linear maaear_map_ee smull,
52

---

Under review as a conference paper at ICLR 2023
have h19 subrepresentation (linear magaeragaaaaageeeee... f), from subrepresentation..tte (h18 :-,,
have h20 is_submodule (Linear_map, range f] W, from is_submodule.ne (h18 _),
So the image of (x) is subspace SW (Iprineee) of $us stable under the action of SGS, so it a subrepresentation and $5$ must be zero or suzjective.
have h21 is_submodule (Linear_mal map. range H) linear_map range i W * from by auto [iinear_ pawnear_map..ce map.range__se _e________ saage_____ppl_
have h22 is_submodule (1inear_map,
alinear_map.p. range w + * 0, from by auto [h21, h20] using siinear_ma.injeee
f)
have h23 is_submodule G (linear_map.ran
f) w + 1inear_map. range f
= W + * from by auto [h22,
linear Sanear_map.co map.injective_eet Ler_rvee_____eeeeeeeee___eee_e sa____anne___________e top] using dilnear_app.injettee
have h24 is submoduul (linear_ma) map. rangr f) > linear_map map. range
= N + * 0, from by auto [h23, h16] using
surjective, in which case it have h25 f * + linear_mape map._mmppaa.. range R, from by auto [h24, hib] using [iinear_man sateaar_appppee saange_e__topll
By assumption
zero, so
is an isomorphism.
have h26 * linear map. range
from by auto [h25, h12]
using [Linear map. range eq range_ee_tops topl,
-- QED
show # 0 V w, from auto [linear_map ls__iinar_eeuueeeeeeeeeeeeeessse h26]
using Slinear_map.3 lww.ai__eee_iiii
end
D.4.12 A GRAPH IS BIPARTITE IFF IT IS 2-COLOURABLE
The scores for the statement formalisation were overall very low the most common formalisation was two cooocclaaableeeeeooo G <+ bipartite G, which is incorrect as neither of these terms are defined mathlib. The proof outlines and outlines with auto were also of low quality, often failing to split the proof into two cases and failing to explicitly define the two parts in the bipartite graph. Full proofs seem to be doing marginally better, with outlines being the second best. Although the average performances in temperatures 0.4 and 0.8 are the same, the maximum scores attained at temperature 0.8.
The best proof format observed were outlines at temperature 0.8. Correct Lean theorem statement was not included in the prompt.
Theorem statement:
Let G be graph. Then G is 2-colorable and only if G is bipartite.
Natural language proof:
Let G be a 2-colorable graph, which means we can color every vertex either red or blue, and no edge will have both endpoints colored the same color. Let A denote the subset of vertices colored red, and let denote the subset vertices colored blue. Since all vertices of A are red, there are no edges within A, and similarly for B. This implies that every edge has one endpoint in A and the other in B, which means G is bipartite.
Conversely, suppose G is bipartite, that is, edge has one endpoint in Vi and the other in Vz. Then coloring every vertex of Vi red and every vertex of V2 blue yields valid coloring, so G 2-colorable.
partition the vertices into subsets V1, V/ every
Q.E.D.
Codex Output
53

---

Under review as a conference paper at ICLR 2023
theorem graph 2 colorable iff bipartite V graph, (3 coloring 2, ele_valid_collring G c) + bs_ 6
begin
--
Let $G$ be a 2-colorable graph, which means can color every vertex either red or blue, and no edge will have both endpoints colored the same color.
assume (G : graph),
have h1 : V c coloring c 2, (eid_ c), from by
assume (c coloring 2), serry, b
-- Let $2$ denote the subset of vertices colored red, and let SBS denote the subset of vertices colored blue.
have h2 V c: coloring G 2, (iis_ jiis_valid_coloing
c) +
A : set (vertex G), 3 set (vertex G),
(4 v vertex G, e = red + V A (A v vertex
G, c blue v B)), from
by
assume (c : coloring G 2) (h2 : Bis_valid sorry, b
c),
$A$ and $B$ are subsets of verties of SGS, by definition of valid coloring. have h3 V c coloring 6 2,
3 c) +
(3 A set (vertex G), 3 B set (vertex G),
(V vertex G, e red
A) : vertex
G, c v blue 4 v B)
A S vertex G A S vertex G), from
by
assume (c coloring 2) (h3 Bis dis_valid c), sorry, b
Since all vertices of $A$ are red, there are edges within SAS, and similarly for SHS. have h4 V c coloring 2, (Bis valid coloring c) +
(3 A set (vertex G), B set (vertex G)
(V v vertex G, a = red t v E A) A (V vertex A
G, C blue +
e edge G, (source E A target o A) V (scurce e E B A target E B)), from by
S vertex A C vertex
assume (c coloring G 2) (h4 Bis fis_validdcoloring G c),
scrry, b
This implies that every edge has one endpoint in $A$ and the other in SHS,
which means SG$ is bipartite.
have h5 : V.C. C coloring G 2, (Bis @eis_valid_coloring
c) +
(3 A set (vertex G), B set (vertex G),
(V vertex G, e = red t v E A) A (V vertex B)
G, C blue
C vertex E V scurce o B) (V o edge G, target e E A V target e E B)), from
C vertex
edge G, source
by
assume (a : coloring 2) (h5 dis_valid_emm sorry,
c),
54

---

Under review as a conference paper at ICLR 2023
Hence the existence of valid coloring implies that the graph is bipartite.
have h6 4 с coloring G 2, (eie_valld c) + (3 A set (vertex G), 3 B : set (vertex G),
(V v vertex G, red & E A) A (V vertex S vertex A LBAAUE vertex
G, c
blue
S vertex
G),
from by
assume (c : coloring 2) (h6 _is_valid dis_valid_colorig c) sorry,
h
Conversely,
have h7 V B set (vertex G), G + A BUB vertex G -
S vertex C vertex ( c coloring G 2, eis_valid G c (V vertex
red + A) A (V vertex
G, c blue by
B)), from
assume (A B set (vertex G)) (h7 A 1 B) (h8 : A C vertex G
A S vertex G) (h9 A U.B vertex G), sorry, I
-- Suppose SG$ is bipartite, have h8 A B set (vertex G), A 1 S vertex G A C vertex
vertex is biparrtt G, from
by assume (A B set (vertex G)) (h8 A 1 B) (h9 : A S vertex G A S vertex G) (h10 AUB B vertex 3), serry, h
Hence the existence of valid coloring is eguivalent to the graph being bipartite. sorry, end
D.4.13 P-ADIC UNITS
In a few cases, Codex ignored the p-adic setting entirely and formalised everything in terms of integers and natural numbers. The correct notation for p-adic integers was also captured correctly in most cases. A common етгог was to formalise the first line of the proof ("Let us prove the contrapositive, that is, is x is not a unit Zp. then x is not coprime to p."), which outlined the general strategy of the proof, best, with fairly useful outlines and relevant-looking theorem names the arguments for auto. The results seem be better temperature 0.4.
separate have statement. Proofs with premises
by far the
This proof is entirely uncontaminated.
Theorem statement:
Given a prime number p and a natural number x, if x coprime to then x is a unit in the p-adic integers.
Natural language proof: Let us prove the contrapositive, that is, is is not a unit of Zp. then æ is not
coprime to p. We know that any element of Z, is a unit and only it has norm 1, thus ||x:] # 1. Also, since every element of Z, must have norm less than equal 1, conclude that |||| < 1. But this must imply that plz. This completes our proof.
Q.F.D.
55

---

Under review as a conference paper at ICLR 2023
Codex Outpur
One of the best outputs (proof with premises, temperature 0.4):
theorem P_adi c_uitts (p : N) (x N) (h coprime P x) is_unit (x 2
/p)
begin
Prove the contrapositive, that is, is 5x8 is not a unit of \mathbb(2)_pp then 5xş is not coprime to $p$ have h1 is_unit (x 2/p) + coprime X, from by auto cnprice syperreeessmm, symm, cop.coprime deff, nat coprime def, nat. nat.coprime. symm, nat.com coprimm, def, nat. coprime, defl,
We know that any element of $lmathbb(2]_ss is a unit if and only if it has norm have h2 is_unit (x 2/p) (norm_num (x : 2/p)) 1, from by auto oet_e_e__n_____________
-- Also, since every element of $lmathbb [X]_p$ must have norm less than equal to have h3 (norm_num (x 2/p)) < from by auto [norm_num_le_onee
But this must imply that 6p 1 x have h4 - is unit http__uu__e__oo__i__ieeeeee_____ nat a.d.dvvdLLff..ooonnnn.ooo.oo..
(x is_unit
Z/p) + p from by auto norm_nun__e__ne,,
-- This completes our proof
show is in_t (x Z/p), from by auto [h1, h2, h3, h4, b]
end
56


Reviews:
[{"review_id": "wkWu9wKmwL", "reviewer": "Reviewer_orra", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper considers the automatic generation of formal math statements from (less formal) mathematical statements in natural language. The statements are translated using Codex in a few-shot setting. The contributions are a postprocessing technique for formalized statements, prompt engineering to improve results, and some first attempts at formalizing proofs (not only theorem statements).\n\nThe paper also introduces two simple evaluation sets that address the problem that Codex might have seen the formalizations in their regular evaluation set during pretraining.", "summary_of_the_review": "Interesting paper, but I am not sure if the contributions make the bar for ICLR.", "strength_and_weaknesses": "I am not sure about the novelty and impact of the contributions:\n- The postprocessing technique presented in this work addresses the problem that most of the available training data is for Lean3, but the approach here used Lean4 syntax. So the problem addressed here is not of general interest. The technique itself seems to be rather adhoc as well.\n- The prompt engineering is similar to Jain et al. (2022), which the authors attribute correctly. It uses similar examples in the few-shot prompt to improve the results.\n- The formalization of proofs seems novel to me (it goes significantly beyond Wu et al. (2022)), but is restricted to a very small dataset and only 2 of the 18 attempts were successful.\n- Other possible contributions, like the evaluation sets, may be nice, but I'm not sure if they carry the paper.\n\nMinor questions:\n- \"For proofs quantitative analysis is infeasible\" Why?\n- \"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).\" I do not understand the justification \"as they often assume more in terms of implicit context\". ", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "1: The contributions are neither significant nor novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "_311U4ntPd6", "reviewer": "Reviewer_jvt2", "summary": "", "questions": "", "limitations": "", "rating": 1, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper shows empirically that Codex LLM is able to generate mathematical formalizations in a recently developed proof assistant Lean from natural language using prompting. The results include formalization of the relatively short theorem statements with a modest accuracy of 75%, and attempts to formalize short proofs. The overall results are mixed, with proofs requiring significant post-processing and manual fixing. ", "summary_of_the_review": "In its current form, the draft appears to be a work in progress. The focus of the work is empirical demonstration of LLM for autoformalization and the draft falls far short of presenting enough empirical evidence. Expanding to other proof assistants (Coq, PVS etc) and using their large corpus of theorems and proofs to test whether Codex LLM can complete these would be useful. Also, given the lukewarm results, perhaps, prompt engineering can help improve results. ", "strength_and_weaknesses": "Strength:\n\n+ The paper builds on a recent line of promising work on using LLMs for mathematical reasoning task - the focus of this paper on autoformalization. \n\nWeakness: \n\n- Why only limit the work to Lean theorem prover? If the Codex LLM is capable of autoformalization, it should be able to work with Coq, Isabelle and PVS - theorem provers which have been around for decades and are widely used in academia and industry. They also have fairly large libraries that can be used for evaluation. The current simple theorems are not representative of typical need for formalization. \n\n- Some of the prompt examples appear to be imprecise. For example, the natural language talks about vector space and the formalization uses division_ring and module. While one could argue that this is okay because the formal statements are correct but nonetheless the English statement was more specific and one would expect formalization to stay at the same level. Given this example, the reviewer fears that the paper is using a rather liberal notion of \"correct\" statement. This is particularly concerning given the very simple nature of this \"theorem\" statements, which aren't really the challenging aspects of formalization in proof assistants. \n\n- There appears to be significant shift in technique and results for theorems and proofs. Input-dependent prompting is not feasible for proofs. Elaboration is also not feasible. The results for proofs appear to be far worse and no correct proof were generated. The notion of identifying \"easily repairable\" proof is unclear and rather vague. Looking at figure 3, the error in constructed proof were significant. The expansion of absolute value would have created branches and led to severe difficulty in the proof. It is much better not to expand before applying triangle inequality.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "1: The contributions are neither significant nor novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "KdEmoQ7TBm", "reviewer": "Reviewer_eYGZ", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper investigates the application of language models to interactive theorem proving by doing a qualitative case study on input-dependent prompt engineering. It shows that Codex is capable of producing partially correct formal proofs (in Lean 4) that can be turned into correct proofs with a moderate amount of modification (possibly done by a human user).", "summary_of_the_review": "I am glad to see the nice qualitative study in this paper, but the overall contribution of this paper is rather insufficient. I suggest the authors try to add more content before the paper can be accepted.", "strength_and_weaknesses": "Strength:\n\n+ The qualitative study is interesting. There hasn't been much work in the field of ML for interactive theorem proving that includes a case study like the one in this paper.\n\nWeakness:\n\n- The contribution looks a bit pale. While observing the consequence of prompt engineering is interesting, prompt engineering itself and the particular methodology (i.e., input-dependent prompts by similarity) adopted in this paper are not new.\n\n- The postprocessing of a completion produced by Codex is claimed as part of the contribution. However, if I understand it correctly, the elaborator is technically a procedure that tranlates expressions in Lean 3 to their counterparts in Lean 4 while making sure that the translated expressions type check.  I appreciate the engineering efforts here, but this part is more of a Lean-specific tweak required to make things work, and does not seem general enough to be a significant contribution.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "6v2J-bVxRS", "reviewer": "Reviewer_Pspz", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper applies a large language model, Codex to the autoformalisation of proof statements and of proofs. Two main contributions resulting are: (1) translating theorem statements of a form similar to docstrings of mathlib to theorems, and (2) translating (outlines of) NL proofs to Lean proofs.\n\n\n\n", "summary_of_the_review": "This is a paper of high novely, yet the results are hard to understand. Further, the technica basis of the approach is lacking.", "strength_and_weaknesses": "Strengths:\nThe paper is very interesting and has good novelty. \n\nWeaknesses:\nThe main drawback is that the article is very hard to read. The paper is written in a very loose style with almost no technical basis on which to understand what is going on. No model for a mathematical statement is provided, or of the technical basis for the rewriting. It is fully an application of existing tools to a rewriting process, with no details of what the technical novelty is. ", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Decision: Reject