6 ms·

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not

> The experts are in agreement that the important ideas are robust enough to withstand knocks like this, but the details of what is actually going on might not actually be where you expect them to be. Past researcher in pure math here. The big problem is that mathematicians are notorious for not providing self-contained proofs of anything because there is no incentive to do so and authors sometimes even seem proud to "skip the details". What actually ends up happening is that if you want a rigorous proof that can be followed theoretically by every logical step, you actually need an expert to fill in a bunch of gaps that simply can't easily be found in the literature. It's only when such a person writes a book explaining everything that it might be possible, and sometimes not even then. The truth is, a lot of modern math is on shaky ground when it comes to stuff written down.

uffjedn 2y ago
Studied math a long time ago and one of my profs was proud about not going into the details. He said "Once you did something 100 times, you can go and say -as easily observable- and move on."
- brobdingnagians 2y ago
  I loved that some of the proof solutions in the back of mathematical logic book said, "Observe that ..." as the start of the proof. Our little study group definitely did not see how what followed was an observation we would have made.
  - moomin 2y ago
    Baker's little book of number theory made me work to get through every page...
- inglor_cz 2y ago
  I was an algebra major at the turn of the century and I hated that attitude. For the prof, yeah, easily observable. What about the students who try to absorb that particular article? You already have to balance the main topic in your brain, and you get these extra distractions on top of it.
hyperthesis 2y ago
There'a a story that when someone wrote up a famous mathematician's work (Euler?), he found many errors, some quite serious. But all the theorems were true anyway. Sounds like Tao's third stage, of informed intuition.
- pfdietz 2y ago
  Back in Euler's time there as a lot of informality. The rigor of the second half of the 19th century was still some time in the future.
- hughesjj 2y ago
  It's still incredibly painful as a learner though when things don't quite pan out. You start gaslighting yourself and then handwaved/convince yourself away that this must be true given how consistent all the "downstream" work is, and that you just don't fully understand it. So, I agree with the author that this is super helpful, even if we know the proofs are "true" in the end
impendia 2y ago
Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone with a good background in high school math. Prove the following statement: there exist constants C, X > 0 such that for every real number x > X, we have log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx. i.e. the left-side is big-O of the right. This flavor of statement comes up all the time in analytic number theory (my subject), would be regarded as obvious to any specialist, and in a paper would be invariably stated without proof. To come up with a complete, rigorous proof would be long, and not interesting. No professional would want to read one. I agree this attitude comes with some tradeoffs, but they do seem manageable.
- ted_dunning 2y ago
  I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e. It would be annoying to have to code that kind of statement every time, but it wouldn't add that much to the effort. Formalizing is still enormously hard, but I don't think that this is the example to hang the argument on.
- vouaobrasil 2y ago
  > but to truly provide all the details would make papers far, far longer. I think what we need in math is that eventually, a collection of frequently cited and closely related papers should be rewritten into a much longer book format. Of course some people do that, but they hardly get much credit for it. It should be much more incentivated, and a core part of grant proposals.
  - jll29 2y ago
    Donald Knuth's literate computing could be an example to follow: combine lean prove language with inline English human language that explains it. Then, Lean files can be fed into Lean to check the proof, and LaTeX files can be fed into LaTeX to produce the book that explains it all to us mere mortals.
rendaw 2y ago
I have no background in math, so this might be naive, but shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps? IIUC you're saying that basically someone with a mental database should be able to identify preconditions matching some theorem and postconditions aligned with the next statement from their mental database. Or is there math that can't be expressed in a way for proof checkers to assess atm? Edit: Or maybe proof checker use just isn't as wide-spread as I imagined. It sounds like the state statically typed languages in programming...
- JulianWasTaken 2y ago
  > shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps? This is essentially exactly what Mathlib[1] is, which is Lean's database of mathematics, and which large portions of the FLT project will likely continually contribute into. [1]: https://github.com/leanprover-community/mathlib4/ https://github.com/leanprover-community/mathlib4/ (Other theorem provers have similar libraries, e.g. Coq's is called math-comp: https://math-comp.github.io/ https://math-comp.github.io/ )
paulddraper 2y ago
Has that ever blown up their faces? I.e. a widely accepted proof that had a critical flaw due to hand waving? If it hasn't, I would understand why they'd be cavalier about explicit details.
- mydogcanpurr 2y ago
  Yes, famously the Italian school of algebraic geometry ran into foundational issues. See https://en.wikipedia.org/wiki/Italian_school_of_algebraic_geometry#Collapse_of_the_school https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge....

