12 ms·

'A-team' of math proves a critical link between addition and sets

274 points by digital55 3y ago

blowski 3y ago
The maths goes over my head, but this paragraph was very interesting: > Tao then kicked off an effort to formalize the proof in Lean, a programming language that helps mathematicians verify theorems. In just a few weeks, that effort succeeded. Early Tuesday morning of December 5, Tao announced that Lean had proved the conjecture without any “sorrys” — the standard statement that appears when the computer can’t verify a certain step. This is the highest-profile use of such verification tools since 2021, and marks an inflection point in the ways mathematicians write proofs in terms a computer can understand. If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, said Gowers.
- robertlagrant 3y ago
  > If these tools become easy enough for mathematicians to use Sick burn, Gowers.
  - gowld 3y ago
    It's honest constructive criticism. Lean is very hard to use. It's even hard to install and run.
    - dumbo-octopus 3y ago
      Elan makes it actually quite easy. It's among the better package managers out there, comparable to cargo. There's a single bash script to install both the runtime and the package manager on a variety of platforms, and the integrated build system and native module bundler is both powerful and isomorphic, so all you need to learn is Lean. Without any prior knowledge of Lean I was able to patch existing build scripts to support platform specific C extensions in less than half an hour.
  - wbhart 3y ago
    I doubt that he was intending a burn here. He's not talking about user interface issues or the like. He's most probably, I would assume, talking about the well-known issue that formalisation tools require knowledge that a standard mathematician doesn't possess, such as the names of all the Lean tactics, how to locate the right theorem to use in mathlib (the Lean library), the necessity to write mathematics in a very formal language which is based on dependent type theory rather than based on sets (which is what most mathematicians are used to), etc. Moreover, formalised mathematics does not work with natural language (and perhaps can't), and it will not accept informal or intuitive arguments. There are a lot of very fiddly things that have to be attended to. One can't assume that the reader is a skilled mathematicians who can easily fill in trivial details, as when writing a maths paper for expert readers. But the Lean people are acutely aware of all of this. In my opinion he's not so much offering them much needed criticism so much as acknowledging one of the known barriers to mathematicians from outside the formalisation community getting into formalisation. This is a major point of the article, that real, serious mathematicians have broken through that barrier recently, and it's not the first time. So things have improved enough to show that it is possible for seriously committed mathematicians to do this, even famous ones!
- kmill 3y ago
  I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support). It's exciting to see how quickly the work was done, but it's worth keeping in mind that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users. There aren't enough experienced Lean users to go around yet for any old project, so Gowers's point about ease of use is an important one. Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It's reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.
  - cs702 3y ago
    > I helped a very little... Thank You for helping with the effort, even if it was only "a very little." I love coming across comments like yours on HN.
  - ska 3y ago
    >Something that was necessary for the success of this was years of development that had already been For projects like this it is often very thankless work in the beginning, and can be a real grind. You need at least one person with a vision of how cool it will be in the (poorly defined) future, and a lot of determination.
    - pastage 3y ago
      It is great for personal growth. Since I have been part of many such grinds that are now big data sets, I can honestly tell you that it is one of the best things in the world. I know that those thousands of hours of my work has led to 100x savings for other people. I also met people and could work on problems I would never get in professional life.
  - zozbot234 3y ago
    > Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib Yes but the bulk of the work on this project was background as well. So the ease of use problem should be solving itself over time as more and more prereqs get filled in. BTW, I find it interesting that mathlib is apparently also getting refactored to accommodate constructive proofs better, as part of the porting effort to Lean 4. This might encourage more CS- and program-verification minded folks to join the effort, and maybe some folks in math-foundations too (though Lean suffers there by not being able to work with the homotopy-types axioms).
- brap 3y ago
  Why did the verification step take so long? I imagine just verifying proofs is very efficient, no? Or do they mean formalizing the proof in Lean is what took weeks?
  - adastra22 3y ago
    They’re talking about formalizing the proof (aka writing Lean “code”).
- spadufed 3y ago
  If anybody's interested in learning more about Lean, he's been posting his experiences with the project over at @tao@mathstodon.xyz
- Affric 3y ago
  On your opening sentence against this one from the article: > feels like really one of the most basic things that we didn’t understand Nothing can prepare us for the depth of mathematics.
