6 ms·

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

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.

tome 8y ago
> 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.
- usgroup 8y ago
  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 https://en.m.wikipedia.org/wiki/Constructive_proof
  - tome 8y ago
    I guess you're talking about the paragraph in this section: https://en.wikipedia.org/wiki/Petersen_graph#Hamiltonian_paths_and_cycles 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?
    - mgsouth 8y ago
      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.
      - tome 8y ago
        > 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!
        usgroup 8y ago
        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.
    - usgroup 8y ago
      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.
- mgsouth 8y ago
  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"]
  - n4r9 8y ago
    That's not intuition, though. That's relying on previously established abstractions and set-theoretic frameworks.
    - mgsouth 8y ago
      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 ...")
- soVeryTired 8y ago
  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.
aeorgnoieang 8y ago
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!
- jasperry 8y ago
  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.

tome 8y ago

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

usgroup 8y ago
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 https://en.m.wikipedia.org/wiki/Constructive_proof
- tome 8y ago
  I guess you're talking about the paragraph in this section: https://en.wikipedia.org/wiki/Petersen_graph#Hamiltonian_paths_and_cycles 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?
  - mgsouth 8y ago
    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.
    - tome 8y ago
      > 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!
      - usgroup 8y ago
        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.
  - usgroup 8y ago
    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.
mgsouth 8y ago
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"]
- n4r9 8y ago
  That's not intuition, though. That's relying on previously established abstractions and set-theoretic frameworks.
  - mgsouth 8y ago
    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 ...")
soVeryTired 8y ago
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.

aeorgnoieang 8y ago

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!

jasperry 8y ago
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.