1. Introduction🔗

1.1. What is autoformalization?🔗

Formal verification involves the use of logical and computational methods to establish claims that are expressed in precise mathematical terms. These can include ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their specifications.

Lean is a tool that allows for the formal verification of mathematical theorems (among other things). In practice, this means that if you formalize a theorem statement and its proof in Lean, you can be sure that the proof is correct and that the theorem holds (as long as (1) the formal statement faithfully represents the informal statement, and (2) you are not using any of the tricks explained here).

Even though Lean is very good at providing certain programs (called tactics) that make formalization more practical and accessible, it is still very difficult and time-consuming to formalize research-level mathematics in Lean. However, in recent months, LLMs (large language models, like, but not really like, ChatGPT) have become so powerful at writing code that they are able to write Lean code at scale. We call autoformalization the process by which LLMs formalize math results by themselves, with humans only supervising the process. This makes formalizing your mathematical research actually possible (although far from trivial).

Is autoformalization then strictly better than (manual) formalization? Not really. This practical approach to formalization comes at a cost: understanding and optimizing the code. Like most things in life, it is a tradeoff: you are giving up code quality, and in exchange you are gaining enough speed and scale to be able to formalize research-level results. This is not better or worse in any way. It is just a different goal. A goal that, by the way, is only possible thanks to the existence of mathlib, the standard Lean mathematical library, which is curated and maintained by humans.

1.2. How to read this guide🔗

This guide is modular: if you are familiar with the topic of a chapter, feel free to skip it. The chapters are meant to build a working practice before filling in every technical detail, so it is fine to move forward before every tool feels completely familiar.

Code blocks show commands, code snippets, or command outputs. For instance, the following is a Lean snippet:

def double (n : Nat) : Nat := n + n

The following is a Bash command (echo hello), together with its output (hello).

echo hello

hello

Don't worry if you don't know yet what a Bash command is. We will explain this in the very first chapter.

1.3. The general approach🔗

The general idea is this: we will ask LLMs to write Lean code that formalizes our mathematical statements and proofs; then the Lean kernel will make sure that the proofs work. However, this is a huge oversimplification of what will be going on under the hood. A more detailed explanation is this:

First, think about all the infrastructure (i.e., preliminary material) you will need to formalize your paper.
(Semi)autoformalize all this infrastructure into one or several shared libraries, so that the material can later be reused.

Semiautoformalization

Semiautoformalization is a term that better describes what will be going on in this part of the process. We will let the LLM write the Lean code, but with a reasonable amount of human supervision and steering. The human will think beforehand about how the formalization will go at a high level, and then let the LLM fill in the details. Also, the human will supervise the work of the LLM, thus discovering, in the process, new abstractions and better ways to organize the content. This will certainly not produce mathlib-level code (because we will not spend enough time with the code; remember, we are sacrificing code quality for scale), but it won't be a pure black-box autoformalization either. Thus the term semiautoformalization.
Finally, once we are sure all the necessary infrastructure for the paper is built, we can autoformalize the paper. At this point it may make sense to use a pure autoformalization if the contents of the paper are still too specific to be included in a library.

1.4. Contributing🔗

This document is alive. The programs and tools presented here, as well as technology and the world in general, change so fast that it doesn't make sense to think about this guide as something static. Contributions are very much appreciated and needed.

TODO: Explain how to contribute.