- westurner 3y ago
  > If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, List of long mathematical proofs: https://en.wikipedia.org/wiki/List_of_long_mathematical_proofs https://en.wikipedia.org/wiki/List_of_long_mathematical_proo... : > This is a list of unusually long mathematical proofs. Such proofs often use computational proof methods and may be considered non-surveyable. > As of 2011, the longest mathematical proof, measured by number of published journal pages, is the classification of finite simple groups with well over 10000 pages. There are several proofs that would be far longer than this if the details of the computer calculations they depend on were published in full. Non-surveyable proof: https://en.wikipedia.org/wiki/Non-surveyable_proof https://en.wikipedia.org/wiki/Non-surveyable_proof : > In the philosophy of mathematics, a non-surveyable proof is a mathematical proof that is considered infeasible for a human mathematician to verify and so of controversial validity.
  - 7thaccount 3y ago
    I wonder how much of mathematics is locked away from us as it requires a level of intelligence we may never have. Why do we assume proofs should be simple little equations or even just a few pages? Elegance? Why should the universe be so elegant? Is it because elegant structures are more efficient and use less energy? Edit: I know some proofs like Fermat's last theorem were like dozens of pages or more, but I realize that is still within the comprehension of a well trained and gifted human being.
    - westurner 3y ago
      Take for example the Standard Model Lagrangian (which is a sum of nonlinear fields and used to predict some but not all of particle physics (i.e. n-body gravity, superfluids, antimatter or not, Copenhagen interpretation or not, etc.)), [ LaTeX rendering of the Standard Model Lagrangian, and other as-yet unintegrated equations ] How elegant are these? Is it ever proven that they are of minimal complexity in their respective domains piece-wisely? Learning of Entropy, I had hoped you know. But then that's just classical Shannon entropy, and not quite the types of quantum entropy described in for example the Quantum discord Wikipedia article, and then that's still not quite quantum fluidic complexity (with other field effects discounted, of course); so is there an elegant quantum fluidic thermodynamic basis for it all and emergence? Quasiparticles display emergent behavior. Virtual particles have or haven't mass independent of 2-body gravity. Gravity alone sometimes produces mass, or photons at least. Regardless, things have curl and Divergence. And so Quantum Chaos: what can it predict? Can it can do quantum gravity effects in Superfluids at scale? Progress in quantum CFD would require a different architecture to prove low error of a model for predictions in superfluids. And so how many error-corrected qubits exist to simulate a gas fluid in space (in microgravity) is the limiting factor in checking the sufficiency of a grander unified model from here, too. And also for how long qubits can be stored; we can save save a integer and a float for longer than human timescale with error corrected distributed storage networks, but we can't store the output wave function(s*) from quantum computer simulations for more than a second. So prove it means QC, and that's not what I see here.
- az226 3y ago
  You can probably fine tune GPT4 to help mathematicians use this new tool as well.
owlbite 3y ago
10 years ago a crack professor unit was defunded by an academic tribunal for misconduct they didn't commit. These men promptly escaped from a maximum teaching schedule to the research underground. Today, still wanted by the activist community, they survive as proovers of fortune. If you have a problem that no one else can solve, and if you can find them, maybe you can hire The A-Team.
- Agingcoder 3y ago
  That’s funny thanks :-)
- 082349872349872 3y ago
  My favourite bit of every episode was the iconic ὅπλισις when Prof. Dr. P.H.D. Baracus first adds structure preserving maps to every object in sight then uses the snake lemma to weld them together with connecting homomorphisms. "I pity the fool who doesn't chase diagrams"
  - CobrastanJorji 3y ago
    I got a little sick of the recurring joke where Prof. Dr. Baracus would complain about flat, two-dimensional, infinite surfaces, and then the team would trick him into using one anyway.
    - jfengel 3y ago
      Goddamn that's a long way to go to make that joke. Worth the journey, but those are brain cells I haven't used in decades. I really wish I could garbage-collect some of the 1980s pop culture neurons and put them to better use.
      - shrimp_emoji 3y ago
        I feel like this about Call of Duty maps.
      - sumtechguy 3y ago
kleiba 3y ago
What do you think, how long until we can give conjectures to a specially trained LLM to come up with a proof?
- brap 3y ago
  My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.
  - prmph 3y ago
    I think you are much too optimistic. Proof verification, though still hard to automate, seems at least tractable. I'm not a mathematician by any means, but something tells me automated proof search, in the general case, would require solving the halting problem, which means it is impossible even in principle.
    - dumbo-octopus 3y ago
      In the general case, proof search is obviously impossible, for the reason you state. But the case need not be general. A proof search machine that takes in a theorem and outputs `"proof: ..." | "antiProof: ..." | "idk"` would be quite powerful indeed.
      - gpm 3y ago
        def decider(_): print("idk") Done ;) --- More seriously, the benchmark would be something along the lines of "and it is better at finding proofs than humans are", like how chess engines haven't solved chess, but they are so much better than humans that they always win in a competition between the two. There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically.
        brap 3y ago
        >There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically That’s really all I was trying to say, not sure why I’m getting downvoted
