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.

本研究使用大型语言模型 (Codex) 探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于 120 个定理，Codex 可以在本科水平上以近 75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex 可以以自然语言形式翻译本科水平的 13 个定理的证明，这些具有两到三自然段长度的证明可以在 12 次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。