Live data from Hacker News

Computer proof ‘blows up’ centuries-old fluid equations

quantamagazine.org

11–20 of 223 posts

Re: Computer proof ‘blows up’ centuries-old fluid equations

#11
post #3

I remember my math professor at university telling me that truth in mathematics was a social construct, and that nothing was true until a social consensus had been reached between mathematicians. This struck me at the time as a very powerful statement, yet unexpected, since very much not what most people expect from mathematics. After all, it's supposed to be a field where there is such a thing as a (most of the time…

Huh? Mathemathical proof is not a social construct. This makes no sense.

The proof is not a social construct.

The truth is.

The proof is a mechanism to reach that consensus, by convincing other mathematicians of a specific truth. That is all it is.

There is a naive idea that a proof is a purely mechanical series of steps that provides access to truth. Last I checked, this isn't so for the vast majority of proofs in math. Such a proof would be way too tedious to construct or check by mathematicians. And if it isn't checkable, how do we know it is actually true?

Automated proofs are a subfield, and (again, last I checked) controversial because they can often not be checked by humans.

So for example, if the proof doesn't convince other mathematicians, then it's not a a proof.

Or it might convince other mathematicians and later turn out to be wrong after all.

For more on the practical aspects of math, I highly recommend The Mathematical Experience.

https://www.amazon.com/Mathematical-Experience-Phillip-J-Dav...

I read it in German:

https://www.amazon.com/Erfahrung-Mathematik-German-P-J-Davis...

Re: Computer proof ‘blows up’ centuries-old fluid equations

#12
post #3

I remember my math professor at university telling me that truth in mathematics was a social construct, and that nothing was true until a social consensus had been reached between mathematicians. This struck me at the time as a very powerful statement, yet unexpected, since very much not what most people expect from mathematics. After all, it's supposed to be a field where there is such a thing as a (most of the time…

Huh? Mathemathical proof is not a social construct. This makes no sense.

There's a difference between a mathematical proof and accepted truths.

When you learn math at school, at first you're just told that these things are true, and so it becomes an accepted truth how addition works.

Only much later can you go and verify the proof from the axioms.

Similarly, if someone today relies on Fermat's last theorem to hold for some of their own work, they're unlikely to have verified the entirety of Wile's proof. Rather they lean upon the experts who have, and thus have accepted the truth that the proof holds.

Re: Computer proof ‘blows up’ centuries-old fluid equations

#13

> Hou and Luo’s work was suggestive, but not a true proof. That’s because it’s impossible for a computer to calculate infinite values. It can get very close to seeing a singularity, but it can’t actually reach it — meaning that the solution might be very accurate, but it’s still an approximation. I feel certain that if you run a process that approaches infinity using ordinary floating-point numbers, you will actually…

Double precision floats have a maximum value of 1.7976931348623158 E + 308

Re: Computer proof ‘blows up’ centuries-old fluid equations

#14

I remember my math professor at university telling me that truth in mathematics was a social construct, and that nothing was true until a social consensus had been reached between mathematicians. This struck me at the time as a very powerful statement, yet unexpected, since very much not what most people expect from mathematics. After all, it's supposed to be a field where there is such a thing as a (most of the time…

Is it because maths is "incomplete" ala godel incompleteness theorem?

Re: Computer proof ‘blows up’ centuries-old fluid equations

#15

> Hou and Luo’s work was suggestive, but not a true proof. That’s because it’s impossible for a computer to calculate infinite values. It can get very close to seeing a singularity, but it can’t actually reach it — meaning that the solution might be very accurate, but it’s still an approximation. I feel certain that if you run a process that approaches infinity using ordinary floating-point numbers, you will actually…

Double precision floats have a maximum value of 1.7976931348623158 E + 308

Aka not infinity

Re: Computer proof ‘blows up’ centuries-old fluid equations

#16

I remember my math professor at university telling me that truth in mathematics was a social construct, and that nothing was true until a social consensus had been reached between mathematicians. This struck me at the time as a very powerful statement, yet unexpected, since very much not what most people expect from mathematics. After all, it's supposed to be a field where there is such a thing as a (most of the time…

> and that nothing was true until a social consensus had been reached between mathematicians.

So how do calculators and computers work then?

Re: Computer proof ‘blows up’ centuries-old fluid equations

#17

> Hou and Luo’s work was suggestive, but not a true proof. That’s because it’s impossible for a computer to calculate infinite values. It can get very close to seeing a singularity, but it can’t actually reach it — meaning that the solution might be very accurate, but it’s still an approximation. I feel certain that if you run a process that approaches infinity using ordinary floating-point numbers, you will actually…

Double precision floats have a maximum value of 1.7976931348623158 E + 308

That is not correct; they have a maximum value of positive infinity. See what you get when you square 1.7e+307.

Re: Computer proof ‘blows up’ centuries-old fluid equations

#18

I remember my math professor at university telling me that truth in mathematics was a social construct, and that nothing was true until a social consensus had been reached between mathematicians. This struck me at the time as a very powerful statement, yet unexpected, since very much not what most people expect from mathematics. After all, it's supposed to be a field where there is such a thing as a (most of the time…

> and that nothing was true until a social consensus had been reached between mathematicians. So how do calculators and computers work then?

1+1=2 is a social construct.

It’s simple, repeatable and therefore programable - but still a social construct.

Re: Computer proof ‘blows up’ centuries-old fluid equations

#19
post #15

Earlier quoted context omitted.

Double precision floats have a maximum value of 1.7976931348623158 E + 308

Aka not infinity

They meant maximum finite value.

0 11111111111 0000000000000000000000000000000000000000000000000000 (base 2) ≙ 7FF0 0000 0000 0000 (base 16) ≙ +∞ (positive infinity)

1 11111111111 0000000000000000000000000000000000000000000000000000 (base 2) ≙ FFF0 0000 0000 0000 (base 16) ≙ −∞ (negative infinity)

Re: Computer proof ‘blows up’ centuries-old fluid equations

#20

I remember my math professor at university telling me that truth in mathematics was a social construct, and that nothing was true until a social consensus had been reached between mathematicians. This struck me at the time as a very powerful statement, yet unexpected, since very much not what most people expect from mathematics. After all, it's supposed to be a field where there is such a thing as a (most of the time…

I don't know why you're being downvoted, but that is a perfectly valid statement.

Everyone thinks proofs are this holy grail and totally rigorous, and they are on a certain level. But the idea is floating around that Mathematicians are infallible when in fact lots of proofs in highly complex areas of mathematics are NOT 100% perfectly rigorous. They contain a lot of skipping, because "it's trivial" and consensus.

This approach may work very often, but there is a danger that sometimes it doesn't work and things get overlooked. Since mathematics is done in a bottom-up approach, at some point some fundament may or may not turn out to be wrong, which endangers parts built on top of it.

The whole movement of rigorous automated proof systems is to prove mathematics from the very bottom to the very top in a 100% rigorous and verifiable way.

Doing actual rigorous proofs a computer can verify is enormously tedious and many Mathematicians dislike it for that reason, because the inherently subjective "elegance" and "beauty" gets lost in translation.

Post reply on HN