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

61–70 of 223 posts

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

#61

Post by qazxcvbnm »

prmph wrote: post #51
auggierose wrote: post #33

Earlier quoted context omitted.

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

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

I think you are mistaken.

I used to be very troubled by the notion that no single set of axioms really can be agreed on to do mathematics, but I have been convinced finally that the truth of the matter is a very subtle point; that the truth of mathematics is absolute; it merely is not finitely-axiomatisable.

With a sufficiently weak proof system, clearly we can conceive of a system where the irrationality of the square root of 2 is not provably true, but no consistent proof system can prove that the square root of 2 is rational. Certain mathematical constructs, indeed most(*) of known mathematics, that which is constructible by constructivist methods, are irrefutably there in any consistent mathematical universe, and in that sense, true.

Yet, no single axiom system can encompass all mathematical truth, as is well known from Goedel's theorems, but neither does that mean that the set of axioms to be worked with can be arbitrarily chosen. The chosen set of axioms must be consistent. The question, then, is whether consistency of axioms can possibly be an objective fact; and even though for any sufficiently strong set of axioms, its consistency cannot be proven in of itself, it consistency can in fact be objectively established - objectively established, but not finitely established.

My evidence for this perspective is Scott Aaronson's construction of a Turing-Machine encoding of the ZFC axioms. What the construction of this encoding implies, is that the revelation of the uncomputable busy-beaver (BB) function for value 8000, which is a finite, well defined, and an objectively irrefutable, albeit unthinkably massive, number, constitutes a proof of the consistency of ZFC axioms. A similar procedure I believe can be applied to any set of axioms that one wishes to work with.

The part where the magic occurs, I believe, is in the uncomputable nature of the BB function, by which it is possible to finally and objectively establish consistency of sets of axioms. Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values; that is the nature I now take of mathematics as well.

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

#62

Post by mjburgess »

thaumasiotes wrote: post #56
mjburgess wrote: post #29

Earlier quoted context omitted.

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…

I'm not sure where your misunderstanding comes from, but at least, you might consider you're disagreeing with an article on quanta magazine which writes up a project by experts in their field.

In any case, no. The idea that a finite number of bits in a particular state "must just be infinity!!!! because the IEEE ref docs say so" is strange to say the least.

The issue is to demonstrate that a given function, say f, for given real-valued inputs, say x, has an output y which is not real-valued and goes to infinity.

A computer cannot demonstrate such a thing, because real-valued functions aren't computable.

No sequence of bit patterns on a computer can ever show the above, because the above is an issue of the limits of a continuous function. Relevant inputs to the function have an infinite precision, and relevant outputs have an infinte precision.

Eg., x = pi, y = pi^100

A computer may very easily mistakenly conclude x = pi is an input which becomes infinite in y, because (1) a computer cannot represent pi; and (2) cannot represent pi^100 either.

infinity isn't a bit pattern; and isn't here in any relevant sense even a number; the IEEE standard may as well have said "Overflow"

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

#63

Post by eesmith »

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

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.

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

#64

Post by auggierose »

prmph wrote: post #51
auggierose wrote: post #33

Earlier quoted context omitted.

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

I am very familiar with those "deep" ideas. It is really just about which axioms you are willing to accept. If you want to deny yourself the law of contradiction, that's fine, go ahead. There are structures where this law doesn't hold if you interpret the logical operators in a special sense, so there are valid reasons for doing so. For example, it is an elegant mechanism to reason inside of Kripke structures.

Personally, I don't think intuitionism makes much sense on a fundamental level beyond being an elegant mechanism in certain situations. If you tell me that it is false that A is false, then certainly A is true. Anything else is really mystic mamboojamboo and not clear thinking. But that's just my opinion, and I am not gonna force it onto you, because this is not something I can prove in a proof-assistant, but just an opinion, and as such a social construct.

I am not really dogmatic about this. You might be able to use intuitionism for things that cannot be done via classical reasoning, for example extract programs from a proof. I have yet to see an example where it is not simpler and more straightforward to just prove an executable program to be equivalent to the specification using classical reasoning.

My point of view is the following: If you are not able to (eventually) make your case within a proof assistant, then what you are trying to tell me is not math.

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

#65

Post by bheadmaster »

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…

The fact that mathematics gives us power to predict events in the real world makes it independent of social consensus.

If everyone in the world believes that 2+2=5, that doesn't make it less true that 2+2=4 - in the sense that I know for sure, if I take throw two rocks on a pile of two rocks, I'll get a pile of four rocks, not five rocks.

I hate this sociologist view that everything depends on the social consensus. Going extreme with it is how you end up in a 1984-esque society:

    Anything could be true. The so-called laws of Nature were nonsense. The law of gravity was nonsense. ’If I wished,’ O’Brien had said, ’I could float off this floor like a soap bubble.’ Winston worked it out. ’If he thinks he floats off the floor, and if I simultaneously think I see him do it, then the thing happens.

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

#66

Post by auggierose »

qazxcvbnm wrote: post #61
prmph wrote: post #51

Earlier quoted context omitted.

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

> 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. I think you are mistaken. I used to be very troubled by t…

> Uncomputability amounts to the acknowledgement that though something may always be well-defined, there is no finite method to encompass its values

That is kind of obvious, isn't it? But some people need more convincing than others :-)

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

#67

Post by agumonkey »

raverbashing wrote: post #43
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…

Because infinity is a mathematical trick, to say where something is going but it is not calculable (it is not a number in itself)

well you end up in bounded axiomatic ranges

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

#68

Post by dorchadas »

qazxcvbnm wrote: post #61
prmph wrote: post #51

Earlier quoted context omitted.

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

> 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. I think you are mistaken. I used to be very troubled by t…

But what this doesn't get at is that the very system of logic we use to make proofs is a social construct. Other cultures have had other systems of logic, and called valid arguments that we wouldn't today precisely because they were using a different system of logic.

So the very foundations of mathematics, the logic we use behind our proofs, is inherently a social construct that arose out of Greek philosophy as it was adapted in the west.

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

#69

Post by dorchadas »

ookdatnog wrote: post #58
rapsey wrote: post #3

Earlier quoted context omitted.

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

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

I don't think you can make this claim really, precisely because the logic we accept as, well, logical, is a social construct. Different cultures across different places have had different ways of accepting what is valid in an argument. The methods of logic we consider valid are themselves social constructs, basically.

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

#70

Post by jfengel »

bheadmaster wrote: post #65
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…

The fact that mathematics gives us power to predict events in the real world makes it independent of social consensus. If everyone in the world believes that 2+2=5, that doesn't make it less true that 2+2=4 - in the sense that I know for sure, if I take throw two rocks on a pile of two rocks, I'll get a pile of four rocks, not five rocks. I hate this sociologist view that everything depends on the social consensus. G…

That's actually an example of what OP was talking about. You have defined + as the operator that mimics what piles of rocks do, and defined numbers as counting rocks.

That's only a tiny fraction of what math does. An interesting and useful one, and mathematicians have put a lot of work into studying basic arithmetic. They have expanded out into numerous other forms, some of which turn out to have correspondence to the real world like non-Euclidean geometry.

Others turn out to be completely abstract and are merely curiosities. There are an infinite number of them, each containing truths, almost all of them of no interest. Interest is defined by mathematicians, not physics. Even so it turns out to sometimes be useful, such as the beautiful theorems of prime numbers that drive Internet security centuries after they were invented.

That is what the OP means. You can make up any axioms you want and prove true theorems. But the hard part is convincing other mathematicians to care.

Post reply on HN