Comment by usgroup | Hacker News Reader

Comment by usgroup | Hacker News Reader

This is also well studied in Philosophy.

Even not that hard math proofs call on intuition pretty quickly, and I think it’s a legit question to ask when does it basically become empirical proof.

To my understanding maths has a common basis in set theory but set theory itself is just a common basis for maths (ie as opposed to “the truth”), but even so proofs are typically not given via set theory especially if the theorem is complicated.

The idea is that mechanising proof and making it more algorithmic will make it more like what the layman thought proof is , but it at the same time raises the question, what is this all for? Ie maths is what mathematicians do. I think it admits to no clearer a definition. So it’d probably make sense for mathematicians to decide, what precisely is the role of proof?

The author talks about this in addressing computer aided maths and the general recruitment of applied mathematicians to solve problems whilst caring less to advance “the science” whilst doing it. Chomsky spoke a lot about this in criticising the use of probabilistic models in science as ultimately scarcely contributing to causal understanding, which in itself is separate from being able to predict phenomena well. Ie you can do practical things without ever knowing what’s going on under the hood, but science wants to know what’s going on under the hood and so prefers different approaches to its advancement.

Mathematics has its own version of 'empirical proof': a constructive proof, i.e. demonstrating that a method (algorithm) can construct a particular mathematical object with specific properties.

I don't think it's really the case that all branches of mathematics really have a 'common basis' as much as that they're all equivalent. It's pretty common to map one branch to another, e.g. arithmetic to set theory, but then once that's been done there's no real reason to write proofs in a particular branch in the formalism of another.

> The idea is that mechanising proof and making it more algorithmic will make it more like what the layman thought proof is , but it at the same time raises the question, what is this all for? Ie maths is what mathematicians do. I think it admits to no clearer a definition. So it’d probably make sense for mathematicians to decide, what precisely is the role of proof?

"A New Kind of Science" has some insights about this that I appreciate greatly. Mathematicians don't bother to enumerate everything that's formally ('mechanically') true, even tho there are some interesting truths to be discovered in that fashion. They instead explore the 'tree of truths' based on history, intuition, and even fashion.

Ultimately, even the most mechanical formal systems are, or can be, nebulous and 'philosophically strange'. Consider the axiom of choice as but one example – there are different set theories depending on whether one accepts that axiom as 'reasonable' (or 'true') or not!

I would not equate the term "constructive proof" with "empirical proof". "Constructive proof" would indicate a proof that gives an algorithm that constructs the desired object, or a proof based on a constructive logic. Either of those could be fully rigorous. But I would take "empirical proof" in mathematics as something like "we've verified that this conjecture holds for values up to 10^100", which of course isn't a proof at all in the proper sense.

> Even not that hard math proofs call on intuition pretty quickly

Can you give an example? Nothing jumps to mind from my years of studying mathematics.

Sure. Prove that a Peterson graph can’t have a Hamiltonian cycle. Often given as a paragraph of English. Actually I’ve only seen it that way personally.

Of course you could (in this example) prove it deductively since Peterson graphs have a specific size , or inductively otherwise but you’d first need to establish a framework... and not a “intuitive framework” at that. Well, all you’ve got then is something axiomatic in which case we arrive back at “intuition” for you axioms.

Here’s a whole line of argument about a large part of the proof we know:

https://en.m.wikipedia.org/wiki/Constructive_proof

I guess you're talking about the paragraph in this section:

https://en.wikipedia.org/wiki/Petersen_graph#Hamiltonian_pat...

I'm not sure what you mean by "intuition". Do you doubt that this proof has a straightforward translation into formal language?

My point is formal language doesn’t mean “doesn’t require intuition”. By “intuition” I mean the appeal to something you expect the reader to believe without further proof.

I hadn’t seen the Wikipedia article you point out but Peterson graphs will be in many graph theory textbooks.

Again have a look at the article on constructionist proof for another angle on maths and intuition.

> Peterson graphs

