If you are a mathematician on earth right now, you have probably heard of the Lean and its enormous growth and success, especially in combination with LLMs. You may, like many other mathematicians, be feeling very disoriented and uncertain about the future of mathematics. I can’t help much with that; I think the world is and will continue to be fundamentally uncertain and disorienting. But I’m here to encourage one relatively simple action that I think will benefit essentially all mathematicians;

Learn to read Lean.

A crucial part of my point is that I do really mean read. A lot of people are intimidated by Lean, and I think focusing on literacy can help ease that feeling. Reading is the easiest part — I think also the most important!

To put my money where my mouth is, a few weeks ago I had the research group that I run start learning Lean systematically, by going through the textbook Mathematics in Lean together.

The overwhelming benefits of Lean

I think a lot of readers will have heard this part before, and it has been said better elsewhere, so you can skip this part if you want. But it feels appropriate to at least list the major reasons why Lean is so helpful.

You no longer have to worry about errors in your proofs. And you no longer have to worry about errors in in other people’s proofs. You can stop worrying about whether a proof is correct and focus on what the proof means.

As an interactive theorem prover, Lean will tell you (via the InfoView pane) the exact state of a proof at any point in the middle. This is useful not only for coming up with proofs, but for understanding existing proofs. It can take a load off your working memory.

Math is much more searchable. If you want to look for existing work on a given conjecture, you can now search for that using the actual formal statement. Any proofs of it are instantly verifiable as a proof for your particular conjecture.

With the automation tools built into Lean and the immensely capable LLMs, large parts of your research can now be automated. At present, taking advantage of these breakthroughs hinges on understanding what the Lean code says.

For many decades, the main reason not to use the existing formal proof systems was because no one used them, almost no mathematics had been implemented in them, and they were very hard to learn. In the last few years all three of these barriers have been pulverized, and the floodgates of the benefits are now open.

Lean Literacy is the crucial human-machine interface

There is a wide variety of ways and depths that someone could choose to use these new tools. But running through all of them, including the super-powered AI automations, is the simple foundational skill of reading Lean.

By reading Lean I mean being able to pull up a .lean file on GitHub, VSCode or anywhere else, and make any sense of it. I mean thinking to yourself, “right, this is a consequence of the data processing inequality” and then being able to find that inequality stated in Lean (or write it yourself) and then be sure that it is the theorem you were thinking of. I mean reading a paper on algebraic varieties, getting to an appendix that shows the Lean code of the paper’s main theorems, and having a rough sense of how those theorems should look different to apply to your own subfield of toric geometry.

I also mean reading your student’s Lean code and being able to tell that they made a mistake in specifying the order of the limit operators such that they accidentally proved a much easier theorem. This is the kind of math literacy that you already employ all day, only now it’s in a fixed-width font where people use less spatial arrangements and more syntax coloring.

LLMs will also make these mistakes, or misinterpret your prompt, or even make adversarial errors. It is crucial for society that its experts in mathematics train to interface with these new systems, to help the broader effort of ensuring that AI is beneficial. This can be done with an overhead cost comparable to learning to write papers in LaTeX, and I also claim it will be way more fun.

[Part 2 coming soon]