1. Introduction
In recent years, a question that has been around for decades has come back with renewed strength: can machines do mathematics?
The answer, in general, is still no. But with recent advances in artificial intelligence and formal verification, this barrier is starting to shake. Some systems have already managed to prove, in a fully automated way, results at the level of the mathematical olympiads (Trinh et al., 2024)Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong (2024). “Solving olympiad geometry without human demonstrations”. Nature. 625(7995), pp. 476–482..
A first challenge when trying to get a computer to do mathematics is closing the gap between the language we understand and the language a machine can process. Even though mathematical language is already quite precise, there is still a considerable distance between a proof written in a paper and one that a computer can validate.
Some of the first attempts to create a language in which mathematics would be understandable to a machine go back to projects such as Automath (1967) and Mizar (1973). Nowadays, tools such as Coq, Isabelle, HOL or Lean make it possible to write and verify mathematics with the assistance of a computer. These tools are known as interactive theorem provers (ITPs) (Geuvers, 2009)Herman Geuvers (2009). “Proof assistants: History, ideas and future”. Sadhana. 34, pp. 3–25..
In this project I focus on learning and using Lean, one of these tools. I am especially interested in this intersection between mathematics and computation: the process of writing mathematics in such a way that a computer accepts it as valid. To me, formalising proofs in Lean feels like solving a complex and challenging puzzle.
I chose Lean over other proof assistants because I had several resources at hand that made it easier to learn, such as courses taught at my Faculty and a large amount of online documentation, thanks to the Lean community. This community is very active, with thousands of users and an extensive library of formalised mathematical results ready to be reused. I also value that its syntax is closer to ordinary mathematical language than that of other systems.
In particular, I decided to work on results from topology because I find it an especially interesting branch (probably influenced by the fame of mugs and doughnuts) and because it is an area abstract enough to put to the test the capabilities of the formal language — as well as my own — in this puzzle of topological pieces.