I don't want to formalize any of my work on mathematics.
-
I don't want to formalize any of my work on mathematics. First because, as Emily Riehl notes, formalization tends to impose consensus. And second, because I find it boring. It steals time from creative thought to nail things down with more rigidity than I need or want.
Kevin Buzzard says "It forces you to think about mathematics in the right way." But there is no such thing as "the" right way to think about mathematics - and certainly not one that can be forced on us.
In Math, Rigor Is Vital. But Are Digitized Proofs Taking It Too Far? | Quanta Magazine
The quest to make mathematics rigorous has a long and spotty history — one mathematicians can learn from as they push to formalize everything in the computer program Lean.
Quanta Magazine (www.quantamagazine.org)
I agree,
Many years ago, um, last century...lol I stumbled over Vedic Mathematics and had all my illusions shattered about there being a right way to do maths.
It's so utterly different to anything I was taught in school, and yet it's easier and it works
-
@pigworker - Good! But to get anywhere with formalizing big theorems in Lean, the topic mainly discussed in this article, you're pressured to work within that system.
@johncarlosbaez @pigworker Or wait for a year or two, and an AI agent will do everything from the ground up, bypassing/recreating mathlib.
-
@dougmerritt - I follow some people who are into formalization, logic and type theory more sophisticated than Lean: @MartinEscardo, @andrejbauer, @pigworker and @JacquesC2 leap to mind. They're the ones to answer your question.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I can give it a try.
First: Lean and Mathlib embody a very particular philosophy. Lean 4 aims to be "practical", which is mainly code for 'allowing lots of automation'. It cuts some serious corners to achieve that (others have written about that at length). Mathlib chooses to be a 'monorepo' (which is laudable indeed IMHO). The combination of Lean's technology choices and the monorepo decision is what forces 'consensus'.
-
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I can give it a try.
First: Lean and Mathlib embody a very particular philosophy. Lean 4 aims to be "practical", which is mainly code for 'allowing lots of automation'. It cuts some serious corners to achieve that (others have written about that at length). Mathlib chooses to be a 'monorepo' (which is laudable indeed IMHO). The combination of Lean's technology choices and the monorepo decision is what forces 'consensus'.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I would compare Lean+Mathlib to Java rather than FORTRAN and Pascal: Java is just as boring a PL as others, but it is a much stronger ecosystem (IDEs, libraries, tutorials, etc). Thus developers have a much better experience using Lean+Mathlib and the surrounding ecosystem (blueprints are super cool, as just one example).
In my mind, it is purely 'social forces' that has made and is making Lean+Mathlib the apparent winner. And that has snowballed - almost to the point of smothering everything else, which is extremely dangerous for innovation.
-
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I would compare Lean+Mathlib to Java rather than FORTRAN and Pascal: Java is just as boring a PL as others, but it is a much stronger ecosystem (IDEs, libraries, tutorials, etc). Thus developers have a much better experience using Lean+Mathlib and the surrounding ecosystem (blueprints are super cool, as just one example).
In my mind, it is purely 'social forces' that has made and is making Lean+Mathlib the apparent winner. And that has snowballed - almost to the point of smothering everything else, which is extremely dangerous for innovation.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker Are there specific ideas around to make things better? Absolutely! Heck, there are old ideas (Epigram comes to mind, but even Automath has not been fully mined yet) that are still not implemented.
I will continue later - need to attend to other things right now.
-
@dougmerritt - I follow some people who are into formalization, logic and type theory more sophisticated than Lean: @MartinEscardo, @andrejbauer, @pigworker and @JacquesC2 leap to mind. They're the ones to answer your question.
@johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker Somewhat unexpectedly, I find myself on the same side as @xenaproject on this one, I suppose because I read "the right way" differently from @johncarlosbaez
Formalized mathematics makes us think "the right way" in the sense that it requires mental hygiene, it encourages better organization, it invites abstraction, and it demands honesty.
Formalized mathematics does not at all impose "One and Only Truth", nor does it "nail things down with rigidity" or "impose concensus". Those are impressions that an outsider might get by observing how, for the first time, some mathematicians have banded together to produce the largest library of formalized mathematics in history. But let's be honest, it's miniscule.
Even within a single proof assistant, there is a great deal of freedom of exploration of foundations, and there are many different ways to formalize any given topic. Not to mention that having several proof assistants, each peddling its own foundation, has only contributed to plurality of mathematical thought.
Current tools are relatively immature and do indeed steal time from creative thought to some degree, although people who are proficient in their use regularly explore mathematics with proof assistants (for example @MartinEscardo and myself), testifying to their creative potential.
Finally, any fear that Mathlib and Lean will dominate mathematical thought, or even just formalized mathematics, is a hollow one. Mathlib will soon be left in the dust of history, but it will always be remembered as the project that brought formalized mathematics from the fringes of computer science to the mainstream of mathematics.
-
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I would compare Lean+Mathlib to Java rather than FORTRAN and Pascal: Java is just as boring a PL as others, but it is a much stronger ecosystem (IDEs, libraries, tutorials, etc). Thus developers have a much better experience using Lean+Mathlib and the surrounding ecosystem (blueprints are super cool, as just one example).
In my mind, it is purely 'social forces' that has made and is making Lean+Mathlib the apparent winner. And that has snowballed - almost to the point of smothering everything else, which is extremely dangerous for innovation.
@JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker Lean is worse, but, infamously, https://en.wikipedia.org/wiki/Worse_is_better
-
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker Are there specific ideas around to make things better? Absolutely! Heck, there are old ideas (Epigram comes to mind, but even Automath has not been fully mined yet) that are still not implemented.
I will continue later - need to attend to other things right now.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I agree with @andrejbauer 's take, including his skepticism of my comments on Lean choking things off: we're talking (implicitly) about different time scales. I'm witnessing a current funnelling of resources, which will cause short-term pain. Indeed this is unlikely to remain 'forever'.
-
@johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker Somewhat unexpectedly, I find myself on the same side as @xenaproject on this one, I suppose because I read "the right way" differently from @johncarlosbaez
Formalized mathematics makes us think "the right way" in the sense that it requires mental hygiene, it encourages better organization, it invites abstraction, and it demands honesty.
Formalized mathematics does not at all impose "One and Only Truth", nor does it "nail things down with rigidity" or "impose concensus". Those are impressions that an outsider might get by observing how, for the first time, some mathematicians have banded together to produce the largest library of formalized mathematics in history. But let's be honest, it's miniscule.
Even within a single proof assistant, there is a great deal of freedom of exploration of foundations, and there are many different ways to formalize any given topic. Not to mention that having several proof assistants, each peddling its own foundation, has only contributed to plurality of mathematical thought.
Current tools are relatively immature and do indeed steal time from creative thought to some degree, although people who are proficient in their use regularly explore mathematics with proof assistants (for example @MartinEscardo and myself), testifying to their creative potential.
Finally, any fear that Mathlib and Lean will dominate mathematical thought, or even just formalized mathematics, is a hollow one. Mathlib will soon be left in the dust of history, but it will always be remembered as the project that brought formalized mathematics from the fringes of computer science to the mainstream of mathematics.
@andrejbauer @johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
> Mathlib will soon be left in the dust of history
Totally. Even on a technical level, having one dominant math library does not signal the degradation of the field. The other day I learned about [1] for automatically porting Lean definitions to Rocq. This project now gets to start with targeting a big, consistent library of formalized math, and even if the Mathlib people won't care that's still an great thing for the field!
-
@andrejbauer @johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
> Mathlib will soon be left in the dust of history
Totally. Even on a technical level, having one dominant math library does not signal the degradation of the field. The other day I learned about [1] for automatically porting Lean definitions to Rocq. This project now gets to start with targeting a big, consistent library of formalized math, and even if the Mathlib people won't care that's still an great thing for the field!
@markusde Have you seen what can be done with this nowadays https://theoremlabs.com/blog/lf-lean/ ?
-
@markusde Have you seen what can be done with this nowadays https://theoremlabs.com/blog/lf-lean/ ?
@mevenlennonbertrand I've read that article rocq-lean-import was the only interesting thing in it
-
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I agree with @andrejbauer 's take, including his skepticism of my comments on Lean choking things off: we're talking (implicitly) about different time scales. I'm witnessing a current funnelling of resources, which will cause short-term pain. Indeed this is unlikely to remain 'forever'.
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker On the more optimistic side:
- there is a lot of structure to mathematics, which is currently not very well leveraged, i.e. Universal Algebra and its many generalizations. But people are working on that (myself included).
- regardless of what some say, there is a lot of 'computational mathematics', which is currently not well supported by any system, and essentially eschewed by Lean+Mathlib. That requires thinking differently. Again, people are working on that.
- in fact, there is quite a bit more to math in general -- see the Tetrapod approach for one.
To me, what's really missing are experts in designing UX having a solid look at mechanized mathematics tools. For that to bear fruit, experts in requirements analysis need to better understand the full "mathematics workflow" -- where proof is just one small aspect. It might indeed be the most time-consuming part, but it is not necessarily where the most value lies. [See LaTeX as an example of a strong value proposition that has completely changed the practice of mathematics, but in a surreptitious way, as it is essentially invisible wrt "mathematical thought". Its effect is no less important.]
-
@mevenlennonbertrand I've read that article rocq-lean-import was the only interesting thing in it
@mevenlennonbertrand Porting a bunch of theorem statements and then saying it's "verified" is... bold
-
This is just the beginning.
Current systems are the FORTRAN and Pascal of proof systems; they are for building pyramids--imposing, breathtaking, static structures built by armies pushing heavy blocks into place.
What we need is for someone to invent the Lisp of proof systems. Something that helps individuals to think new thoughts.
@maxpool @johncarlosbaez @dougmerritt
I mean, Maxima was literally written in the late 60's in LISP to give people help thinking new thoughts (beyond what they could reasonably accurately do by hand)
-
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker On the more optimistic side:
- there is a lot of structure to mathematics, which is currently not very well leveraged, i.e. Universal Algebra and its many generalizations. But people are working on that (myself included).
- regardless of what some say, there is a lot of 'computational mathematics', which is currently not well supported by any system, and essentially eschewed by Lean+Mathlib. That requires thinking differently. Again, people are working on that.
- in fact, there is quite a bit more to math in general -- see the Tetrapod approach for one.
To me, what's really missing are experts in designing UX having a solid look at mechanized mathematics tools. For that to bear fruit, experts in requirements analysis need to better understand the full "mathematics workflow" -- where proof is just one small aspect. It might indeed be the most time-consuming part, but it is not necessarily where the most value lies. [See LaTeX as an example of a strong value proposition that has completely changed the practice of mathematics, but in a surreptitious way, as it is essentially invisible wrt "mathematical thought". Its effect is no less important.]
@johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker On a more personal note, I'm strongly enjoying that all this work on proof assistants is forcing many many more people to think about meta-mathematics (and I don't mean just logic here, but all aspects of 'mathematics' as a subject of study.) /end
-
@JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker Lean is worse, but, infamously, https://en.wikipedia.org/wiki/Worse_is_better
@markusde @JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker it is absolutely wild that lean is (unironically?) being used as an example of worse is better.
-
@mevenlennonbertrand Porting a bunch of theorem statements and then saying it's "verified" is... bold
@markusde Isn't the point that having a proof on the Rocq side + a proof that the statement translated from Lean is equivalent to the Rocq one makes it reasonable to not translate the whole proof? I find it not quite fully satisfying, but the approach sounds honestly very reasonable to me.
-
@johncarlosbaez @dougmerritt @MartinEscardo @JacquesC2 @pigworker Somewhat unexpectedly, I find myself on the same side as @xenaproject on this one, I suppose because I read "the right way" differently from @johncarlosbaez
Formalized mathematics makes us think "the right way" in the sense that it requires mental hygiene, it encourages better organization, it invites abstraction, and it demands honesty.
Formalized mathematics does not at all impose "One and Only Truth", nor does it "nail things down with rigidity" or "impose concensus". Those are impressions that an outsider might get by observing how, for the first time, some mathematicians have banded together to produce the largest library of formalized mathematics in history. But let's be honest, it's miniscule.
Even within a single proof assistant, there is a great deal of freedom of exploration of foundations, and there are many different ways to formalize any given topic. Not to mention that having several proof assistants, each peddling its own foundation, has only contributed to plurality of mathematical thought.
Current tools are relatively immature and do indeed steal time from creative thought to some degree, although people who are proficient in their use regularly explore mathematics with proof assistants (for example @MartinEscardo and myself), testifying to their creative potential.
Finally, any fear that Mathlib and Lean will dominate mathematical thought, or even just formalized mathematics, is a hollow one. Mathlib will soon be left in the dust of history, but it will always be remembered as the project that brought formalized mathematics from the fringes of computer science to the mainstream of mathematics.
@andrejbauer why will Mathlib soon be left in the dust of history?
-
@markusde @JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker it is absolutely wild that lean is (unironically?) being used as an example of worse is better.
@sandmouth @JacquesC2 @johncarlosbaez @dougmerritt @MartinEscardo @andrejbauer @pigworker I mean... I'm serious about it. I've seen really convincing arguments from type theorists about how Lean's type theory is missing features (transitive defeq, decidable defeq, consistency with various axioms). Some of the missing features are just mistakes, but some of them are made in the interest of usability or simplicity or speed or whatnot.
Personally, I don't think has decisively shown that these things _aren't_ in conflict, so that is the sense in which I see Lean as worse and better. Idk, just my opinion.
-
@markusde Isn't the point that having a proof on the Rocq side + a proof that the statement translated from Lean is equivalent to the Rocq one makes it reasonable to not translate the whole proof? I find it not quite fully satisfying, but the approach sounds honestly very reasonable to me.
@mevenlennonbertrand I guess I don't understand their article. I can see how you'd verify that a round-trip Rocq translation is correct (ie. identical) but doesn't that say nothing about the correctness of your Lean code when linked against other Lean code?
Adding to the TCB is not that interesting to me.
