I don't want to formalize any of my work on mathematics.
-
@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.
-
@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.
@markusde I guess it says that :
- the definitions give you objects which once roundtripped are isomorphic to the original ones ; not the best specification, but rather solid (it rules out everything being unit or something, and is especially fine if you also translate the various operations/basic proofs which encode that they behave the way one expects)
- the lemmas you admit on the Lean side are logically equivalent (up to Lean -> Rocq translation) to ones which are proven, which to me makes them very reasonable to assumeOf course that brings the Lean -> Rocq translation to the TCB, as well as Rocq, but I still feel this is ok?
And I don't see how the liking with other Lean code changes anything, you can treat the translated code as some sort of opaque module with a bunch of definitions and proofs and use that opaquely, just as you would any other Lean module? Except in this one the proofs are not there, they're on the Rocq side
-
@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 @JacquesC2 @pigworker @xenaproject
It is not inconceivable that one day in the not-too-distant future, proof assistants will be able to "understand" proofs written in sufficiently careful, informal, mathematical vernacular and translate it to a suitable formal language.
And this formal language doesn't need to be fixed. The mathematician just chooses a foundation, or, in case they don't care, they let the proof assistant choose a suitable one for the informal (but hopefully rigorous) mathematics at hand.
I don't mean AI, but people are certainly trying this with so-called AI nowadays (personally, I think this is the wrong approach, but **I don't want** this to become the subject of discussion here).
In any case, a person will need to check that the definitions and the statements of the theorems and constructions are correctly translated (*). Then the formal proofs obtained from informal proofs don't need to be checked by people.
(*) At least at the beginning. For example, we now trust that C compilers produce correct machine code and don't check it ourselves.
In any case, all of the above can happen only step by step, and currently we are at an important step, I think, where the first were in the 1960's by de Bruijn.
As I said before, I use proof assistants as smart blackboards. If I could get interactive help while I write in mathematical vernacular, I would immediately adopt this incredible new proof assistant.
And, I repeat, I don't mean the kind of non-help I get from ChatGPT, Gemini, Claude, DeepSeek, or what-you-have - I feel I help them rather than the other way round.
I mean the kind of help I already get in non-AI-based proof assistants
-
@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.....
@highergeometer @RobJLow - soon we will give mathematicians brain implants that make their glasses flash a red warning light when they state any result that hasn't been formalized, and this problem will be solved.
-
@markusde I guess it says that :
- the definitions give you objects which once roundtripped are isomorphic to the original ones ; not the best specification, but rather solid (it rules out everything being unit or something, and is especially fine if you also translate the various operations/basic proofs which encode that they behave the way one expects)
- the lemmas you admit on the Lean side are logically equivalent (up to Lean -> Rocq translation) to ones which are proven, which to me makes them very reasonable to assumeOf course that brings the Lean -> Rocq translation to the TCB, as well as Rocq, but I still feel this is ok?
And I don't see how the liking with other Lean code changes anything, you can treat the translated code as some sort of opaque module with a bunch of definitions and proofs and use that opaquely, just as you would any other Lean module? Except in this one the proofs are not there, they're on the Rocq side
@mevenlennonbertrand I am not comfortable with having that added to the TCB, so, getting back to my initial comment I would not call it "verified" given how easy it is to get wrong! Their article brings up several differences between the Lean and Rocq type theory... can they be sure they caught them all? Apply their technique to a proof development in a different language that is not classically valid. What goes wrong? What if all the definitions they choose to port are round-trippable but some of them are not true????
The answer to this rhetorical question is probably that "they wouldn't trust that" but I think the translation is subtle enough that I wouldn't put faith in it.
-
@mevenlennonbertrand I am not comfortable with having that added to the TCB, so, getting back to my initial comment I would not call it "verified" given how easy it is to get wrong! Their article brings up several differences between the Lean and Rocq type theory... can they be sure they caught them all? Apply their technique to a proof development in a different language that is not classically valid. What goes wrong? What if all the definitions they choose to port are round-trippable but some of them are not true????
The answer to this rhetorical question is probably that "they wouldn't trust that" but I think the translation is subtle enough that I wouldn't put faith in it.
@mevenlennonbertrand
There could be engineering value in this as a starting point to porting complete proofs, though ofc that is not demonstrated until you actually do the proofs. For example, I would consider a tool that translates Rocq canonical structures hierarchies into it's type-theoretically similar Lean code _wrong_, because in Lean, you want to use typeclasses 99% of the time. I'll reserve judgement until they fill in the gaps. -
@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
It is not inconceivable that one day in the not-too-distant future, proof assistants will be able to "understand" proofs written in sufficiently careful, informal, mathematical vernacular and translate it to a suitable formal language.
And this formal language doesn't need to be fixed. The mathematician just chooses a foundation, or, in case they don't care, they let the proof assistant choose a suitable one for the informal (but hopefully rigorous) mathematics at hand.
I don't mean AI, but people are certainly trying this with so-called AI nowadays (personally, I think this is the wrong approach, but **I don't want** this to become the subject of discussion here).
In any case, a person will need to check that the definitions and the statements of the theorems and constructions are correctly translated (*). Then the formal proofs obtained from informal proofs don't need to be checked by people.
(*) At least at the beginning. For example, we now trust that C compilers produce correct machine code and don't check it ourselves.
In any case, all of the above can happen only step by step, and currently we are at an important step, I think, where the first were in the 1960's by de Bruijn.
As I said before, I use proof assistants as smart blackboards. If I could get interactive help while I write in mathematical vernacular, I would immediately adopt this incredible new proof assistant.
And, I repeat, I don't mean the kind of non-help I get from ChatGPT, Gemini, Claude, DeepSeek, or what-you-have - I feel I help them rather than the other way round.
I mean the kind of help I already get in non-AI-based proof assistants
@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
And let's not forget.
Everybody here and elsewhere says Lean, Lean, Lean.
Before Lean, we have a long list of successful proof assistants.
In particular, Lean is based on both Rocq (formerly known as Coq) *and* the foundations of Rocq, namely the "calculus of inductive constructions".
Lean is Rocq with a new skin and a new community, based on the very same foundations and approaches.
I can say this without any conflict of interest, because I prefer Agda instead, which is based on a different foundation, namely MLTT.
And this preference is based on the kind of mathematics *I* prefer (constructive, suitable for being interpreted in any (infinity) topos, in the (in)formal language of HoTT/UF).
-
@andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
And let's not forget.
Everybody here and elsewhere says Lean, Lean, Lean.
Before Lean, we have a long list of successful proof assistants.
In particular, Lean is based on both Rocq (formerly known as Coq) *and* the foundations of Rocq, namely the "calculus of inductive constructions".
Lean is Rocq with a new skin and a new community, based on the very same foundations and approaches.
I can say this without any conflict of interest, because I prefer Agda instead, which is based on a different foundation, namely MLTT.
And this preference is based on the kind of mathematics *I* prefer (constructive, suitable for being interpreted in any (infinity) topos, in the (in)formal language of HoTT/UF).
@MartinEscardo @andrejbauer @johncarlosbaez @dougmerritt @JacquesC2 @pigworker @xenaproject
while I mostly agree, I think Lean also inherits many ideas from Isabelle, not about foundations at all but instead about things like proof search and automation.
-
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 What I find interesting about this is that during my mathematical training I was taught there is but one way to do mathematics: ZFC. When I got to meet people working in proof verification I learnt that there is a whole world of formalisms out there.
-
@highergeometer @RobJLow - soon we will give mathematicians brain implants that make their glasses flash a red warning light when they state any result that hasn't been formalized, and this problem will be solved.
@johncarlosbaez your suggestion made me think of this Far Side cartoon:
https://static1.cbrimages.com/wordpress/wp-content/uploads/2023/05/the-far-side-didnt-wash-hands.jpg -
@johncarlosbaez your suggestion made me think of this Far Side cartoon:
https://static1.cbrimages.com/wordpress/wp-content/uploads/2023/05/the-far-side-didnt-wash-hands.jpg@johncarlosbaez uncomfortable in many ways, yes.
-
@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 - "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."
I did read it differently. I was really worrying that Kevin meant formalizing mathematics in *Lean* forces us to think the right way. But in fact I don't think formalizing mathematics at all makes us think "the" right way. It has good sides, which you mention, so it's *a* right way to do mathematics. But it also has bad sides. Mostly, it doesn't encourage radical new ideas that don't fit well in existing formalisms. Newton, Euler, Dirac, Feynman and Witten are just a few of the most prominent people who broke out of existing frameworks, didn't think formally, and did work that led to a huge growth of mathematics. If you say "those people are physicists, not mathematicians", then you're slicing disciplines differently than me. I find their ideas more mathematically interesting than most mathematics that fits into existing frameworks.
@dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
-
@andrejbauer - "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."
I did read it differently. I was really worrying that Kevin meant formalizing mathematics in *Lean* forces us to think the right way. But in fact I don't think formalizing mathematics at all makes us think "the" right way. It has good sides, which you mention, so it's *a* right way to do mathematics. But it also has bad sides. Mostly, it doesn't encourage radical new ideas that don't fit well in existing formalisms. Newton, Euler, Dirac, Feynman and Witten are just a few of the most prominent people who broke out of existing frameworks, didn't think formally, and did work that led to a huge growth of mathematics. If you say "those people are physicists, not mathematicians", then you're slicing disciplines differently than me. I find their ideas more mathematically interesting than most mathematics that fits into existing frameworks.
@dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
I don't agree that working with a proof assistant will reduce the chance that we'll come up with radical new ideas.
It's not at all difficult for me to picture someone like Grothendieck, who also broke out of many existing formalisms, writing his own library from scratch in order to express his ideas -- In many ways this is exactly what he did! Though of course he (and his collaborators) wrote a long series of books rather than writing a long list of agda/lean/etc files.
In fact, it's quite easy for me to picture someone like Grothendieck writing their own theorem prover! Perhaps in that world EGA/SGA would look much more like the currently-under-development synthetic algebraic geometry, formalized in a proof assistant that's custom made for arguments in the (big) zariski or etale topos.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
-
@andrejbauer - "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."
I did read it differently. I was really worrying that Kevin meant formalizing mathematics in *Lean* forces us to think the right way. But in fact I don't think formalizing mathematics at all makes us think "the" right way. It has good sides, which you mention, so it's *a* right way to do mathematics. But it also has bad sides. Mostly, it doesn't encourage radical new ideas that don't fit well in existing formalisms. Newton, Euler, Dirac, Feynman and Witten are just a few of the most prominent people who broke out of existing frameworks, didn't think formally, and did work that led to a huge growth of mathematics. If you say "those people are physicists, not mathematicians", then you're slicing disciplines differently than me. I find their ideas more mathematically interesting than most mathematics that fits into existing frameworks.
@dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
@johncarlosbaez
John, I'm a huge fan of nonstandard analysis. i get that not everyone is, but what I found interesting about the history of NSA is that it started out informal, was ridiculed, then an alternative formalism invented which I find... annoying, and then Abraham Robinson came along and he wanted NSA to be rigorous so he found a way to make it so, and then since then others found simpler ways and in some ways
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject -
@johncarlosbaez
John, I'm a huge fan of nonstandard analysis. i get that not everyone is, but what I found interesting about the history of NSA is that it started out informal, was ridiculed, then an alternative formalism invented which I find... annoying, and then Abraham Robinson came along and he wanted NSA to be rigorous so he found a way to make it so, and then since then others found simpler ways and in some ways
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject@johncarlosbaez
the hyperreals are so "easy" to formalize its hard to imagine how long we went without a formalism.What's also interesting is how strong the pushback is about NSA. Multiple times a week on the internet calculus students will ask questions about dy/dx being a fraction or not... mention nonstandard analysis and youre likely to get down voted and attacked as unhelpful... happens on r/learnmath regularly.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
-
I don't agree that working with a proof assistant will reduce the chance that we'll come up with radical new ideas.
It's not at all difficult for me to picture someone like Grothendieck, who also broke out of many existing formalisms, writing his own library from scratch in order to express his ideas -- In many ways this is exactly what he did! Though of course he (and his collaborators) wrote a long series of books rather than writing a long list of agda/lean/etc files.
In fact, it's quite easy for me to picture someone like Grothendieck writing their own theorem prover! Perhaps in that world EGA/SGA would look much more like the currently-under-development synthetic algebraic geometry, formalized in a proof assistant that's custom made for arguments in the (big) zariski or etale topos.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
It is not clear who specifically you are replying to. I hope it is not me.
@johncarlosbaez @andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject
-
@johncarlosbaez
the hyperreals are so "easy" to formalize its hard to imagine how long we went without a formalism.What's also interesting is how strong the pushback is about NSA. Multiple times a week on the internet calculus students will ask questions about dy/dx being a fraction or not... mention nonstandard analysis and youre likely to get down voted and attacked as unhelpful... happens on r/learnmath regularly.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
@johncarlosbaez
So, while I think of formalism as a needed tool, I'm also with John in thinking that formalism is not always helpful. if formalism was enough we could replace all math books by the axioms of ZFC and be done with it... everything else left as an exercise for the reader
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
