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.
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.
> 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.
How is any of that different from what we had in math before Lean?
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.
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.
> 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”
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.
As a former professional mathematician: the benefits mentioned in the article (click-through definitions and statements, analyzing meta trends, version control, ...) do not seem particularly valuable.
The reason to formalize mathematics is to automate mathematical proofs and the production of mathematical theory.
I know nothing of mathematics but found it fascinating, especially the idea that if outside information changes that affects your proof, you can have the Lean compiler figure out which lines of your proof need updating (instead of having to go over every line, which can take days or more).
Is there, somewhere, a list of theorems that were considered proved and true for a while, but after attempts at formalization the proof was invalidated and the theorem is now unknown or disproved?
I recommend the natural number game (also mentioned above) for a casual introduction to the mathematics side, just to get a feeling.
If you are serious about learning lean, I recommend Functional Programming in Lean for learning it as a programming language and Theorem Proving in Lean for learning it as a proof assistant
I’m not a mathematician, so could someone explain the difference in usage between Lean and Coq?
On a surface level my understanding is that both are computer augmented ways to formalize mathematics. Why use one over the other? Why was Lean developed when Coq already existed?
I think the difference is mostly cultural. The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.
Many people in the Rocq community see this as a no-go and some argue this will cause the system to be hard to use over the long run. In the Lean community, the interest in type theory is at a much lower level, and people see this as a practical tradeoff. They recognize the theoretical issues show up in practice, but so infrequently that having this axiom is worth it.
I consider this matter to be an open question.
If you look at what's being done in the communities, in Lean the focus is very much on and around mathlib. This means there's a fairly monolithic culture of mathematicians interested in formalizing, supplemented with some people interested in formal verification of software.
The Rocq community seems much more diverse in the sense that formalization effort is split over many projects, with different axioms assumed and different philosophies. This also holds for tooling and language features. It seems like any problem has at least two solutions lying around.
My personal take is that this diversity is nice for exploring options, it also causes the Rocq community to move slower due to technical debt of switching between solutions.
> The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.
Couldn't you introduce proof relevance as an explicit axiom into a Lean program to solve that particular issue?
Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation?
If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check?
I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tests don't check what you thought.
In a lot of cases you can get far by locally proofreading the definitions.
Trying to formally prove something and then failing is a common way people find out they forgot to add an hypothesis.
Another pitfall is defining some object, but messing up the definitions, such that there's actually no object of that kind. This is addressed by using test objects. So suppose you define what a ring is, then you also prove that real numbers and polynomials are examples of the thing you defined.
A point that is maybe not obvious to people who have not done mathematics at a high level or done “new” mathematics, is that often you end of changing your theorem or at least lemmas and definitions while figuring out the proof. That is, you have something you want to prove, but maybe it is easier to proving something more general or maybe your definitions need to change slightly. Anecdotally, during a project I spend perhaps a year figuring out exactly the right definition for a problem to be able to prove it. Of course, this was a very new thing. For well-know areas it is often straight forward, but at the frontier, both definitions and theorems often change as your proceed and understand the problem better.
I have proven quite a few theorems in Lean (and other provers) in my life, and the unfortunate reality is that for any non-trivial math, I still have to figure out the proof on paper first, and can only then write it in Lean. When I try to figure out the proof in Lean, I always get bogged down in details and loose sight of the bigger picture. Maybe better tactics will help. I'm not sure.
If anyone is curious about the phenomenon, the second problem in session 7 at https://incredible.pm/ [ ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) ] is one where the proof is straightforward, but you're unlikely to get to it by just fooling around in the prover.
I love the analogy in David Bessis's wonderful book Mathematica (nothing to do with Wolfram). We all know how to tie our shoes. Now, write in words and symbols to teach someone how you tie your shoes. This is what a proof is.
Often even people with STEM degrees confuse what mathematicians do with the visible product of it - symbols and words on a page. While the formalism of mathematics has immense value for precision, and provides a "serialization language" (to borrow a CS analogy), it would be akin to confusing a Toaster with the Toaster manual, or shoelaces with the instructions.
I think the analogy between JavaScript and TypeScript is not 100% because although JavaScript has some quirks in its design, it is fully consistent. My biggest issue with math is symbols that are reused to mean different things in different contexts. It makes maths more time-consuming to learn and makes it difficult to jump between different fields.
Personally, at times, I struggled with the dual nature of mathematics; its extreme precision in meaning combined with vague and inconsistent use of symbols is challenging... Especially frustrating when learning something new and some symbols that you think you understand turn out to mean something else; it creates distrust towards maths itself.
For anyone that's interested in formalizing mathematics but wished there was an easier way to do it, I've been working on a different sort of theorem prover recently.
The idea is that there's a small AI built into the VS Code extension that will fill in the details of proofs for you. Check it out if you're interested in this sort of thing!
I don't get the point about trivial proofs. Can't you just tell Lean to assume something is true and then get on with the rest of the interesting part?
You can but that ruins the fun and also misses the point. How do you know your "trivial" theorem is actually trivial? Proofs are mechanized to increase our trust into them, and it defeats the point if you have to still manually review a myriad of helper lemmas.
Rado Kirov shows that formalization transforms how mathematicians think about structure and collaboration. My work begins from the same premise, but in the world of programming and system software. I aim to bring formal structure to programming itself, treating algorithms, operating systems, and programming languages as subjects that can be expressed with the same rigor as mathematics.
Elements of Programming presents programming as a mathematical discipline built on structure, logic, and proof. Written in the style of Euclid’s Elements, it defines computation through clear axioms, postulates, and propositions. Each book develops one aspect of programming as a coherent system of reasoning.
Book I establishes identity, transformation, and composition as the foundations of computation.
Book II introduces algebraic structures such as categories, functors, and monads.
Book III unites operational and denotational semantics to show that correctness means equivalence of meaning.
Book IV formalizes capability-based security and verification through invariants and confinement.
Book V connects type theory with formal assurance, explaining how types embody proofs.
Book VI extends these ideas into philosophy and ethics, arguing that software expresses human intention and responsibility.
The issue is when people conflate formalism with truth itself. I know a lot of people who reject anything that isn't under the umbrella of "stuff that is formalised", even if it can be formalised but was simply not presented as formalised in its first incarnation.
Not super convinced by this analogy. Tooling and convenience feel secondary in math. If formalization doesn't help us do better mathematics, not just more structured mathematics, I'm pretty skeptical these benefits will justify the cost.
31 comments
[ 5.0 ms ] story [ 49.8 ms ] threadComputerized mathematics is just another step in that direction.
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.
> 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.
How is any of that different from what we had in math before Lean?
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.
> 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.
From https://news.ycombinator.com/item?id=44214804 sort of re: Tao's Real Analysis formalisms:
> So, Lean isn't proven with HoTT either.
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.
The reason to formalize mathematics is to automate mathematical proofs and the production of mathematical theory.
I know nothing of mathematics but found it fascinating, especially the idea that if outside information changes that affects your proof, you can have the Lean compiler figure out which lines of your proof need updating (instead of having to go over every line, which can take days or more).
[1] https://mathoverflow.net/questions/291158/proofs-shown-to-be...
I recommend the natural number game (also mentioned above) for a casual introduction to the mathematics side, just to get a feeling.
If you are serious about learning lean, I recommend Functional Programming in Lean for learning it as a programming language and Theorem Proving in Lean for learning it as a proof assistant
Many people in the Rocq community see this as a no-go and some argue this will cause the system to be hard to use over the long run. In the Lean community, the interest in type theory is at a much lower level, and people see this as a practical tradeoff. They recognize the theoretical issues show up in practice, but so infrequently that having this axiom is worth it. I consider this matter to be an open question.
If you look at what's being done in the communities, in Lean the focus is very much on and around mathlib. This means there's a fairly monolithic culture of mathematicians interested in formalizing, supplemented with some people interested in formal verification of software.
The Rocq community seems much more diverse in the sense that formalization effort is split over many projects, with different axioms assumed and different philosophies. This also holds for tooling and language features. It seems like any problem has at least two solutions lying around. My personal take is that this diversity is nice for exploring options, it also causes the Rocq community to move slower due to technical debt of switching between solutions.
Couldn't you introduce proof relevance as an explicit axiom into a Lean program to solve that particular issue?
Say I'm wanting to formalize a proof. How do I know that what I'm writing is actually a correct formulation?
If it gets more complicated, this problem gets worse. How do I know the thing it is checking is actually what I thought it was supposed to check?
I guess this is a bit like when you write a program and you want to know if it's correct, so you write some tests. But often you realize your tests don't check what you thought.
Trying to formally prove something and then failing is a common way people find out they forgot to add an hypothesis.
Another pitfall is defining some object, but messing up the definitions, such that there's actually no object of that kind. This is addressed by using test objects. So suppose you define what a ring is, then you also prove that real numbers and polynomials are examples of the thing you defined.
I don't see why they would.
If anyone is curious about the phenomenon, the second problem in session 7 at https://incredible.pm/ [ ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) ] is one where the proof is straightforward, but you're unlikely to get to it by just fooling around in the prover.
I love the analogy in David Bessis's wonderful book Mathematica (nothing to do with Wolfram). We all know how to tie our shoes. Now, write in words and symbols to teach someone how you tie your shoes. This is what a proof is.
Often even people with STEM degrees confuse what mathematicians do with the visible product of it - symbols and words on a page. While the formalism of mathematics has immense value for precision, and provides a "serialization language" (to borrow a CS analogy), it would be akin to confusing a Toaster with the Toaster manual, or shoelaces with the instructions.
Personally, at times, I struggled with the dual nature of mathematics; its extreme precision in meaning combined with vague and inconsistent use of symbols is challenging... Especially frustrating when learning something new and some symbols that you think you understand turn out to mean something else; it creates distrust towards maths itself.
https://acornprover.org
The idea is that there's a small AI built into the VS Code extension that will fill in the details of proofs for you. Check it out if you're interested in this sort of thing!
I just released my treatise yesterday, at https://leanpub.com/elementsofprogramming
Elements of Programming presents programming as a mathematical discipline built on structure, logic, and proof. Written in the style of Euclid’s Elements, it defines computation through clear axioms, postulates, and propositions. Each book develops one aspect of programming as a coherent system of reasoning.
Book I establishes identity, transformation, and composition as the foundations of computation.
Book II introduces algebraic structures such as categories, functors, and monads.
Book III unites operational and denotational semantics to show that correctness means equivalence of meaning.
Book IV formalizes capability-based security and verification through invariants and confinement.
Book V connects type theory with formal assurance, explaining how types embody proofs.
Book VI extends these ideas into philosophy and ethics, arguing that software expresses human intention and responsibility.