The plural here is confusing. Are you talking about the Petersen graph, on ten vertices? There does exist a constructivist proof of its non-Hamiltonicity: merely enumerate every cycle of length ten and show that none are Hamiltonian.

There is a class of objects called generalised Petersen graphs but these are usually Hamiltonian: https://core.ac.uk/download/pdf/82084439.pdf

I think the point is that it usually isn't given formally. In practice it's just too tedious to formally specify proofs using some kind of rigorous set-theoretic language. It's like building a web app with a Turing machine.

> I think the point is that it usually isn't given formally.

Is the claim that the opposite of "formal" is "intuitive"? That's news to me!

I think your statement sounds controversial but I’d be willing to argue that. I.e the opposite of formal is indeed intuitive.

I’d start like this : if you’re explaining something in English then you’re invoking and reliant on the readers common sense and intuition to do the work in your explanation. E.g a pipe is used to smoke tobacco. Pipe. Usage. Smoking. Tobacco. It’s left to the reader to define, disambiguate and on that basis accept. Contrast to: a pipe is used for transporting water.

Q: If I have a rectangle "a" wide and "b" high, how do I find the width "c" of another rectangle which has the same area but is "d" high?

A: I'll be pedantic and take it in baby steps:

  Given: area = height * width
  Given: area(c, d) = area(a, b)

  c * d = a * b               Because equivalencies of
                              equivalents are equivalent

  (c * d) * x = (a * b) * x   Equivalencies multiplied
                              by the same thing are
                              equivalent

Q: Wait, where did "x" come from?

A: Just bear with me...

  x = 1 / d                   Because I say so
  (c * d) * (1 / d) = (a * b) * (1 / d)   Substitution again
  ...                         Blah blah blah
  c = (a * b) / d             Tadah!

Q: What if "d" is zero?

A: (Chuckle) Division by zero isn't defined.

Q: Why not?

A: Well, we want division to be defined as the inverse of multiplication.

Q: Inverse?

A: If x * y = z, and we know x and z, what is y? x * y = z => z / x = y.

Q: So why can't we divide by zero?

A: Because if x is zero then y could be anything. It's not so much that division by zero is evil as it is that multiplying by zero does not have a unique inverse, and disallowing multiplication by zero would be just too weird.

Q: Why don't we just say that y has a whole slew of possible values?

A: Because we don't. Look, this is simple arithmetic, not some weird group thing. You wanted one equivalent rectangle and I gave it to you. If d is zero there's no c that could be big enough to equal a * b. (Before you ask, "infinity" is not a number.) Well, I suppose you could pick a number if...

Q: ... a or b is zero. I have no idea if a or b or d will be zero. Can I still use "c = a * b / d?"

A: Don't you have to wash the car or something?

[edit: consistent use of "c" and "d"]

That's not intuition, though. That's relying on previously established abstractions and set-theoretic frameworks.

That's part of it. The core difficulties here are the definition of "inverse" and knowing when it's applicable to use the transformations. The former is difficult to pin down in a totally formal yet useful form. The latter will in practice depend upon intuition; no one is going to back-compute invariants ("d = ab/c" is always legitimate in the larger context of "given b = ac*d ...")

> Q: What if "d" is zero?

You can avoid chuckling by pointing out that this is a nonsense question. A rectangle which has a height of zero isn't a rectangle at all - it's a line. And lines don't have areas.

(You can continue chuckling after someone asks why lines have no area, I guess.)

I'm not aware of a formal definition of rectangle which excludes zero height. Sounds like an intuitive leap :)

The premiere dialectic in this area is Lakatos' "Proof and Refutations", which I highly recommend in general, and has plenty to say about the present topic.

> Q: Wait, where did "x" come from?

A proof from intuition is not the same as a formal proof with an insightful step. I wager that many formal proofs (in Coq, say) would spur such "Wait, what is that for?" questions.

In this case, the selection of some arbitrary non-zero real "x" is a creative step, not an intuitive one. The missing proviso that "x" is non-zero is an oversight, but it's a "small error", and -- with some experiential intuition -- can be recovered.

