I don't want to formalize any of my work on mathematics.
-
@johncarlosbaez "It forces you to think about mathematics in the right way." is such a rich statement given the amount of mathematical jank there is in Mathlib.
For example, did you know that (ℝ,+) is technically not a group?
@johncarlosbaez Another classic is of course 1/0 = 0 and its corollary, ζ(1) = (γ - log(4π))/2. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Harmonic/ZetaAsymp.html#riemannZeta_one
-
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)
@johncarlosbaez I take your point on Kevin's comment ( @xenaproject if he logs in and sees this), but a) Kevin likes making hyperbolic public statements to stir the pot b) never forget the journalist and then their editors in the process and c) what Kevin in currently doing is actually stopping to re-think how best to prove FLT, in a way that's novel and more cleanly abstracted and packaged. Perhaps this type of novel re-thinking is not happening every day in number theory, and so it feels really fun. Obviously, category theorists abstract structures and proofs all the time, so this process feels like an absolute no-brainer to us. (Nota Bene: I can also make hyperbolic statements to stir the pot).
Actually looking at the mathematics he is doing currently is really interesting, because it's making it much clearer and leaner (pun not intended), or at least exposing where the really hard core theorems are. Ideally those can subsequently get the same treatment, and people don't just cite a 150-page paper from the 70s or 80s that makes enormous effort to prove a very elementary statement as a black box, but think through if it can be improved.
-
@johncarlosbaez I take your point on Kevin's comment ( @xenaproject if he logs in and sees this), but a) Kevin likes making hyperbolic public statements to stir the pot b) never forget the journalist and then their editors in the process and c) what Kevin in currently doing is actually stopping to re-think how best to prove FLT, in a way that's novel and more cleanly abstracted and packaged. Perhaps this type of novel re-thinking is not happening every day in number theory, and so it feels really fun. Obviously, category theorists abstract structures and proofs all the time, so this process feels like an absolute no-brainer to us. (Nota Bene: I can also make hyperbolic statements to stir the pot).
Actually looking at the mathematics he is doing currently is really interesting, because it's making it much clearer and leaner (pun not intended), or at least exposing where the really hard core theorems are. Ideally those can subsequently get the same treatment, and people don't just cite a 150-page paper from the 70s or 80s that makes enormous effort to prove a very elementary statement as a black box, but think through if it can be improved.
@highergeometer - I'm glad Kevin can have good new ideas about math while formalizing it. I don't want to go that way myself, and I don't want people to feel pressured to do it.
-
@highergeometer - I'm glad Kevin can have good new ideas about math while formalizing it. I don't want to go that way myself, and I don't want people to feel pressured to do it.
@johncarlosbaez @highergeometer I hope we're not in for some kind of 'purity test' era, where if it ain't formally verified, it ain't really mathematics.
-
@johncarlosbaez @highergeometer I hope we're not in for some kind of 'purity test' era, where if it ain't formally verified, it ain't really mathematics.
@RobJLow @johncarlosbaez Well, I heard Kevin talk about problems in the Langlands program where Jim Arthur claimed big results in a number of really meaty "forthcoming" papers and people took his word, and then it turned out there were big problems. In that kind of mathematics, the problem wasn't that it wasn't formalised, but that people are perhaps getting a bit too confident.....
-
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)
@johncarlosbaez I, on the other hand, like using Agda as a blackboard for thinking, just like I like using pen and paper for thinking.
I do believe that mathematics is inherently informal (and that ZFC, MLTT, ETCS etc. are not the ultimate answer to anything, but just distillation of what various people did informally in various different fronts).
This doesn't prevent me from both liking and finding formal mathematics with the aid of a computer useful (for myself - I am not advocating it would be useful for e.g. you).
-
@UweHalfHand - I am not kind of lost without computer-based formalization. Math did perfectly fine without it for millennia.
@johncarlosbaez @UweHalfHand Even before computers, a few mathematicians felt that formalization was a good thing to do. Frege, and Russell and Whitehead, are the most obvious examples; Freek Wiedijk also pointed out how similar Euclid's writing is to the input to a proof assistant.
But of course the important question is consent. Mathematicians should be free to build formal proofs, for a variety of reasons. They should never be required to do so
-
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)
@johncarlosbaez by "formalize" do you mean, "rewrite in a computer-checked proof system"?
The definition of a function as a set of ordered pairs was/is a formalisation, but not computer-checked; it just allows us to state in simpler terms the properties a function needs to have.
-
@johncarlosbaez by "formalize" do you mean, "rewrite in a computer-checked proof system"?
The definition of a function as a set of ordered pairs was/is a formalisation, but not computer-checked; it just allows us to state in simpler terms the properties a function needs to have.
@ActiveMouse - yes, that's what I mean. I grew up in the era where it had a different meaning, and that meaning is still common. but now a lot of mathematicians use "formalize" to mean "prove using a proof assistant such as Lean or Rocq".
https://mathoverflow.net/questions/378473/what-is-the-endgoal-of-formalising-mathematics
-
@dougmerritt - You got my point. Working in Lean or any computer system for formalization, you need to submit to the already laid down approaches, or spend a lot of time rewriting things.
I added a quote from Kevin Buzzard to emphasize the problem:
Kevin Buzzard says "It [formalization? Lean?] forces you to think about mathematics in the right way."
But there's no such thing as "the" right way!
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.
-
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
Yes, well, moving past John's point:Easier said than done. Current things like Lean are lots better than the systems of years ago, but -- do you have any specific ideas?
I used to follow that area of technology, but I somewhat burned out on it. For now, Terry Tao et al is getting good mileage out of Lean.
I suppose there's some analogy with the period of shift from Peano axioms to ZFC and beyond.
-
@maxpool @johncarlosbaez
Yes, well, moving past John's point:Easier said than done. Current things like Lean are lots better than the systems of years ago, but -- do you have any specific ideas?
I used to follow that area of technology, but I somewhat burned out on it. For now, Terry Tao et al is getting good mileage out of Lean.
I suppose there's some analogy with the period of shift from Peano axioms to ZFC and beyond.
@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.
-
@dougmerritt - You got my point. Working in Lean or any computer system for formalization, you need to submit to the already laid down approaches, or spend a lot of time rewriting things.
I added a quote from Kevin Buzzard to emphasize the problem:
Kevin Buzzard says "It [formalization? Lean?] forces you to think about mathematics in the right way."
But there's no such thing as "the" right way!
@johncarlosbaez @dougmerritt Formalism exists to provide rigor and math without rigor isn't really math. But you are right that rigor can be developed in multiple ways, also that computer verified formulations are not as rich as the math literature at large.
I wonder if generative AI will lead to richer computer verified formulations though. I keep hearing about how the AI assisted with a problem that people find interesting. What happens when we train an AI to recognize results that people find interesting and tell it to go find new results of that sort?
-
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
