Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Computer proof ‘blows up’ centuries-old fluid equations

quantamagazine.org

Post reply on HN
Print view View original

51–60 of 223 posts

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

#51

Post by prmph »

auggierose wrote: post #33
Agingcoder wrote: post #2

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…

It certainly is a social construct, because what tools are at my disposal to convince someone who disagrees otherwise? In that sense everything is a social construct. Apart from that, with the help of computers, it can be made absolutely precise and clear which statements follow from which axioms, and in that sense it is not a social construct at all. It also is much less cumbersome than it used to be, and will conti…

> Apart from that, with the help of computers, it can be made absolutely precise and clear which statements follow from which axioms, and in that sense it is not a social construct at all.

I think you are mistaken. The idea that math proofs are a social construct relates to, in my view, much deeper ideas than you seem to think [1].

It is not just that convincing other mathematicians that a proof is correct is a social process, but also that the reasoning on which any proof relies, even if it seems unassailable, even if built into an automated checker, is still a product of the human mind. Usually there is a level of logic that can challenge even what seems so basic as to be fool-proof.

Take the proof that the square root of 2 is irrational. The proof relies on a contradiction that arises if one assumes the root is rational, but one can imagine a logic system where such a contradiction does not imply that the original assumption is false. How possible, you say? It's all math, where one is allowed any starting assumptions, and works out the implications of those.

But, there is something deeply satisfying about thinking that contradictions are (or should be) impossible in our universe, and so this "proof" seems solid.

1. https://plato.stanford.edu/entries/intuitionism/

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

#52

Post by prmph »

AnonCoward42 wrote: post #22
mpweiher wrote: post #11

Earlier quoted context omitted.

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 mathe…

> The proof is not a social construct. > The truth is. Yeah, that is how it feels like nowadays, however the truth is bound in a narrow set of assumptions. These assumptions are bound in reality even in mathematics (One apple is one apple, you add another one, you have two). And while there is an epistemologic level to reality, you would dismiss reality entirely by calling it a social construct. The details of how a…

Imagine a universe, where, when you combine two apples (or really anything), you always, through some weird physical process, ended up with three items.

Would that invalidate (or not), the statement that 1 + 1 = 2?

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

#53

Post by prmph »

jojobas wrote: post #25
yazaddaruvala wrote: post #18

Earlier quoted context omitted.

1+1=2 is a social construct. It’s simple, repeatable and therefore programable - but still a social construct.

Well if "1+1=2" is a social construct then "there are planets, stars, and, in general, objects" is also a social construct. No kind of society can make 1+1=3, and also there is mathematical proof that 1+1=2 (built of course on some sort of axioms that somebody might also consider social constructs).

Imagine a universe, where, when you combine two apples (or really anything), you always, through some weird physical process, end up with three items.

Would that invalidate (or not), the statement that 1 + 1 = 2?

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

#54

Post by thaumasiotes »

Karliss wrote: post #32
thaumasiotes wrote: post #10

> 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…

Sure calculating infinity is easy as long as you redefine "infinity" to be something which isn't actual infinity. But it's useless for many mathematical proofs. Having overflow of some finite floating point calculations labelled as "infinity" is useful for calculations of some practical problems, but it shouldn't be confused with the actual mathematical concept of infinity just because both use the same word.

Floating point infinity is "actual infinity". It has all the correct mathematical properties. If you want to slam a special IEEE constant, you should slam 0, which has different properties from mathematical zero.

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

#55

Post by e12e »

jules wrote: post #49
Agingcoder wrote: post #2

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…

There are (short) computer programs where you input a mathematical proposition and a proof in a kind of proof programming language, and the program will then check if it's a valid proof. Saying that mathematical truth is a social construct is technically true but misses the point entirely.

How does one decide which axioms to build on?

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

#56

Post by thaumasiotes »

mjburgess wrote: post #29
thaumasiotes wrote: post #17

Earlier quoted context omitted.

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

A computer is always just a function from {0,1}^N -> {0,1}^M The "Inf" interpretation, of, eg., 11111111111111111 isnt infinity. And, in general, almost every function isnt representable on the discrete domain above. floats are a hacky interpretation of discrete bit patterns

