6 ms·

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 th

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.

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.