I don't want to formalize any of my work on mathematics.
-
@johncarlosbaez Aye! It's depressing to see these tools flip to being the new orthodoxy in no time flat. I'm both impressed and depressed by Lean. I think we can do better, but we may not be allowed to.
@johncarlosbaez And yes, ownership of "the right way" is a political project which need not lie at the heart of this innovation, but apparently does.
-
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 Am I right in understanding that you don’t object to your work being formalised, you just don’t want to do it yourself?
-
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
> formalization tends to impose consensusI'm not sure people are getting your point. The way I see it, formalization tends to make people subconsciously think in terms of The One And Only Truth -- and thus consensus.
But we know that in mathematics, there are always other paths, and truths follow from axioms / axiom schemas, which themselves can vary.
Or perhaps I'm missing your point, too.
-
@johncarlosbaez Am I right in understanding that you don’t object to your work being formalised, you just don’t want to do it yourself?
@richardelwes - I don't object to my work being formalized.
I think a lot of people are spending time and money on formalization which they could better spend on something else. I encourage pluralism, so I expect that lots of mathematicians will do things that are not to my taste, including this. But bandwagons tend to decrease pluralism - especially ones where you get "locked in" to a specific software package.
-
@johncarlosbaez
> formalization tends to impose consensusI'm not sure people are getting your point. The way I see it, formalization tends to make people subconsciously think in terms of The One And Only Truth -- and thus consensus.
But we know that in mathematics, there are always other paths, and truths follow from axioms / axiom schemas, which themselves can vary.
Or perhaps I'm missing your point, too.
@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 And yes, ownership of "the right way" is a political project which need not lie at the heart of this innovation, but apparently does.
@pigworker - Elsevier must already be drooling, thinking of a future where you need to formalize your theorems to publish them... and you need to formalize them in a system owned by Elsevier. We're not there yet, but formal systems of math always have "economies of scale" that foster conformity, and once everyone is using Lean, someone will figure out a way to charge for it.
-
@johncarlosbaez I think it takes both kinds, the explorers and the formalizers. Each would be kind of lost without the other.
@UweHalfHand - I am not kind of lost without computer-based formalization. Math did perfectly fine without it for millennia.
-
@pigworker - Elsevier must already be drooling, thinking of a future where you need to formalize your theorems to publish them... and you need to formalize them in a system owned by Elsevier. We're not there yet, but formal systems of math always have "economies of scale" that foster conformity, and once everyone is using Lean, someone will figure out a way to charge for it.
@johncarlosbaez And the ACM are very nearly there!
The thing is that to have any credibility, the proof rules need to be open and the checking procedure needs to be independently reimplementable.
Lean's is. And it's broken, but not in a way that says yes to wrong things.
-
@UweHalfHand - I am not kind of lost without computer-based formalization. Math did perfectly fine without it for millennia.
@johncarlosbaez True, but even millennia ago there were explorers and builders. I would guess that if you had been born 2000 years ago, you’d still be an explorer…
-
@johncarlosbaez True, but even millennia ago there were explorers and builders. I would guess that if you had been born 2000 years ago, you’d still be an explorer…
@UweHalfHand - yes, I'm an explorer. The particular challenge right now, to be really specific, is that there's increasing pressure on mathematicians to formalize our work in Lean.
-
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 "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 "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?
@jameshanson - because that ordered pair doesn't include the additive identity, or inverses, or something?
-
@jameshanson - because that ordered pair doesn't include the additive identity, or inverses, or something?
@johncarlosbaez No, it's an additive group, which is a distinct thing from a group (which happens to be defined in the same way but with different notation).
-
@johncarlosbaez No, it's an additive group, which is a distinct thing from a group (which happens to be defined in the same way but with different notation).
@jameshanson - wow, so there's no type coercion that makes every additive group count as a group?
-
@jameshanson - wow, so there's no type coercion that makes every additive group count as a group?
@johncarlosbaez There's a tactic/script that converts proofs of statements for groups to the corresponding statement for additive groups, but it's not yet seamless.
-
@jameshanson - wow, so there's no type coercion that makes every additive group count as a group?
@johncarlosbaez @jameshanson There is (there has to be, since you just take the data and reassemble it under different notation), but I heavily heavily advise you to not use it because it would be miserable under mathlib's system of conventions. Instead people just duplicate every single theorem proved about groups.
Worth noting that the Rocq proof assistant uses another approach called the Hierarchy Builder where they don't need this duplication. -
@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.
