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

31–40 of 223 posts

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

#31

Post by mjburgess »

jojobas wrote: post #28
mjburgess wrote: post #24

Earlier quoted context omitted.

Almost all functions aren't computable, as they aren't discrete. A "computer" is just a function from {0,1}^N -> {0,1}^M

Symbolic engines are way above and beyond number crunching in many respects.

Mathematics is constrained by properties of abstract objects that the symbols are about.

Here, for example, the mathematician has to imagine a scenario to describe with mathematics (two couter-flow fluids, etc.). The notation gains its meaning from this imagined scenario.

Rules for manipulating symbols are therefore insufficient. The proof has to follow from the scenario, which the machine is unable to represent.

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

#32

Post by Karliss »

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.

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

#33

Post by auggierose »

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 continue to improve quickly.

I can sit down and prove something using a tool like Isabelle, and I will be as sure of its "truth" as I can possibly be, and it really doesn't matter what other people, mathematicians or not, think about it. That's the beauty of it.

Of course, you could say my belief in Isabelle is also a social construct. Except it is not, I know exactly how Isabelle works. There could be issues with Isabelle, but these issues adding up to make my proof wrong are very unlikely, especially in addition to my independent understanding of the proof.

But of course, it is much nicer if others can see the same truth that I do, and for this, computer-assisted proof is actually great, because it allows to understand and trust in the high-level structure of a proof without having to verify every little gritty low-level detail.

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

#34

Post by zozbot234 »

ThereIsNoWorry wrote: post #20
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…

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

> because the inherently subjective "elegance" and "beauty" gets lost in translation.

That's a very subjective POV, and perhaps one that varies by area of math. Many computer proof developments are more cleanly refactored/abstracted than the manual equivalent, because it's so easy to refactor a computer proof without worrying that the new proof might fail to prove the same statement.

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

#35

Post by marginalia_nu »

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…

An ideal computer is an universal machine. A real computer has real limitations on what is calculable, even among the things that are theoretically calculable.

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

#36

Post by Karliss »

thaumasiotes wrote: post #17
blurbleblurble wrote: post #13

Earlier quoted context omitted.

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.

Just because some people decided to label floating point overflow conditiona as "infinity" doesn't mean it can actually represent values up to infinity.

There are ways of getting floating point infinity which doesn't involve overflow like dividing by there. But with exception of most trivial cases you have the same problem. You can't know whether you had actual 0 or value closer to 0 than what floating point can represent.

All of that of course depends on how floating point unit or calculation environment is configured. It's probably possible to configure it so that overflows/underflows report an error instead of simply returning "inf".

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

#37

Post by krcz »

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's a social construct in the the same sense anything not directly verifiable using senses is. Is there an Eiffel tower in Paris? Most people haven't seen it, so they can only accept the social consensus that it is there.

If one can afford it, they can travel to Paris and check themselves. The same with mathematical truth: if one has means (time, intelligence, access to training), they can check the proof themselves. Otherwise they need to trust the consensus.

So again, is the truth in mathematics just a social construct? In some sense, I guess, but probably not the one some people might assume hearing such a statement.

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

#38

Post by chmod775 »

mjburgess wrote: post #31
jojobas wrote: post #28

Earlier quoted context omitted.

Symbolic engines are way above and beyond number crunching in many respects.

Mathematics is constrained by properties of abstract objects that the symbols are about . Here, for example, the mathematician has to imagine a scenario to describe with mathematics (two couter-flow fluids, etc.). The notation gains its meaning from this imagined scenario. Rules for manipulating symbols are therefore insufficient. The proof has to follow from the scenario , which the machine is unable to represent.

> which the machine is unable to represent.

If you believe that a computer will eventually be able to accurately simulate a human brain, you might as well give up right now.

Since if a computer with all its constraints is able to simulate a human (brain), but cannot do this, then a human can't do it either.

Conversely if a human can do this but a computer can't, then a computer can never simulate a human.

Don't tell this to a software developer working on AI. They might quit their job and become a baker instead.

I don't think you would have any effect on a mathematician, since they would already be acutely aware some things provably cannot be done.

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

#39

Post by TheOtherHobbes »

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…

An apple is not an apple. An apple is a subjective construct that summarises the distinguishing features of a certain kind of object as it appears to our sense.

To a non-human consciousness those features may be uninteresting, irrelevant, or incomprehensible, so they might not see apples at all. But they could see " "s, which we don't even have a concept for, never mind a word. And which we either ignore or possibly don't see at all. (Imagine perceiving complex networked relationships directly instead of having to access them through symbolic models.)

There's no reason why math wouldn't be the same. From experiments we know that cats can't count, but they can distinguish sizes. So cat math likely wouldn't have integers as we know them, but would have some kind of size-based analogue.

I have a theory this is why Hilbert's Project failed and you always end up with an incompleteness theorem.

You cannot create an absolute internally consistent mathematics, because foundational axioms depend on subjective experience, not on objective logic.

So you can define integers in various more and more obscure ways. But fundamentally you have to start with the subjective experience of "integer" as a concept that matters to you. And you can't prove a subjective experience objectively.

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

#40

Post by MarcelOlsz »

mjburgess wrote: post #24
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…

Almost all functions aren't computable, as they aren't discrete. A "computer" is just a function from {0,1}^N -> {0,1}^M

What level of math do I need to be at to "compute" this comment?
Post reply on HN