Why formalize mathematics – more than catching errors
17 comments
·October 19, 2025cbondurant
bwfan123
Bessis [1] argues that formalism - or loosely math writing - is foundational to clarifying intuition/meaning in a way that natural language cannot. Imagine it as a scalpel carving out precise shapes from the blur of images we carry thereby allowing us to "see" things we otherwise cannot.
I am curious to try out lean to understand how definitions in lean are able to operationally capture meaning in an unambiguous manner.
[1] https://www.amazon.com/Mathematica-Secret-World-Intuition-Cu...
lo_zamoyski
For mathematics and certain fields, that is true. But the formalism matters, and as some have argued, the Fregean style that came to dominate in the 20th century is ill-suited for some fields, like linguistics. One argument is that linguists using this style inevitably recast natural language in the image of the formalism. (The traditional logical tradition is better suited, as its point of departure is the grammar of natural language itself.)
No formalism is ontologically neutral in the sense that there is always an implied ontology or range of possible ontologies. And it is always important to make a distinction between the abstractions proper to the formalism and the object of study. A common fallacy involves reifying those abstractions into objects of the theory, at least implicitly.
anon291
I mean, if you understand leans system then you understand the formal manipulation needed for precise and accurate proofs. Most mathematical papers are rather handwavy about things and expect people to fill in the formalism, which is not always true, as we have seen
oersted
I've been excited about Lean for years, not because of correctness guarantees, but because it opens the door to doing maths using software development methods.
Libraries of theorems and mathematical objects, with well defined abstractions that are ergonomic to apply in target use cases. Accompanied by good documentation, focused less on how the theorems are proven (how the functions are implemented), and more on what to use them for and how. With proper version control and package management.
I believe that all these practices could vastly improve collaboration and research velocity in maths, as much or more than AI, although they are highly complementary. If maths is coding, AI will be much better at it, and AI will be more applicable to it.
vonnik
Out of curiosity, does anyone know the mathematicians actively leaning into AI + Lean?
oersted
Terence Tao is well known for being enthusiastic about Lean and AI and he regularly posts about his experiments.
He is also a serious research mathematician at the top of his game, considered by many one of the best mathematicians alive. This might be biased by the fact that he is such a good communicator, he is more visible than other similarly good mathematicians, but he is a Fields medallist all the same.
thechao
Terence Tao posts on mathstodon fairly regularly about lean, AI, and math. I'm not going to interpret his posts.
anon291
As a a hobbyist mathematician / type theorist, chatgpt et al are great at 'looking up' theorems that you want to exist but that you may not have read about yet. It's also good at connecting disparate areas of math. I don't think lean subsumes AI. Rather, lean allows you to check the AI proof. ChatGPT genuinely does have a knack for certain lines of thought.
nyrikki
LLMs and Lean are orthogonal, neither subsumes either.
They both can be useful or harmful, do to their respective strengths and trade offs.
PAC/statistical learning is good at needles in the haystack problems assuming that the tail losses, simplicity bias, and corpus representation issues are acceptable and you understand that it is fundamentally existential quantification and control for automation bias etc…
Lean is a wonderful collection of concepts and heuristics but due to Rice and Gödel etc… will not solve all problems with software development.
How Gödel’s second incompleteness theorem shows that you can prove anything, without that proof being meaningful is a lens into that.
It is horses for courses, and remember that even in sub-TC total functional programming, proving and arbitrary functions is very hard, while constructing one is far more tractable.
Even those proofs don’t demonstrate semantic correctness. History is riddled with examples of people using powerful tools that elegantly explain flawed beliefs.
The 2009 crash and gaussian copula as an example.
Get all the value you can out of these tools, but use caution, especially in math, where superficially similar similarities often have conflicting conventions, constraints, and assumptions.
Obviously if you problem is ergotic with the Markov property, both will help, but Automated theorem proving and PAC learning will never be a meta theory of the other IMHO.
KalMann
I want to respond to each of his points one by one
> powering various math tools
I don't think going through a math proof like they were computer programs is a good way to approach mathematics. In mathematics I think the important thing is developing a good intuition and mental model of the material. It's not a huge problem if the proof isn't 100% complete or correct if the general approach is good. Unlike programming, where you need a program to work 99.9% of the time, you have to pay close attention to all the minute details.
> analyzing meta-math trends
I'm highly skeptical of the usefulness of this approach in identifying non-trivial trends. In mathematics the same kinds of principles can appear in many different forms, and you won't necessarily use the same language or cite the same theorems even though the parallels are clear to those who understand them. Perhaps LLMs with their impressive reasoning abilities can identify parallels but I doubt a simple program would yield useful insights.
> Basically, the process of doing math will become more efficient and hopefully more pleasant.
I don't see how his points make things more efficient. It seems like it's adding a bunch more work. It definitely doesn't sound more pleasant.
UltraSane
Lean is amazing for collaboration because anyone can contribute to a proof and their work be automatically verified.
westurner
> While Paulson focuses on the obvious benefit of finding potential errors in proofs as they are checked by a computer, I will discuss some other less obvious benefits of shifting to formal math or “doing math with computers”
From https://news.ycombinator.com/item?id=44214804 sort of re: Tao's Real Analysis formalisms:
> So, Lean isn't proven with HoTT either.
constantcrying
Much of the argument is the same as for the initial push to formalize mathematics in the late 19th century. Formalisms allow for precision and help reduce errors, but the most important change was in how mathematicians were able to communicate, by creating a shared understanding.
Computerized mathematics is just another step in that direction.
null
dboreham
Imho it was always "computerized", they just didn't have a computer. To me the approaches used in the early 20th century look like people defining a simple VM then writing programs that "execute" on that VM.
pfdietz
Another reason to formalize math is that formalized proofs become training material for automated mathematics.
Ultimately we want all of the math literature to become training material, but that would likely require automated techniques for converting it to formalized proofs. This would be a back-and-forth thing that would build on itself.
Lean was a gamechanger for me as someone who has a "hobby" level interest in abstract mathematics. I don't have the formal education that would have cultivated the practice and repetition needed to just know on a gut level the kinds of formal manipulations needed for precise and accurate proofs. but lean (combined with its incredibly well designed abbreviation expansion) gives probably the most intuitive way to manipulate formal mathematical expressions that you could hope to achieve with a keyboard.
It provides tools for discovering relevant proofs, theorems, etc. Toying around with lean has actively taught me math that I didn't know before. The entire time it catches me any time I happen to fall into informal thinking and start making assumptions that aren't actually valid.
I don't know of any way to extract the abbreviation engine that lean plugins use in the relevant editors for use in other contexts, but man, I'd honestly love it if I could type \all or \ne to get access to all of the mathematical unicode characters trivially. Or even extend it to support other unicode characters that I might find useful to type.