Motivation
I’ve been captivated by the recent movement to popularize mathematics formalization through the Lean theorem prover, and this year I’m diving deeper into learning it.
For those unfamiliar with this revolution, I highly recommend watching Kevin Buzzard’s talks on YouTube for an overview of why formal mathematics is generating such excitement in the mathematical community.
The immediate benefits of formalization are well-documented: it helps catch errors in proofs and reduces the need for trust between collaborators since every step is mechanically verified. However, I believe there’s another compelling advantage that’s less frequently discussed: formalization enables a better separation of concerns in mathematical writing.
When proofs are formally verified by tools like Lean, mathematicians can focus their written exposition on what truly matters to human understanding: the intuition, motivation, and creative journey that led to the proof. Instead of devoting pages to mechanical verification of technical details, we can concentrate on conveying the key insights that make the proof work.
This shift in mathematical writing style becomes even more significant in the era of Large Language Models (LLMs). Having more written text about mathematical intuition and proof strategies, rather than just formal proof details, will be invaluable for training AI systems to understand how mathematicians actually think and approach problems.
I envision future mathematicians collaborating with AI in a two-tiered approach: engaging with conversational AI to explore high-level proof strategies while using Lean and specialized coding assistants to construct the formal proofs themselves. The resulting papers will focus on telling the story of the proof—highlighting the key insights, explaining where the “spark of genius” occurred, and distinguishing these moments from the parts that were “just following the symbols.” The complete formal proofs will live in GitHub repositories, serving as detailed technical appendices to the main narrative.
Audience
I am trying to follow the ethos of “learning in public,” but these are still more of my personal learning notes and not (yet) targeting a very broad audience. Also, I am optimizing for getting posts out quickly over a polished presentation.
As such, this post will be most useful for people with a similar background as mine. A quick summary of where I am as I begin this journey:
... continue reading