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

211–220 of 223 posts

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

#211

Post by naasking »

qazxcvbnm wrote: post #199
naasking wrote: post #182

Earlier quoted context omitted.

These are the implications of Godel's incompleteness theorems. No formal system expressive enough to encode arithmetic can simultaneously be both complete and prove its own consistency, because there will always be true propositions expressible in that system that cannot be proven in that system. This is why Hilbert's program to finitely axiomatize mathematics can't be completed. The "escape hatch" here is simply tha…

> there is another possible escape hatch that hasn't been fully explored IMO, and that's some variant of finitism. All these impossibility proofs depend on infinite structures to derive incompleteness or contradiction, but if infinite structures are not expressible... Could you elaborate on what such a formalism where infinite structures are not expressible might look like? It sounds an intriguing notion, though I'm…

Bendegem's paper is a good introduction and overview:

A Defense of Strict Finitism, http://www.jeanpaulvanbendegem.be/strict%20finitism.pdf

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

#212

Post by wwalker3 »

throwaway81523 wrote: post #187
civilized wrote: post #167

Earlier quoted context omitted.

This raises a question I hadn't thought of before. Real-world fluid flow is ultimately well-modeled by the equations of many-body Newtonian mechanics, right (atoms bumping around)? Are those equations vulnerable to blow-ups?

There are all kinds of blow-ups in Newtonian mechanics and in other equations of physics. The singularity at the center of a black hole in general relativity is a famous example. The ultraviolet catastrophe in classical thermodynamics was another. The presumption is that blow-ups in an equation indicate a mismatch between the equation and the true physical world, telling physicists to look for better theories, whose…

That's a great article! 1) I'd seen a lot of other cool stuff from the same author over the years (see https://math.ucr.edu/home/baez/README.html), but had somehow missed this one.

1) "Struggles with the Continuum" by John Baez

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

#213

Post by lambdatronics »

kzz102 wrote: post #165

Computer assisted proof is not a new idea. The most famous example is the four color theorem, which (as far as I know) does not have a humanly understandable proof. For this particular proof, it looks like the computer assisted part would be similar to writing down hundreds of pages of checkable inequalities. One way to do this is to use interval arithmetic, which always guarantees the answer is within the a certain…

> people believe is true, but cannot build upon because they don't fully understand it.

OK, maybe it doesn't help people build on the proof, but does it help computers build on the proof? Why does it have to come back to human understanding? Maybe it's not possible right now for computers to generalize proof strategies, but I wouldn't bet against it becoming possible down the road.

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

#214

Post by feanaro »

mpweiher wrote: post #98
feanaro wrote: post #73

Earlier quoted context omitted.

Saying Mathematics ≠ Reality fails to capture a large portion of the story, since a subset of mathematics is clearly necessary to be able to encode science, and confirmed by science, and is in that sense a part of reality.

It's not necessary. It is empirically useful. Mathematics is about describing possible worlds. Given these assumptions (including the rules of the game), what follows? Science is about figuring out the real world. The real world has no obligation to be describable by mathematics. That it is so describable is fortuitous. "The miracle of the appropriateness of the language of mathematics for the formulation of the laws…

> It's not necessary.

I didn't mean "necessary" in the sense of modal logic, but in a more colloquial sense. Physical laws as known to us today are described using mathematics. We know of no other viable ways to describe them. In that sense, (a subset of) mathematics is necessary for this purpose.

It was just meant as a restatement of the concept of unreasonable effectiveness of mathematics in a more natural language.

> The real world has no obligation to be describable by mathematics.

There is no obligation, but that it is so in our particular world is undeniable fact.

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

#215

Post by prmph »

auggierose wrote: post #148
musingsole wrote: post #128

Earlier quoted context omitted.

> whether any given formal system actually is consistent is not dependent on consensus, it is a fact, either true or false, completely independent of consensus. The definition of "consistent" seems completely entangled with a given social group's ideas of "rational". You might imply that our word for it hints at a Platonic ideal of "consistent", but if that's true, then you're caught in an infinite cascade of which n…

There is a simple definition for what consistent means, which naasking is referring to: is it impossible to derive "false" purely by applying the rules of the logical system?

"False" is meaningless in a logic system that relies on probabilities in stead or true/false.

Even in our commonly used logic system, what does false actually mean?

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

#216

Post by blurbleblurble »

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…