logtempo 3y ago
Yesterday I was wondering if it's possible to have an AI that can "recreate" the mathematics as we know it, and even go further and explore unexplored paths. Though prduced by a video explaining how AI helped to find optimization in the computation of matrix multiplication.
- jmj 3y ago
  I am working on that for my PhD!
  - logtempo 3y ago
    Ho, that's really cool! Sounds a bit like digging your own grave as mathematician but it must be very challenging
- 082349872349872 3y ago
  Unfortunately it's too late to give Theory Mine theorems named after your loved ones as gifts this year: https://www.theorymine.com/home https://www.theorymine.com/home
wslh 3y ago
BTW "Katalin Marton’s Lasting Legacy" [1] [1] https://ee.stanford.edu/~gray/Kati_Marton.pdf https://ee.stanford.edu/~gray/Kati_Marton.pdf
swayvil 3y ago
You always hear "the map is not the territory". Which is to say, names are applied, models are asserted and all our fine ideas about the world are our own contrivance, not the world's. But how close could we get?
- oldandtired 3y ago
  Not very close at all. Every map that is made leaves out an enormous amount of the territory because that detail is irrelevant to the map being used or created. The more detailed the map is, the more one should recognise just how much more detail is being ignored. If you want to get close, just go to the territory itself and be there directly. All too often, we use mathematics as a map for the actual world around and to keep that map manageable, we have to ignore much of the actual world.
  - swayvil 3y ago
    The trick would be to find a real phenomenon that expresses itself symbolically. Like discovering an animal born with a nametag. I think you'd have to look in the realm of thought for that. Surely it isn't just empty space where we build our memories and models. Surely it has its own landscape.
oldandtired 3y ago
Now that it has been done in Lean, how about the version that can be put into Metamath?

274 points by digital55 3y ago

The maths goes over my head, but this paragraph was very interesting: > Tao then kicked off an effort to formalize the proof in Lean, a programming language that helps mathematicians verify theorems. In just a few weeks, that effort succeeded. Early Tuesday morning of December 5, Tao announced that Lean had proved the conjecture without any “sorrys” — the standard statement that appears when the computer can’t verify a certain step. This is the highest-profile use of such verification tools since 2021, and marks an inflection point in the ways mathematicians write proofs in terms a computer can understand. If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, said Gowers.

robertlagrant 3y ago
> If these tools become easy enough for mathematicians to use Sick burn, Gowers.
- gowld 3y ago
  It's honest constructive criticism. Lean is very hard to use. It's even hard to install and run.
  - dumbo-octopus 3y ago
    Elan makes it actually quite easy. It's among the better package managers out there, comparable to cargo. There's a single bash script to install both the runtime and the package manager on a variety of platforms, and the integrated build system and native module bundler is both powerful and isomorphic, so all you need to learn is Lean. Without any prior knowledge of Lean I was able to patch existing build scripts to support platform specific C extensions in less than half an hour.
- wbhart 3y ago
  I doubt that he was intending a burn here. He's not talking about user interface issues or the like. He's most probably, I would assume, talking about the well-known issue that formalisation tools require knowledge that a standard mathematician doesn't possess, such as the names of all the Lean tactics, how to locate the right theorem to use in mathlib (the Lean library), the necessity to write mathematics in a very formal language which is based on dependent type theory rather than based on sets (which is what most mathematicians are used to), etc. Moreover, formalised mathematics does not work with natural language (and perhaps can't), and it will not accept informal or intuitive arguments. There are a lot of very fiddly things that have to be attended to. One can't assume that the reader is a skilled mathematicians who can easily fill in trivial details, as when writing a maths paper for expert readers. But the Lean people are acutely aware of all of this. In my opinion he's not so much offering them much needed criticism so much as acknowledging one of the known barriers to mathematicians from outside the formalisation community getting into formalisation. This is a major point of the article, that real, serious mathematicians have broken through that barrier recently, and it's not the first time. So things have improved enough to show that it is possible for seriously committed mathematicians to do this, even famous ones!