> A computer is always just a function from {0,1}^N -> {0,1}^M

> The "Inf" interpretation, of, eg., 11111111111111111 isnt infinity.

This is incoherent nonsense. If you want to say that the floating point value "infinity" isn't really infinity, you must also say that nothing else is really infinity either. That is true in a completely useless and uninformative sense, but it's false in every sense a person would ever use. And it fails to distinguish the correct mathematical proof demonstrating an infinite limit from the simulation suggesting, but not demonstrating, an infinite limit. Neither of them is really infinity. Each of them can represent infinity just as accurately as the other, though.

A paper is just a function from a bounded countable subset of ℝ² to another bounded countable subset of ℝ². What would you conclude, from that, about the limitations of what you can represent on paper?

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

#57

Post by e12e »

somat wrote: post #21

"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" Why not? Is it impossible to calculate infinite values in general? I suspect not, My understanding is that a lot of calculus is in fact on how to calculate infinite values. And a computer is a universal machine, this means that while it can not calculate everythin…

> Is it impossible to calculate infinite values in general?

I would say that it's impossible in a finite universe to calculate infinite values. But it's quite possible to define and manipulate relationships that involve infinity.

You can't calculate the sum of all integers - but you can relate it to the sum of all real numbers. Or compare the sum of all integers lager than one hundred, to the sum of all integers larger than ninety.

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

#58

Post by ookdatnog »

rapsey wrote: post #3
Agingcoder wrote: post #2

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.

I think you can make a philosophical argument that a fully formal proof, where every claim is traced all the way back to the axioms, is not a social construct.

But when we say "proof", we usually don't mean "fully formal proof", and there are good reasons why:

1. Fully formal proofs didn't exist for most of the history of mathematics. 2. School by and large don't teach formal proofs, and most students are probably not aware of the existence of formal proofs. 3. Even today, most professional mathematicians never write formal proofs, except perhaps as an exercise during their education.

So what do we mean by "proof" if it is not an argument that is exhaustively traced back to axioms? It's really no more than "that which the teacher/other mathematicians will accept as a convincing argument". When you learned a proof of the Theorem of Pythagoras in high school, you almost certainly didn't learn a fully formal proof. You learned a proof that, at some point, just implicitly got "cut off": the proof tree didn't work all the way back to the axioms but stopped at some point where the argument would become too tedious to continue laying out in full (without even being told that the proof got cut off: your teachers perhaps even told you that this was a rigorous argument).

To write such a proof, you need to judge where the acceptable cut-off point is, which is entirely based on what other people will accept as good work. Hence, a social construct.

edit: if you're not convinced that the proofs you learn in school/university aren't fully rigorous, I warmly recommend trying out a proof assistant like Coq, Agda, or Lean. Try to encode some well-known piece of mathematics. Euclid's Elements is a good candidate: working through it fully formally, you'll find huge omissions in the Elements immediately.

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

#59

Post by fay59 »

somat wrote: post #21

"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" Why not? Is it impossible to calculate infinite values in general? I suspect not, My understanding is that a lot of calculus is in fact on how to calculate infinite values. And a computer is a universal machine, this means that while it can not calculate everythin…

In context, it sounds like they relied on simulations that don’t use exact numbers. I’m guessing that they saw an IEEE-754 floating-point infinity and then had to determine whether they got it because the accurate result was infinity or if the infinity they saw was the result of floating-point calculation artifacts.

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

#60

Post by eesmith »

prmph wrote: post #53
jojobas wrote: post #25

Earlier quoted context omitted.

Well if "1+1=2" is a social construct then "there are planets, stars, and, in general, objects" is also a social construct. No kind of society can make 1+1=3, and also there is mathematical proof that 1+1=2 (built of course on some sort of axioms that somebody might also consider social constructs).

Imagine a universe, where, when you combine two apples (or really anything), you always, through some weird physical process, end up with three items. Would that invalidate (or not), the statement that 1 + 1 = 2?

1 cloud combined with 1 cloud gives 1 cloud.
Post reply on HN