It's always going to be an approximation, and if you do some serious work with computer graphics you'll say some point maybe get a chance to see that the limits of floating point numbers aren't actually as large as they seem. Double precision is way bigger than single precision but still, if computers could actually "reach infinity" there wouldn't be any issues with floating point error in sensitive calculations. But the fact of the matter is that there is.

And at any rate, "infinity" is not a single value to be reached.

Take an analysis class and you'll understand this better!

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

#217

Post by auggierose »

prmph wrote: post #215
auggierose wrote: post #148

Earlier quoted context omitted.

There is a simple definition for what consistent means, which naasking is referring to: is it impossible to derive "false" purely by applying the rules of the logical system?

"False" is meaningless in a logic system that relies on probabilities in stead or true/false. Even in our commonly used logic system, what does false actually mean?

I can point you to my favourite logic ;-) Here false is defined as

   false = (∀x. x)
So in this case, it derives its meaning from whatever the meaning of the ∀ operator is. Its meaning is the result of applying the ∀ operator to the identity operation.

Nobody is questioning that there are different possibilities for logical systems, and different possible semantics for them. The choice of logical system is up to you, and ultimately, part of your assumptions. A proof assistant uses a fixed logical system, and your mathematics needs to fit into this system to be expressible in the proof assistant. Apart from my favourite logic, there are several well-known logical systems commonly assumed to be able to represent all of mathematics more or less faithfully: first-order logic, simply-typed higher-order logic, and dependent type theory.

What I like about my favourite logic is that I believe that all other logics, even quantum logics, can be expressed in it in a straightforward way. This has the advantage that once you expressed your logic in this way, you get the meaning of it for free. Of course, you still need to make sure that this is the intended meaning.

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

#218

Post by prmph »

naasking wrote: post #169
prmph wrote: post #147

Earlier quoted context omitted.

Exactly the point I was making. Many do not seems to see the fundamental issue at play here, and another way to think of them is what you have hinted at: the role of language. There is no objective way to nail down the meaning of words, like "consistent", "proof", "equal", etc. Suppose one wanted a maximally rigorous definition of "equal". Does it mean two things that cause people to think of the same thing when they…

Have you perchance been reading a lot of Wittgenstein? I think you're conflating universality and objectivity. Those terms you list all have objective definitions, but the specific characteristics they have in any given logic may differ. That means they are not universal, but that doesn't make them non-objective. Objective typically means "mind independent". Your example of equality already demonstrates you understan…

Wow, did you read my comment carefully at all? This is what I said:

> This is not to deny that there is an objective reality...

So I do agree that object reality exists, contrary to what you imply in your response.

However, there is no word in human language that has an objective definition. If you think this is so, maybe you have not thought or read enough about the subject.

On the subject of equality, you said: > Your example of equality already demonstrates you understand equality's objective definition: you implicitly operate on the notion that "equality" means some form of equivalence, some ability to substitute B for C in a specific context that results in no observable/expressible change.

You're making my point. Consider the vagueness of what you have written: "...some form of equivalence, some ability to substitute B for C in a specific context that results in no observable/expressible change." That doesn't sound very rigorous to me, and in fact I could argue this is not what I understand by "equality" at all.

Now you could make the point the definition can be made rigorous for a very specific context, but this is still not 100% possible. To show this, you can attempt to give me a specific definition of equality of a specific context, and I will show that it still admits of multiple possible meanings.

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

#219

Post by auggierose »

prmph wrote: post #215
auggierose wrote: post #148

Earlier quoted context omitted.

There is a simple definition for what consistent means, which naasking is referring to: is it impossible to derive "false" purely by applying the rules of the logical system?

"False" is meaningless in a logic system that relies on probabilities in stead or true/false. Even in our commonly used logic system, what does false actually mean?

Do you have a particular logical system based on probabilities in mind? Most likely (pun intended) false will be simply probability 0.

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

#220

Post by musingsole »

auggierose wrote: post #217
prmph wrote: post #215

Earlier quoted context omitted.

"False" is meaningless in a logic system that relies on probabilities in stead or true/false. Even in our commonly used logic system, what does false actually mean?

I can point you to my favourite logic ;-) Here false is defined as false = (∀x. x) So in this case, it derives its meaning from whatever the meaning of the ∀ operator is. Its meaning is the result of applying the ∀ operator to the identity operation. Nobody is questioning that there are different possibilities for logical systems, and different possible semantics for them. The choice of logical system is up to you, a…

You draw lines and insist there's no space between them.
Post reply on HN