1.1. What is autoformalization?🔗

According to Theorem Proving in Lean:

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 practise, 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 in TODO).

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 the recent months, LLMs have become so powerful at writing code, that they are able to write Lean code at scale. We call autoformalization the process in 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 then autoforamalization strictly better than (manual) formalization? Not really. This practical approach to formalization comes at a cost. A cost of understanding and optimizing the code. Like most things in life, it is a tradeoff: you are leaving out code quality and in exchange you are gaining enough speed and scale to be able to formalize your own 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, configuration, code snippets or command outputs. For instance, the following is a Lean snippet:

The following is a Bash command together with its output (we will see later what this means).

echo hello

hello

When a block is marked as Lean, treat it as the precise version of the surrounding informal explanation.

1.3. Contributing🔗

This document is alive. The programs and tools presented here, 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 appreciated and needed.

TODO: Explain how to contribute.