kmill 3y ago
I helped a very little with the formalization (I filled in some trivial algebraic manipulations, and I was there for some Lean technical support). It's exciting to see how quickly the work was done, but it's worth keeping in mind that a top mathematician leading a formalization effort is very exciting, so he could very easily scramble a team of around 20 experienced Lean users. There aren't enough experienced Lean users to go around yet for any old project, so Gowers's point about ease of use is an important one. Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib. It's reassuring that mathlib is being developed in such a way that new mathematics can be formalized using it. Like usual though, there was plenty missing. I think this drove a few thousand more lines of general probability theory development.
- cs702 3y ago
  > I helped a very little... Thank You for helping with the effort, even if it was only "a very little." I love coming across comments like yours on HN.
- ska 3y ago
  >Something that was necessary for the success of this was years of development that had already been For projects like this it is often very thankless work in the beginning, and can be a real grind. You need at least one person with a vision of how cool it will be in the (poorly defined) future, and a lot of determination.
  - pastage 3y ago
    It is great for personal growth. Since I have been part of many such grinds that are now big data sets, I can honestly tell you that it is one of the best things in the world. I know that those thousands of hours of my work has led to 100x savings for other people. I also met people and could work on problems I would never get in professional life.
- zozbot234 3y ago
  > Something that was necessary for the success of this was years of development that had already been done for both Lean and mathlib Yes but the bulk of the work on this project was background as well. So the ease of use problem should be solving itself over time as more and more prereqs get filled in. BTW, I find it interesting that mathlib is apparently also getting refactored to accommodate constructive proofs better, as part of the porting effort to Lean 4. This might encourage more CS- and program-verification minded folks to join the effort, and maybe some folks in math-foundations too (though Lean suffers there by not being able to work with the homotopy-types axioms).
brap 3y ago
Why did the verification step take so long? I imagine just verifying proofs is very efficient, no? Or do they mean formalizing the proof in Lean is what took weeks?
- adastra22 3y ago
  They’re talking about formalizing the proof (aka writing Lean “code”).
spadufed 3y ago
If anybody's interested in learning more about Lean, he's been posting his experiences with the project over at @tao@mathstodon.xyz
Affric 3y ago
On your opening sentence against this one from the article: > feels like really one of the most basic things that we didn’t understand Nothing can prepare us for the depth of mathematics.
westurner 3y ago
> If these tools become easy enough for mathematicians to use, they might be able to substitute for the often prolonged and onerous peer review process, List of long mathematical proofs: https://en.wikipedia.org/wiki/List_of_long_mathematical_proofs https://en.wikipedia.org/wiki/List_of_long_mathematical_proo... : > This is a list of unusually long mathematical proofs. Such proofs often use computational proof methods and may be considered non-surveyable. > As of 2011, the longest mathematical proof, measured by number of published journal pages, is the classification of finite simple groups with well over 10000 pages. There are several proofs that would be far longer than this if the details of the computer calculations they depend on were published in full. Non-surveyable proof: https://en.wikipedia.org/wiki/Non-surveyable_proof https://en.wikipedia.org/wiki/Non-surveyable_proof : > In the philosophy of mathematics, a non-surveyable proof is a mathematical proof that is considered infeasible for a human mathematician to verify and so of controversial validity.
- 7thaccount 3y ago
  I wonder how much of mathematics is locked away from us as it requires a level of intelligence we may never have. Why do we assume proofs should be simple little equations or even just a few pages? Elegance? Why should the universe be so elegant? Is it because elegant structures are more efficient and use less energy? Edit: I know some proofs like Fermat's last theorem were like dozens of pages or more, but I realize that is still within the comprehension of a well trained and gifted human being.
  - westurner 3y ago
    Take for example the Standard Model Lagrangian (which is a sum of nonlinear fields and used to predict some but not all of particle physics (i.e. n-body gravity, superfluids, antimatter or not, Copenhagen interpretation or not, etc.)), [ LaTeX rendering of the Standard Model Lagrangian, and other as-yet unintegrated equations ] How elegant are these? Is it ever proven that they are of minimal complexity in their respective domains piece-wisely? Learning of Entropy, I had hoped you know. But then that's just classical Shannon entropy, and not quite the types of quantum entropy described in for example the Quantum discord Wikipedia article, and then that's still not quite quantum fluidic complexity (with other field effects discounted, of course); so is there an elegant quantum fluidic thermodynamic basis for it all and emergence? Quasiparticles display emergent behavior. Virtual particles have or haven't mass independent of 2-body gravity. Gravity alone sometimes produces mass, or photons at least. Regardless, things have curl and Divergence. And so Quantum Chaos: what can it predict? Can it can do quantum gravity effects in Superfluids at scale? Progress in quantum CFD would require a different architecture to prove low error of a model for predictions in superfluids. And so how many error-corrected qubits exist to simulate a gas fluid in space (in microgravity) is the limiting factor in checking the sufficiency of a grander unified model from here, too. And also for how long qubits can be stored; we can save save a integer and a float for longer than human timescale with error corrected distributed storage networks, but we can't store the output wave function(s*) from quantum computer simulations for more than a second. So prove it means QC, and that's not what I see here.
