I don't want to formalize any of my work on mathematics.
-
@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 -
It is not clear who specifically you are replying to. I hope it is not me.
@johncarlosbaez @andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject
Sorry, let me adopt your convention to make my reply more clear -- but you can tell I was replying to John since it's his post that show up above mine when you click my post (at least on my instance)
@johncarlosbaez @andrejbauer @dougmerritt @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 writes "But in fact I don't think formalizing mathematics at all makes us think the right way."
You should try it once to see by yourself. You are talking about something you've never done.
I say this because I also said the same thing as you said in the past.
And here is the first time I repent in public:
Computing an integer using a Grothendieck topos
https://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/@andrejbauer @dougmerritt @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
Having spent several years in the trenches of formalized mathematics by now, I'm actually more sympathetic @johncarlosbaez 's line of thinking than I used to be, but I think there's nothing about formalized mathematics *per se* that forces this to be the case.
The way I've come to use proof assistants/etc. over the years actually, counterintuitively, ends up making math more "empirical," in a way. My informal proofs and ideas become "hypotheses" I can "test" by attempting to find a formalism and suitable abstractions that make them checkable by a computer. And like any good scientific experiment, this quickly becomes an iterative process—take some informal ideas, attempt to formalize them, get some data back about what ends up being difficult, refine the ideas, repeat until a satisfactory equilibrium is found. And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself.
As already noted, however, this process carries the risk of railroading one's thoughts into those ways of thinking that are more easily formalized in a particular system. But imo this is a failure of that particular system to be sufficiently syntactically/semantically flexible, and not of formalism/interactive theorem proving in general.
The future I hope for, and which I am actively building toward, is one in which we have general systems for defining, simulating, and verifiably translating between different logical/formal systems, so that if someone has a new mathematical idea they want to try out it's easy to get up and running with a system for testing it and relating it to other frameworks.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
-
@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
@MartinEscardo Re: trusting C code, I heard horror stories about compilers for aeronautics, where one of the criteria for acceptance is that the "compiler" is very transparent and that the assembly code is auditable on its own. Apparently, getting these sort of people to accept an optimising compiler, even CompCert, was a hard battle… (But it was won!)
-
@yakmacker - That would be cool. I will let someone else work on this, while I spend my limited remaining years thinking about the mysteries of math and physics that intrigue me.
-
@johncarlosbaez writes "But in fact I don't think formalizing mathematics at all makes us think the right way."
You should try it once to see by yourself. You are talking about something you've never done.
I say this because I also said the same thing as you said in the past.
And here is the first time I repent in public:
Computing an integer using a Grothendieck topos
https://math.andrej.com/2021/05/18/computing-an-integer-using-a-sheaf-topos/@andrejbauer @dougmerritt @JacquesC2 @pigworker @xenaproject
@MartinEscardo - how long would it take to "try it once"? Then I can weigh that against other things I could do with that time.
I have absolutely nothing I want to formalize, and I'd be weighing time spent on this against things like learning how to make music on a digital audio workstation, which I put off because it doesn't provide the instant gratification of playing a piano, but which I know I'd like in the end. In either case I know I'll start by suffering for hours, learning someone else's syntax and conventions instead of thinking my own thoughts. But for music software I know I'll eventually get a product I enjoy that I couldn't make any other eay.
-
Having spent several years in the trenches of formalized mathematics by now, I'm actually more sympathetic @johncarlosbaez 's line of thinking than I used to be, but I think there's nothing about formalized mathematics *per se* that forces this to be the case.
The way I've come to use proof assistants/etc. over the years actually, counterintuitively, ends up making math more "empirical," in a way. My informal proofs and ideas become "hypotheses" I can "test" by attempting to find a formalism and suitable abstractions that make them checkable by a computer. And like any good scientific experiment, this quickly becomes an iterative process—take some informal ideas, attempt to formalize them, get some data back about what ends up being difficult, refine the ideas, repeat until a satisfactory equilibrium is found. And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself.
As already noted, however, this process carries the risk of railroading one's thoughts into those ways of thinking that are more easily formalized in a particular system. But imo this is a failure of that particular system to be sufficiently syntactically/semantically flexible, and not of formalism/interactive theorem proving in general.
The future I hope for, and which I am actively building toward, is one in which we have general systems for defining, simulating, and verifiably translating between different logical/formal systems, so that if someone has a new mathematical idea they want to try out it's easy to get up and running with a system for testing it and relating it to other frameworks.
@andrejbauer @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject
@cbaberle said "And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself."
I have found the same thing. When I am working on things that are not directly about formalized mathematics, but with using a proof assistant as a blackboard (echoing Martin's wonderful phrasing), I feel that I am much freer to make wild conjectures, because I can disprove them equally quickly.
The numbers of "models" of quantum programming based on traced monoidal categories (that did not in fact work) is staggering. The failures were usually quite subtle. My co-author(s) and I had convinced ourselves via 'paper math' that they worked, for each and every one of them.
@johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject
-
@cbaberle said "And this process itself can lead to a lot of "a ha" moments and "radical" new ideas, itself."
I have found the same thing. When I am working on things that are not directly about formalized mathematics, but with using a proof assistant as a blackboard (echoing Martin's wonderful phrasing), I feel that I am much freer to make wild conjectures, because I can disprove them equally quickly.
The numbers of "models" of quantum programming based on traced monoidal categories (that did not in fact work) is staggering. The failures were usually quite subtle. My co-author(s) and I had convinced ourselves via 'paper math' that they worked, for each and every one of them.
@johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject
@JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject I feel like there is a bit of a selection bias here. Would you say that formalization is as useful as a blackboard for eg number theory or geometric measure theory, as it is for type-theory/logic/computer science?
There is a huge UX problem, due to the fact that most mathematical research is done with objects and methods that fit badly in the current text-based, heavily formal (I don't know how to say this better) proof assistants. So my impression is that for most mathematics working formalization-first would be as painful and counterproductive as it would be for a PL/type theorist to work only on a whiteboard.
Hopefully this will change in the future! I do believe that formalization is very useful for mathematics. -
@JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject I feel like there is a bit of a selection bias here. Would you say that formalization is as useful as a blackboard for eg number theory or geometric measure theory, as it is for type-theory/logic/computer science?
There is a huge UX problem, due to the fact that most mathematical research is done with objects and methods that fit badly in the current text-based, heavily formal (I don't know how to say this better) proof assistants. So my impression is that for most mathematics working formalization-first would be as painful and counterproductive as it would be for a PL/type theorist to work only on a whiteboard.
Hopefully this will change in the future! I do believe that formalization is very useful for mathematics.@mc These areas might be more painful, but they contain mistakes. I found a few measure theoretic mistakes in some recent papers / theses over the last year or two.
@JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @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 @dougmerritt @MartinEscardo @JacquesC2 @pigworker @xenaproject Well, it should be obvious, but let me say it anyway.
We need mathematicians of every kind: the thinkers, the dreamers, the formalizers, and even physicists.
-
@JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject I feel like there is a bit of a selection bias here. Would you say that formalization is as useful as a blackboard for eg number theory or geometric measure theory, as it is for type-theory/logic/computer science?
There is a huge UX problem, due to the fact that most mathematical research is done with objects and methods that fit badly in the current text-based, heavily formal (I don't know how to say this better) proof assistants. So my impression is that for most mathematics working formalization-first would be as painful and counterproductive as it would be for a PL/type theorist to work only on a whiteboard.
Hopefully this will change in the future! I do believe that formalization is very useful for mathematics.@mc @JacquesC2 @cbaberle @johncarlosbaez @dougmerritt @MartinEscardo @pigworker @xenaproject I'd go further and "blame" the philosophers of language, too.
-
@MartinEscardo - how long would it take to "try it once"? Then I can weigh that against other things I could do with that time.
I have absolutely nothing I want to formalize, and I'd be weighing time spent on this against things like learning how to make music on a digital audio workstation, which I put off because it doesn't provide the instant gratification of playing a piano, but which I know I'd like in the end. In either case I know I'll start by suffering for hours, learning someone else's syntax and conventions instead of thinking my own thoughts. But for music software I know I'll eventually get a product I enjoy that I couldn't make any other eay.
@johncarlosbaez @MartinEscardo It took me weeks to finish my first non-trivial proof (preservation in an STLC). I'd think there's stuff that can be knocked out in a few hours that still retain the flavor, but no example leaps to mind.
-
@JacquesC2 @cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject I feel like there is a bit of a selection bias here. Would you say that formalization is as useful as a blackboard for eg number theory or geometric measure theory, as it is for type-theory/logic/computer science?
There is a huge UX problem, due to the fact that most mathematical research is done with objects and methods that fit badly in the current text-based, heavily formal (I don't know how to say this better) proof assistants. So my impression is that for most mathematics working formalization-first would be as painful and counterproductive as it would be for a PL/type theorist to work only on a whiteboard.
Hopefully this will change in the future! I do believe that formalization is very useful for mathematics.This issue of fit (which is indeed related to linguistics) is why CASes have a huge leg up on ITPs regarding UX. But they also have their fit problems, never mind their correctness problems.
Mathematica's UI coupled with a nice ITP would be nice. That would need a complete rewrite of both halves to be viable. But that would be a vast improvement.
Then we'd be in a good position, as a community, to actually figure out the "next generation" system.
@cbaberle @johncarlosbaez @andrejbauer @dougmerritt @MartinEscardo @pigworker @xenaproject