(EDIT: The arbitrary variable is quickly overridden with a specific definition, but this is not typical unless there's a good reason to conceptualize it this way. If its value is obvious, define it up front and discuss why that value is the correct one.)

> What if "d" is zero?

This is (very nearly) a refutation, in the sense of Lakatos. We reflect and decide that our basic proof idea works for rectangles of positive area, and in some sense zero-area rectangles aren't really the objects we wanted to talk about. So we include this as an assumption.

The digression about division by zero, inverses, etc. is valuable, but missing the point that this is an algebraic representation of a geometric problem. There's a lot that could be said about whether geometry is intuitive or formal, but I think the issue of divisibility by zero is side-stepping most of the interesting stuff.

...anyway, this is quite a convoluted proof. We assume a priori that for any rectangle R, its "area" A(R) is well-defined and computable. We'll assume that the rectangles are axis-aligned with side-lengths R.x and R.y for each axis. We could have a separate discussion and proof about the invariance of area under a change of basis.

Theorem: Given a rectangle R with non-zero side-lengths R.x and R.y, and given a non-zero real number c, there exists a rectangle R2 with non-zero side-lengths where R2.x = c and A(R) = A(R2).

Proof: Because R2.x is already specified, we need only determine R2.y. We know that, for rectangles, A(R) = R.x * R.y. So we desire that R.x * R.y = R2.x * R2.y. Because R2.x = c and c is non-zero, we have the equivalent desire that (R.x * R.y) / c = R2.y. Thus, the rectangle where R2.x = c and R2.y = (R.x * R.y) / c will have the same area as R and will have the desired side-length c. []

English? Yes. But it has more similarity with legalese than informal English. Each clause makes direct appeal to some rule of logic, and it could be transformed into a Coq proof (or any other proof assistant) without much ceremony.

> ...anyway, this is quite a convoluted proof.

Agreed :)

> Theorem: Given a rectangle R with non-zero side-lengths...

And this is the key problem with the "proof" I laid out. My theorem does not specify non-zero dimensions. Therefore standard arithmetic division by a dimension is not well-defined. Since we're pondering intuition, it's interesting to consider how fixing the "proof" was approached. On the one hand, you fixed it by in effect back-progating invariants to the problem definition. Another approach would be to use a modified definition of "division" ("d = 0 if a or b are zero"--would still require the constraint "c !=0 unless a*b=0").

Mathematically, the former appoach is almost always what you're going to want, since a modified definition will be pretty useless to build upon consistently. From an application standpoint, the latter would be much more robust.

This is kind of one of the points made in the Sci Am article--pure vs. applied proofs are different.

Yes, this is a fair point! Interestingly though, projective geometry already provides us with a space potentially suited to this question — I find https://en.m.wikipedia.org/wiki/Projectively_extended_real_l... to be a good introduction, although I’m not terribly familiar with the field myself.

The intuition behind this choice is, if we’re squishing the rectangle so hard that one side approaches 0 length, the constant area has to go somewhere. If the other side length approaches infinity, why not literally let its measure be infinity? One would argue that the real numbers are too impoverished to give a satisfactorily general answer to our original question.

Of course, we still obtain a zero area, so we’re no longer really solving the same problem as we started with. If we want a zero side length and a non-zero area, we may need to move into non-Euclidean geometries. It really depends on what we’re doing.

My point is that when an application needs to make changes to the foundation, usually there’s going to be a richer pure setting we can move to. And if there isn’t yet, that’s a great opportunity to find out how robust of a new foundation we can create.

Hiding edge cases away in an otherwise unobtrusive definition bothers me as both a mathematician and as a software developer. In all cases, I want to highlight the assumptions we’re making and find the right abstraction to tame them.

Intuition may not be the right word but there's a massive gap between proofs mathematicians find acceptable and proofs generated by automated proof systems like coq.

Mathematicians need to be convinced that in principle a proposition could be stripped down to axioms and syllogisms. It turns out that it's quite hard to do that stripping-down in practice.

Reply on news.ycombinator.com