> This infuriating situation notwithstanding, I would not advise anyone to formalize the Mœglin-Waldspurger books so that Lean can decide which pages remain valid when number fields are replaced by function fields and which require new ideas. And you can be sure I’m not going to do that myself.
I don't get it Michael -- why would you not advise anyone to formalise a technical piece of mathematics? One of the *powers* of a formal system is that it will tell you exactly which lemmas don't work as stated in the function field case. After that Tao et al formalisation of the polynomial Freiman-Ruzsa conjecture had finished, someone improved a constant from 12 to 11 and formalising the revised version in Lean was far easier than doing it on paper, where you are forever worrying that a minor tweak to definition 7 now makes a stronger variant of lemma 9 true, but might also break lemma 11.
Now, Kevin, I have a question for you. I'm not at all convinced that there are enough enthusiasts to carry out the project of formalizing the entire theory of automorphic forms, or even the substantial portion that goes into the stabilization of the twisted trace formula. Treating the theory of Eisenstein series, as in the previous Mœglin-Waldspurger book, as a black box, along with the unstabilized twisted trace formula to be expected from work in progress of Lemaire, could make the process much more manageable. Actually, I wonder whether the missing steps might require going all the way back to the axioms, but suppose what I just suggested is possible, and one could formalize the Mœglin-Waldspurger books relative to this earlier work. Would you find that an acceptable use of Lean, or would it be ideologically tainted to use it in such a hybrid fashion?
I am formalising a proof of FLT but I'm going to assume Mazur's torsion theorem, cyclic base change and Jacquet-Langlands (for now) (and some other things), so I definitely don't think it would be tainted to use Lean in this way! My first goal is [theorems proved by the end of the 1980s] => FLT.
I should make my question more precise. Could you imagine this being your only goal? Or the end of a process, for purely opportunistic reasons, rather than the first step?
I think people formalise for different reasons. My personal motivation for formalising a result of the form "these hard theorems imply this hard theorem" is that it will force me to put a lot of the definitions of the key players in the theory of automorphic forms (e.g. an automorphic form...) into Lean. Definitions are tricky in a formal system -- e.g. is a group a pair (G,*) or a quadruple (G,*,1,^{-1}), and are there three axioms or five? (e.g. 1*x=x follows from x*1=x, associativity, and one of the inverse axioms (but not the other one)). Right now language models are becoming better at translating statements of theorems from natural to formal language, and maybe one day they'll get good at proofs, but their life will be made much easier if I can already offer them the definitions. So that's one reason to use the systems in this way. I would say I have multiple goals which motivate me to do work like this; one is possible AI applications, one is to show that the systems are now good enough to eat a 150 page paper relying on algebra, analysis, topology, geometry and number theory (rather than 300 page paper about finite groups basically relying only on the theory of finite groups, which we know has been possible for over a decade), one is to increase the number of definitions in Lean's maths library, one is to increase the amount of foundational Bourbaki-like material in Lean's maths library (e.g. I have students developing the theory of central simple algebras because I want quaternion algebras, and they're showing the link to cohomological Brauer groups because I want to check that our theory of group cohomology works in practice before I start working hard on class field theory). I'm very much of the mindset now that formalisation of mathematics is just a hugely good idea in general, perhaps for reasons we didn't think of yet. Weil and Serre and the other Bourbakistes were have been doing this for decades, I also think it's just a good idea to write things down -- anything we're interested in -- carefully and correctly.
Thank you for giving me a chance to expand on that comment. As I approach the end of each essay Substack warns me that my text is "too long for email," so my paragraphs become more cryptic.
All I meant in this case was that it would be a bad career move. Hiring committees tend to be dismissive of this kind of work, and so do journal editors. Of course this could change, and I wouldn't mind at all if you wanted to join me in a dialogue about this: why it's the case, whether or not it could change, and what would be the implications if it did.
Somehow I discovered that Ernie Davis wrote a comment about my last paragraph on his Facebook page: "In particular, though it is the reverse of his intent, the description at the end of the difficulties involved in transferring deep results from the theory of number fields to the theory of function fields, and how all this affects a theorem that he is working on, is, from a different point of view, one of the best arguments I've seen for why formalization of mathematics is a worthwhile undertaking." I wrote to him to explain that it was not at all the reverse of my intent; on the contrary:
"My intentions when writing about this material are always ambiguous and contradictory; I would even say an installment is a failure if it ends unambiguously. [Here I mentioned several exceptions.]… I would be delighted if someone were to formalize the Moeglin-Waldspurger book so that the arguments that break down for function fields were to become visible — turned red, for example — and then if a journal were to publish, and thus to certify, the corrected revisions of the red material. I see this as just an elaborate form of bookkeeping, but that's because I've spent enough time going through the stabilization of the trace formula (in a seminar in Paris with Labesse, Moeglin, and Waldspurger, among others, years before the books came out) to feel I know what the issues are."
But I then added:
"Someone who is encountering this for the first time will have to go through the arguments in some detail, on the other hand, and the ritualistic aspect of publishing requires that the editor provide such a reader with a coherent narrative. So just the revised red pages, together with instructions to read the surrounding pages in Moeglin-Waldspurger, can't be published. This is one more example of the irrationality of mathematics, but it's one I believe should be preserved. I'm realizing that my book can be read as a defense of the most irrational aspects of mathematics, and I don't mind that at all."
So for the foreseeable future spending several months or years to learn the Mœglin-Waldspurger books and then to formalize them would be incompatible with the existing reward system, and the result would not be publishable. But if some group of colleagues felt motivated to sacrifice their careers so that some of us could have a reference for our current projects that is plausible enough to get past the referees, I certainly wouldn't object.
Yes, I agree that it would be a bad career move and is incompatible with the existing reward system. I think that formalising important mathematics is important, but I agree that mathematical society does not yet place much of a value on it in general. Of course one approach is just to say "well wait for a few people to formalise the correct *definitions* (this is a much easier problem) and then wait until AI becomes good at translating textbooks into a formal language" (which is surely much easier than actually getting a machine to come up with a new theorem).
"Sam Altman said it cost $100 million to train GPT-4!! What angel investor is going to cough up that kind of money for the privilege of ‘exploring the space of what is true and what is false and why things are true,’ (which is how Tao explains what mathematicians do)?!?"
$100 million exceeds the amount currently expended by the Federal Government on "Mathematics" and can thereby be promoted by "Trump 47 Administration" as a "cost-cutting measure".
I long to understand the Langlands program more. It seems like a kind of Fourier Transform extended to much (all?) of math. One day I hope you will write about it for the rest of us.
> This infuriating situation notwithstanding, I would not advise anyone to formalize the Mœglin-Waldspurger books so that Lean can decide which pages remain valid when number fields are replaced by function fields and which require new ideas. And you can be sure I’m not going to do that myself.
I don't get it Michael -- why would you not advise anyone to formalise a technical piece of mathematics? One of the *powers* of a formal system is that it will tell you exactly which lemmas don't work as stated in the function field case. After that Tao et al formalisation of the polynomial Freiman-Ruzsa conjecture had finished, someone improved a constant from 12 to 11 and formalising the revised version in Lean was far easier than doing it on paper, where you are forever worrying that a minor tweak to definition 7 now makes a stronger variant of lemma 9 true, but might also break lemma 11.
Now, Kevin, I have a question for you. I'm not at all convinced that there are enough enthusiasts to carry out the project of formalizing the entire theory of automorphic forms, or even the substantial portion that goes into the stabilization of the twisted trace formula. Treating the theory of Eisenstein series, as in the previous Mœglin-Waldspurger book, as a black box, along with the unstabilized twisted trace formula to be expected from work in progress of Lemaire, could make the process much more manageable. Actually, I wonder whether the missing steps might require going all the way back to the axioms, but suppose what I just suggested is possible, and one could formalize the Mœglin-Waldspurger books relative to this earlier work. Would you find that an acceptable use of Lean, or would it be ideologically tainted to use it in such a hybrid fashion?
I am formalising a proof of FLT but I'm going to assume Mazur's torsion theorem, cyclic base change and Jacquet-Langlands (for now) (and some other things), so I definitely don't think it would be tainted to use Lean in this way! My first goal is [theorems proved by the end of the 1980s] => FLT.
I should make my question more precise. Could you imagine this being your only goal? Or the end of a process, for purely opportunistic reasons, rather than the first step?
I think people formalise for different reasons. My personal motivation for formalising a result of the form "these hard theorems imply this hard theorem" is that it will force me to put a lot of the definitions of the key players in the theory of automorphic forms (e.g. an automorphic form...) into Lean. Definitions are tricky in a formal system -- e.g. is a group a pair (G,*) or a quadruple (G,*,1,^{-1}), and are there three axioms or five? (e.g. 1*x=x follows from x*1=x, associativity, and one of the inverse axioms (but not the other one)). Right now language models are becoming better at translating statements of theorems from natural to formal language, and maybe one day they'll get good at proofs, but their life will be made much easier if I can already offer them the definitions. So that's one reason to use the systems in this way. I would say I have multiple goals which motivate me to do work like this; one is possible AI applications, one is to show that the systems are now good enough to eat a 150 page paper relying on algebra, analysis, topology, geometry and number theory (rather than 300 page paper about finite groups basically relying only on the theory of finite groups, which we know has been possible for over a decade), one is to increase the number of definitions in Lean's maths library, one is to increase the amount of foundational Bourbaki-like material in Lean's maths library (e.g. I have students developing the theory of central simple algebras because I want quaternion algebras, and they're showing the link to cohomological Brauer groups because I want to check that our theory of group cohomology works in practice before I start working hard on class field theory). I'm very much of the mindset now that formalisation of mathematics is just a hugely good idea in general, perhaps for reasons we didn't think of yet. Weil and Serre and the other Bourbakistes were have been doing this for decades, I also think it's just a good idea to write things down -- anything we're interested in -- carefully and correctly.
Thank you for giving me a chance to expand on that comment. As I approach the end of each essay Substack warns me that my text is "too long for email," so my paragraphs become more cryptic.
All I meant in this case was that it would be a bad career move. Hiring committees tend to be dismissive of this kind of work, and so do journal editors. Of course this could change, and I wouldn't mind at all if you wanted to join me in a dialogue about this: why it's the case, whether or not it could change, and what would be the implications if it did.
Somehow I discovered that Ernie Davis wrote a comment about my last paragraph on his Facebook page: "In particular, though it is the reverse of his intent, the description at the end of the difficulties involved in transferring deep results from the theory of number fields to the theory of function fields, and how all this affects a theorem that he is working on, is, from a different point of view, one of the best arguments I've seen for why formalization of mathematics is a worthwhile undertaking." I wrote to him to explain that it was not at all the reverse of my intent; on the contrary:
"My intentions when writing about this material are always ambiguous and contradictory; I would even say an installment is a failure if it ends unambiguously. [Here I mentioned several exceptions.]… I would be delighted if someone were to formalize the Moeglin-Waldspurger book so that the arguments that break down for function fields were to become visible — turned red, for example — and then if a journal were to publish, and thus to certify, the corrected revisions of the red material. I see this as just an elaborate form of bookkeeping, but that's because I've spent enough time going through the stabilization of the trace formula (in a seminar in Paris with Labesse, Moeglin, and Waldspurger, among others, years before the books came out) to feel I know what the issues are."
But I then added:
"Someone who is encountering this for the first time will have to go through the arguments in some detail, on the other hand, and the ritualistic aspect of publishing requires that the editor provide such a reader with a coherent narrative. So just the revised red pages, together with instructions to read the surrounding pages in Moeglin-Waldspurger, can't be published. This is one more example of the irrationality of mathematics, but it's one I believe should be preserved. I'm realizing that my book can be read as a defense of the most irrational aspects of mathematics, and I don't mind that at all."
So for the foreseeable future spending several months or years to learn the Mœglin-Waldspurger books and then to formalize them would be incompatible with the existing reward system, and the result would not be publishable. But if some group of colleagues felt motivated to sacrifice their careers so that some of us could have a reference for our current projects that is plausible enough to get past the referees, I certainly wouldn't object.
Yes, I agree that it would be a bad career move and is incompatible with the existing reward system. I think that formalising important mathematics is important, but I agree that mathematical society does not yet place much of a value on it in general. Of course one approach is just to say "well wait for a few people to formalise the correct *definitions* (this is a much easier problem) and then wait until AI becomes good at translating textbooks into a formal language" (which is surely much easier than actually getting a machine to come up with a new theorem).
Needless to say, this apllies to "Harris 47 Administration" as well.
I meant "barely exceeds"
"Sam Altman said it cost $100 million to train GPT-4!! What angel investor is going to cough up that kind of money for the privilege of ‘exploring the space of what is true and what is false and why things are true,’ (which is how Tao explains what mathematicians do)?!?"
$100 million exceeds the amount currently expended by the Federal Government on "Mathematics" and can thereby be promoted by "Trump 47 Administration" as a "cost-cutting measure".
I long to understand the Langlands program more. It seems like a kind of Fourier Transform extended to much (all?) of math. One day I hope you will write about it for the rest of us.