uffjedn 2y ago

Studied math a long time ago and one of my profs was proud about not going into the details. He said "Once you did something 100 times, you can go and say -as easily observable- and move on."

brobdingnagians 2y ago
I loved that some of the proof solutions in the back of mathematical logic book said, "Observe that ..." as the start of the proof. Our little study group definitely did not see how what followed was an observation we would have made.
- moomin 2y ago
  Baker's little book of number theory made me work to get through every page...
inglor_cz 2y ago
I was an algebra major at the turn of the century and I hated that attitude. For the prof, yeah, easily observable. What about the students who try to absorb that particular article? You already have to balance the main topic in your brain, and you get these extra distractions on top of it.

hyperthesis 2y ago

There'a a story that when someone wrote up a famous mathematician's work (Euler?), he found many errors, some quite serious. But all the theorems were true anyway. Sounds like Tao's third stage, of informed intuition.

pfdietz 2y ago
Back in Euler's time there as a lot of informality. The rigor of the second half of the 19th century was still some time in the future.
hughesjj 2y ago
It's still incredibly painful as a learner though when things don't quite pan out. You start gaslighting yourself and then handwaved/convince yourself away that this must be true given how consistent all the "downstream" work is, and that you just don't fully understand it. So, I agree with the author that this is super helpful, even if we know the proofs are "true" in the end

impendia 2y ago

Speaking as a current researcher in pure math -- you're right, but I don't think this is easily resolved. Math research papers are written for other specialists in the field. Sometimes too few details are provided; indeed I commonly gripe about this when asked to do peer review; but to truly provide all the details would make papers far, far longer. Here is an elementary example, which could be worked out by anyone with a good background in high school math. Prove the following statement: there exist constants C, X > 0 such that for every real number x > X, we have log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cx. i.e. the left-side is big-O of the right. This flavor of statement comes up all the time in analytic number theory (my subject), would be regarded as obvious to any specialist, and in a paper would be invariably stated without proof. To come up with a complete, rigorous proof would be long, and not interesting. No professional would want to read one. I agree this attitude comes with some tradeoffs, but they do seem manageable.

ted_dunning 2y ago
I don't think that is a great example since it only takes a moment to see the loose bounds C, X = 3, e. It would be annoying to have to code that kind of statement every time, but it wouldn't add that much to the effort. Formalizing is still enormously hard, but I don't think that this is the example to hang the argument on.
vouaobrasil 2y ago
> but to truly provide all the details would make papers far, far longer. I think what we need in math is that eventually, a collection of frequently cited and closely related papers should be rewritten into a much longer book format. Of course some people do that, but they hardly get much credit for it. It should be much more incentivated, and a core part of grant proposals.
- jll29 2y ago
  Donald Knuth's literate computing could be an example to follow: combine lean prove language with inline English human language that explains it. Then, Lean files can be fed into Lean to check the proof, and LaTeX files can be fed into LaTeX to produce the book that explains it all to us mere mortals.

rendaw 2y ago

I have no background in math, so this might be naive, but shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps? IIUC you're saying that basically someone with a mental database should be able to identify preconditions matching some theorem and postconditions aligned with the next statement from their mental database. Or is there math that can't be expressed in a way for proof checkers to assess atm? Edit: Or maybe proof checker use just isn't as wide-spread as I imagined. It sounds like the state statically typed languages in programming...

JulianWasTaken 2y ago
> shouldn't proof checkers have a database of theorems and be able to fill in the intermediate steps or confirm that it's possible to fill in the missing steps? This is essentially exactly what Mathlib[1] is, which is Lean's database of mathematics, and which large portions of the FLT project will likely continually contribute into. [1]: https://github.com/leanprover-community/mathlib4/ https://github.com/leanprover-community/mathlib4/ (Other theorem provers have similar libraries, e.g. Coq's is called math-comp: https://math-comp.github.io/ https://math-comp.github.io/ )

paulddraper 2y ago

Has that ever blown up their faces? I.e. a widely accepted proof that had a critical flaw due to hand waving? If it hasn't, I would understand why they'd be cavalier about explicit details.

mydogcanpurr 2y ago
Yes, famously the Italian school of algebraic geometry ran into foundational issues. See https://en.wikipedia.org/wiki/Italian_school_of_algebraic_geometry#Collapse_of_the_school https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge....