> This is not separate groups of two or three mathematicians each belaboring on a paper on their own. It's not like that. This is not anymore the medieval mathematician's guild--which is how mathematics is still organized today. This is a post-industrial division of labor. It is completely new. It's a math hive. It's exciting, and we haven't seen this sort of thing before, and I think it's going to change mathematics.
Change itself is speeding up. We are going to zoom through the hive era and jump straight into AI era, where 99%, if not more, of the heavy lifting will be done by the machines. The centaur era is rather close ahead. Beyond that, the hope is there will be some room left for humans, but I won't take a long term bet.
I think it is the future. Writing a mathematical proof is writing a computer program. I think it is common to see lots of lets say hacky, untyped work, like some janky bash script, that takes you on some adventure, that you have to spend extra work exploring. Imagine instead reading some declarative program. Everything formalised, use of higher order functions/constructs when appropriate that encapsulate important generalisable ideas (eg in the programming example using "map" when you want to loop over some list). Hacky stuff is fine for exploration and experimentation. But something for publication should be clear. You could use engineering principles, optimising your proofs for readability and efficiency, version control. Seems like it is the future.
I am of the opinion that mathematics is very much a human endeavor. Writing a proof is to convince other mathematicians that it’s true. While formalized mathematics is one such technique, I don’t believe it will replace how mathematics is generally done. Writing a program is something different entirely.
One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.
I want to second this. I started working on a project in Lean only last December. Since then, I've made several contributions to the mathlib github repo - the first time I've contributed to open source despite wanting to get into it for a few years. The Zulip forum https://leanprover.zulipchat.com/# is very welcoming and responsive to questions. If you're interested in mathematics and you want to contribute to the growing hivemind working on this kind of thing, I highly encourage you to learn Lean and join this community.
I'm not sure if I would recommend that, given that Lean has less support for constructive math than some existing systems, and constructive math can be very convenient for proving stuff about programs/computations.
I'm wondering about the 'searchability' or canonicalization of such a theorem library. How do you make sure there's no duplicate work? How do you index the thing? Can you match and input / output proposition and look through the whole database and have it find all related theorems?
I'm thinking 'automatic lemma matching' for software verification. e.g. In a SPARK proof you might need to use a lemma [0]. If you formal math education is lacking or maybe your theorem library is not encyclopedic, you might want suggestions from 'the hive'...
How does Lean compare to Coq? And which one would be preferable for non-mathematicians trying to learn more about math? Which one would be better if you come from a software background and want to do formal verification for parts of your programs?
There's an excellent online book that introduces Coq and how to use it for verification of programs: https://softwarefoundations.cis.upenn.edu/. There's also a more advanced book, http://adam.chlipala.net/cpdt/, that goes into more detail. In comparison, Lean has little teaching material for formal verification of programs.
This is only a partial answer, but my understanding is that Lean is really not meant for software verification work. That's very much Coq's alley.
I'm much less certain of this, but I think Lean is better for non-mathematicians trying to learn more about math --- provided, that is, that you're set on playing with a proof assistant. I'm not sure I'd recommend that.
Sorry to be the buzzkill here, but I'll say what needs to be said. Computers are decades away from being able to formalize any serious mathematical results, and "formalized mathematics" is a fancy term for "formal methods in computer science".
I've worked for a good numbers of years in the US software industry as a compiler engineer, and am a Mathematics masters student now. I've played with proof assistants extensively, and in particular I'm currently working on a paper to formalize semi-cubical sets in Coq. Working with Coq has been most painful, and it requires spoon-feeding for verifying even the simplest results. Worst of all, it's riddled with bugs, and I'm constantly astounded at how stupid it is.
That said, Lean is a much newer proof assistant, and while it offers some nice conveniences, it will take at least a decade before its power is comparable to Coq.
Mathematics is a solitary activity for good reason. Much of the work happens on pen-and-paper, and it takes months of toil to prove a result. No serious mathematician is going to go through the pain of encoding her proof in a proof assistant, and spoon-feeding it to verify every little result.
What's the news? That several computer scientists in the area are doing the work of formalizing simple mathematical results in Lean. Don't mistake Lean for some ground-breaking new technology; sure, it has a thriving community, and offers many conveniences, but the level of abstraction it offers isn't even close to the level of abstraction that my subject offers (I study stable ∞-categories).
Sure, if you want to do the thankless work of formalizing well-known results from group theory, ring theory, or vector spaces in Lean, be my guest. But don't be under the illusion that it's going to change the way mathematics is fundamentally done. The work is comparable to type-setting a document, except that it's a LOT more painful.
"I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research." Peter Scholze [1].
Nope. You clearly are not up to date on what is happening right now. With leading edge mathematics being defined and proven correct in Lean, in a collaboration of mathematicians and computer scientists.
[+] [-] dwrensha|4 years ago|reply
> This is not separate groups of two or three mathematicians each belaboring on a paper on their own. It's not like that. This is not anymore the medieval mathematician's guild--which is how mathematics is still organized today. This is a post-industrial division of labor. It is completely new. It's a math hive. It's exciting, and we haven't seen this sort of thing before, and I think it's going to change mathematics.
[+] [-] bookofsand|4 years ago|reply
[+] [-] pathsjs|4 years ago|reply
[+] [-] foxes|4 years ago|reply
Disclaimer I have written many "hacky" proofs.
[+] [-] bmitc|4 years ago|reply
One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.
[+] [-] outlace|4 years ago|reply
[+] [-] fogof|4 years ago|reply
[+] [-] mbrodersen|4 years ago|reply
[+] [-] zozbot234|4 years ago|reply
[+] [-] pohl|4 years ago|reply
https://www.youtube.com/watch?v=aSU0xBGfkfg
[+] [-] touisteur|4 years ago|reply
I'm thinking 'automatic lemma matching' for software verification. e.g. In a SPARK proof you might need to use a lemma [0]. If you formal math education is lacking or maybe your theorem library is not encyclopedic, you might want suggestions from 'the hive'...
[0] https://blog.adacore.com/gnatprove-tips-and-tricks-using-the...
[+] [-] alimw|4 years ago|reply
https://leanprover-community.github.io/mathlib_docs/tactics....
[+] [-] elcapitan|4 years ago|reply
[+] [-] logicchains|4 years ago|reply
[+] [-] srl|4 years ago|reply
I'm much less certain of this, but I think Lean is better for non-mathematicians trying to learn more about math --- provided, that is, that you're set on playing with a proof assistant. I'm not sure I'd recommend that.
[+] [-] artagnon|4 years ago|reply
I've worked for a good numbers of years in the US software industry as a compiler engineer, and am a Mathematics masters student now. I've played with proof assistants extensively, and in particular I'm currently working on a paper to formalize semi-cubical sets in Coq. Working with Coq has been most painful, and it requires spoon-feeding for verifying even the simplest results. Worst of all, it's riddled with bugs, and I'm constantly astounded at how stupid it is.
That said, Lean is a much newer proof assistant, and while it offers some nice conveniences, it will take at least a decade before its power is comparable to Coq.
Mathematics is a solitary activity for good reason. Much of the work happens on pen-and-paper, and it takes months of toil to prove a result. No serious mathematician is going to go through the pain of encoding her proof in a proof assistant, and spoon-feeding it to verify every little result.
What's the news? That several computer scientists in the area are doing the work of formalizing simple mathematical results in Lean. Don't mistake Lean for some ground-breaking new technology; sure, it has a thriving community, and offers many conveniences, but the level of abstraction it offers isn't even close to the level of abstraction that my subject offers (I study stable ∞-categories).
Sure, if you want to do the thankless work of formalizing well-known results from group theory, ring theory, or vector spaces in Lean, be my guest. But don't be under the illusion that it's going to change the way mathematics is fundamentally done. The work is comparable to type-setting a document, except that it's a LOT more painful.
[+] [-] mathgenius|4 years ago|reply
"I find it absolutely insane that interactive proof assistants are now at the level that within a very reasonable time span they can formally verify difficult original research." Peter Scholze [1].
[1] https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...
[+] [-] ukj|4 years ago|reply
You know what you want to express - you don't know how to express it in a way that your interlocutor will understand.
Whether your interlocutor is a computer speaking Lean, or a human speaking your non-native tongue.
All the benefits are on the other side of the learning curve.
[+] [-] mbrodersen|4 years ago|reply