Computer proof ‘blows up’ centuries-old fluid equations • Hacker News Board

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

#191

Post by nico » Sat, Nov 19, 2022, 10:28 PM UTC

prolyxis wrote: post #143

nuclearnice1 wrote: post #130

Earlier quoted context omitted.

What a wonderfully informative and educational comment. Thank you. Would you also be able to shed some light on what a singularity is? It was not intuitive to me that incompressiblity should lead to a singularity. The article dances around the term: > At that point, the Euler equations are said to give rise to a “singularity” — or, more dramatically, to “blow up.” > Once they hit that singularity, the equations will…

A simple example of a function with a singularity is f(t)=1/t. Note that at t=0, f(t) is undefined due to division by zero. On either side of zero, the absolute value of f(t) approaches infinity. In this case, we are tracking the flow of an incompressible fluid over time. This flow is represented by a velocity field evolving over time, under the constraint of no net inflow/outflow of material into any region of space…

Thank you for the great explanation.

Do these swirls shed energy? Is it considered in these equations that for example friction within the swirls would slow them down (and hence not reach a singularity)?

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

#192

Post by [deleted] » Sat, Nov 19, 2022, 11:09 PM UTC

e12e wrote: post #55

jules wrote: post #49

Earlier quoted context omitted.

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?

[deleted]

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

#193

Post by pas » Sat, Nov 19, 2022, 11:16 PM UTC

nico wrote: post #191

prolyxis wrote: post #143

Earlier quoted context omitted.

A simple example of a function with a singularity is f(t)=1/t. Note that at t=0, f(t) is undefined due to division by zero. On either side of zero, the absolute value of f(t) approaches infinity. In this case, we are tracking the flow of an incompressible fluid over time. This flow is represented by a velocity field evolving over time, under the constraint of no net inflow/outflow of material into any region of space…

Thank you for the great explanation. Do these swirls shed energy? Is it considered in these equations that for example friction within the swirls would slow them down (and hence not reach a singularity)?

In real fluids yes, absolutely, they basically transform/branch/divide/split into smaller and smaller scale vortices and then those dissipate the energy into the fluid (heating it up a bit).

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

#194

Post by jojobas » Sat, Nov 19, 2022, 11:56 PM UTC

eesmith wrote: post #63

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).

We know "planet" is a social construct because the astronomers decided, some years back, that Pluto wasn't a planet. And the rules they created to make that definition only apply in the Solar System, not to exoplanets around other stars nor to rogue/free-floating planets. And Ceres, Pallas, Juno, and Vesta were considered planets for over half a century.

In order to decide whether Pluto is a planet, one has to assume that there are, in fact, planets. This assumption is not social in nature, it's language describing natural, inarguable phenomena.

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

#195

Post by auggierose » Sun, Nov 20, 2022, 12:39 AM UTC

ChadNauseam wrote: post #158

auggierose wrote: post #87

Earlier quoted context omitted.

Not many do this currently, that is true. But this will change. In a hundred years every mathematician will do this. I think it will reach "mainstream" much much earlier than this, probably around 2030.

Probably by 2030 and by 2040 at the latest, you will be able to give a proposition to a machine learning model and the model will output a machine-verifiable proof of its truth or falsity at least as often as a human can.

It's not that easy. Humans often work weeks, months, or even years towards proving a theorem. They need to build new theories for it, generalise the theorem, etc., before the proof becomes possible. I would not expect machines to be able to prove any of those theorems by 2030 automatically without human guidance (but maybe I am too pessimistic!) I definitely would expect machines to be able to do the sort of effortless small step reasoning that humans are capable of, and that's really all that is needed for proof assistants to go main stream. It is already possible to a certain extent now, but it needs to get a whole lot better.

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

#196

Post by acchow » Sun, Nov 20, 2022, 2:24 AM UTC

wwalker3 wrote: post #101

The question that the referenced paper (1) is trying to answer is "do the 3D incompressible Euler equations develop a finite time singularity from smooth initial data of finite energy?" This is an important question in the theory of nonlinear partial differential equations, but is probably not as relevant to real fluid flow as a lay reader might imagine. The incompressible Euler equations model a very strange and unp…

The infinite implied speed is of course because the Euler equations are just a rough approximation of what is happening, right? Much like Newtonian physics was an approximation?

There’s a real causality bound of the speed of light

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

#197

Post by fuzzfactor » Sun, Nov 20, 2022, 3:54 AM UTC

wwalker3 wrote: post #183

vba616 wrote: post #172

Earlier quoted context omitted.

>The incompressible Euler equations model a fluid as a two-valued field. This means that at every point in space, the field has two values, density and velocity I don't get it. If the fluid is incompressible, how can density have a value at every point in space? Isn't it just a constant?

The density can be constant, but it doesn't have to be. If the density field starts out with some variation in it, then those variations move around as the fluid flows. Incompressibility just means that those density variations can't get bigger or smaller, they can only move, shear, and rotate.

When you work with near-supercritical and supercritical fluids under laboratory conditions, you can turn the pump by hand and you feel when the density hits the ceiling.

So you know something is up.

Systems would be modeled mathematically using a fluid's individual component values, but we were paid for the real-world laboratory data.

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

#198

Post by 1letterunixname » Sun, Nov 20, 2022, 5:56 AM UTC

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…

Infinite values are representable in IEEE floating point.

I think the author didn't understand the concepts of precision, range, or of arbitrary precision calculations, and so mades bullshit proclamations without sufficient understanding of the fundamentals.

PS: I notice many people I work with (in MAANG) lack an understanding of Computer Science, aren't formally educated, and lack curiosity. It's discouraging because they also lack concern for code craftsmanship and don't know how to use a debugger. This and they're paid $350-450k / year. If you had to recommend a computer science postgraduate program, which would you choose?

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

#199

Post by qazxcvbnm » Sun, Nov 20, 2022, 6:23 AM UTC

naasking wrote: post #182

auggierose wrote: post #178

Earlier quoted context omitted.

> Godel showed that there is no such thing as a universal logic in our current approach to formal systems, but that didn't suddenly make logic non-objective. It simply means that there is no Ur-logic that can subsume all other logics (which is why most assert that Godel ended Hilbert's program). Could you elaborate on that? Any references?

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 unable to quite get at it.

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

#200

Post by eesmith » Sun, Nov 20, 2022, 6:48 AM UTC

jojobas wrote: post #194

eesmith wrote: post #63

Earlier quoted context omitted.

We know "planet" is a social construct because the astronomers decided, some years back, that Pluto wasn't a planet. And the rules they created to make that definition only apply in the Solar System, not to exoplanets around other stars nor to rogue/free-floating planets. And Ceres, Pallas, Juno, and Vesta were considered planets for over half a century.

In order to decide whether Pluto is a planet, one has to assume that there are, in fact, planets. This assumption is not social in nature, it's language describing natural, inarguable phenomena.

Does "marriage" exist, as a "natural, inarguable phenomena" independent of its social construct?

What about "US citizen"?

I don't think so.

Which means we can't say the existence of a word means its the result of a physical assumption.

When you wrote "planets, stars", did you not assume those two are different? But originally, "planet" meant "wandering star" - a planet was assumed to be a type of star.