az226 3y ago
You can probably fine tune GPT4 to help mathematicians use this new tool as well.

owlbite 3y ago

10 years ago a crack professor unit was defunded by an academic tribunal for misconduct they didn't commit. These men promptly escaped from a maximum teaching schedule to the research underground. Today, still wanted by the activist community, they survive as proovers of fortune. If you have a problem that no one else can solve, and if you can find them, maybe you can hire The A-Team.

Agingcoder 3y ago
That’s funny thanks :-)
082349872349872 3y ago
My favourite bit of every episode was the iconic ὅπλισις when Prof. Dr. P.H.D. Baracus first adds structure preserving maps to every object in sight then uses the snake lemma to weld them together with connecting homomorphisms. "I pity the fool who doesn't chase diagrams"
- CobrastanJorji 3y ago
  I got a little sick of the recurring joke where Prof. Dr. Baracus would complain about flat, two-dimensional, infinite surfaces, and then the team would trick him into using one anyway.
  - jfengel 3y ago
    Goddamn that's a long way to go to make that joke. Worth the journey, but those are brain cells I haven't used in decades. I really wish I could garbage-collect some of the 1980s pop culture neurons and put them to better use.
    - shrimp_emoji 3y ago
      I feel like this about Call of Duty maps.
    - sumtechguy 3y ago

kleiba 3y ago

What do you think, how long until we can give conjectures to a specially trained LLM to come up with a proof?

brap 3y ago
My uneducated hunch is that we’re just a few years away from “proof search” being a solved problem. But that’s only a part of mathematical research.
- prmph 3y ago
  I think you are much too optimistic. Proof verification, though still hard to automate, seems at least tractable. I'm not a mathematician by any means, but something tells me automated proof search, in the general case, would require solving the halting problem, which means it is impossible even in principle.
  - dumbo-octopus 3y ago
    In the general case, proof search is obviously impossible, for the reason you state. But the case need not be general. A proof search machine that takes in a theorem and outputs `"proof: ..." | "antiProof: ..." | "idk"` would be quite powerful indeed.
    - gpm 3y ago
      def decider(_): print("idk") Done ;) --- More seriously, the benchmark would be something along the lines of "and it is better at finding proofs than humans are", like how chess engines haven't solved chess, but they are so much better than humans that they always win in a competition between the two. There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically.
      - brap 3y ago
        >There's no good reason to think that humans are capable of finding proofs that are hard to find algorithmically That’s really all I was trying to say, not sure why I’m getting downvoted

logtempo 3y ago

Yesterday I was wondering if it's possible to have an AI that can "recreate" the mathematics as we know it, and even go further and explore unexplored paths. Though prduced by a video explaining how AI helped to find optimization in the computation of matrix multiplication.

jmj 3y ago
I am working on that for my PhD!
- logtempo 3y ago
  Ho, that's really cool! Sounds a bit like digging your own grave as mathematician but it must be very challenging
082349872349872 3y ago
Unfortunately it's too late to give Theory Mine theorems named after your loved ones as gifts this year: https://www.theorymine.com/home https://www.theorymine.com/home

wslh 3y ago

BTW "Katalin Marton’s Lasting Legacy" [1] [1] https://ee.stanford.edu/~gray/Kati_Marton.pdf https://ee.stanford.edu/~gray/Kati_Marton.pdf

swayvil 3y ago

You always hear "the map is not the territory". Which is to say, names are applied, models are asserted and all our fine ideas about the world are our own contrivance, not the world's. But how close could we get?

oldandtired 3y ago
Not very close at all. Every map that is made leaves out an enormous amount of the territory because that detail is irrelevant to the map being used or created. The more detailed the map is, the more one should recognise just how much more detail is being ignored. If you want to get close, just go to the territory itself and be there directly. All too often, we use mathematics as a map for the actual world around and to keep that map manageable, we have to ignore much of the actual world.
- swayvil 3y ago
  The trick would be to find a real phenomenon that expresses itself symbolically. Like discovering an animal born with a nametag. I think you'd have to look in the realm of thought for that. Surely it isn't just empty space where we build our memories and models. Surely it has its own landscape.

oldandtired 3y ago

Now that it has been done in Lean, how about the version that can be put into Metamath?