6 ms·

The opening sentence of a linked article sums it up quite well: "If nobody understands a mathematical proof, does it count?" The abc conjecture may be solved t

The opening sentence of a linked article sums it up quite well: "If nobody understands a mathematical proof, does it count?" The abc conjecture may be solved today but only when a sufficient number of people understand and accept the proof as a proof.

tobhahn 9y ago
According to the article, there are more than 10 people who understand and accept the proof.
pacala 9y ago
Formalize it with Isabelle / Coq / Lean. Then it counts.
- tobhahn 9y ago
  Math is more about figuring out why things are true than what is true. Mathematicians want to understand Mochizuki. They couldn't care less if hn thinks it counts.
  - SomeStupidPoint 9y ago
    I don't know why this got flagged. At the point that we no longer understand the relationship between the formal proof witnesses (and really, the class of possible witnesses) and the axioms we choose, we can no longer do mathematics, because we can no longer meaningfully explore axioms -- our ability to make guided changes is destroyed by our inability to understand their effect. It's important for the community to understand something of why a thing, not just that it's true, because that's why drives the development of mathematics forward. (And indeed, particularly so in the ABC conjecture, which sits at a node between the nature of multiplication and addition, which don't usually have much to do with each other.) I actually wonder if US (and perhaps other) math education is harmful here: the focus on rote learning and just knowing that a thing is true (to mechanistically apply it) has conditioned people to not understand why the hesitance over proofs that humans don't understand -- for most of those people, they never understood the proofs anyway.
    - pacala 9y ago
      That is an excellent point. The future is mechanical proofs. Which will bring tools for proof search, proof refactoring, proof minimization, proof navigation, theorem generation. We'll be able to tackle _much_ harder problems, while still being able to get the gist of it. Sometimes I'm saddened that this future may come slower than we'd like due to imperfect funding structures. But I've grown a lot of patience over the years :)
      - SomeStupidPoint 9y ago
        I'm actually very pro-formalization and mechanical verification -- both for mathematics and computer science. $HOBBYPROJECT involves automated theorem proving, while I'm trying to convince $DAYJOB to adopt some formal methods. I was just pointing out that the person got flagged for commenting that "witness and dump" isn't actually very useful for mathematics as a field, except as a signal that we should investigate a topic further. But in the case of the ABC conjecture, we already have plenty of incentive to investigate. I think mathematics and science have a lot of learn from computer science in terms of managing large models, proofs, etc -- and that we'll get a lot of automatic tools. That will all be really great. But there are proofs that are basically just brute-forcing a solution for which we have no higher-level understanding, and those don't really add much by way of knowledge to mathematics. At the point that those are all we can generate for "big" problems, we may be in trouble.
        pacala 9y ago
        Another excellent point. Right now it's a "winner takes all" competition. It matters to prove a result, and much less to provide an "elegant" proof. I can only hope for a future where we measure the algorithmic entropy of a proof [log proof length][0], and results like "ABC theorem proof using half the bits as best known proof" become notable. [0] https://en.wikipedia.org/wiki/Kolmogorov_complexity https://en.wikipedia.org/wiki/Kolmogorov_complexity
        haskellandchill 9y ago
        I'm interested in your $HOBBYPROJECT. I'm hoping to develop some software similar to edukera.com, ie using proof assistants as educational tools for mathematics. Would love to swap some cool links and references. Thanks!
- sanxiyn 9y ago
  Indeed. We now actually have some math results of interest for which we have only formal proofs and no human proofs. https://arxiv.org/abs/1509.05468 https://arxiv.org/abs/1509.05468 is an example.
- mikebenfield 9y ago
  We are very far from the point where that is feasible for many new results in math.
deleted 9y ago
[deleted]
MikkoFinell 9y ago
>"If nobody understands a mathematical proof, does it count?" Just wait until general AI really kicks off, then all of new math will be like that. It's not that humans are bad at logical thinking, our weakness is memory. That won't be the case for an artificial agent with instantaneous perfect recall of everything it has ever seen.
- LeifCarrotson 9y ago
  Even an AI will have various levels of cache. Some memories will be register-level instant, some will be thousands of miles and quite a few servers away, and others in between.
  - MikkoFinell 9y ago
    That's a good point. Lets throw "instantaneous" out, having the ability to store and perfectly recall data is a critical advantage for any thinking entity.
- BucketSort 9y ago
  lol. I think the resurgence of interest in constructionist mathematics via Homotopy Type Theory will lead to better proofs ( since all proofs in HoTT are like programs and can be computationally verified in a straightforward way ).
- deleted 9y ago
  [deleted]
- KGIII 9y ago
  Mathematics is a language. You don't really need to memorize it, you can read it. Unfortunately, most people aren't exposed to anything higher than arithmetic.
  - posterboy 9y ago
    yeah, well, have fun reading e.g. the stacks project[1] of round about 4000 pages without remember the necessary steps leading up to a corollary. [1] https://stacks.math.columbia.edu/browse https://stacks.math.columbia.edu/browse - abstract algebra as far as I can tell

tobhahn 9y ago

According to the article, there are more than 10 people who understand and accept the proof.

pacala 9y ago

Formalize it with Isabelle / Coq / Lean. Then it counts.

tobhahn 9y ago
Math is more about figuring out why things are true than what is true. Mathematicians want to understand Mochizuki. They couldn't care less if hn thinks it counts.
- SomeStupidPoint 9y ago
  I don't know why this got flagged. At the point that we no longer understand the relationship between the formal proof witnesses (and really, the class of possible witnesses) and the axioms we choose, we can no longer do mathematics, because we can no longer meaningfully explore axioms -- our ability to make guided changes is destroyed by our inability to understand their effect. It's important for the community to understand something of why a thing, not just that it's true, because that's why drives the development of mathematics forward. (And indeed, particularly so in the ABC conjecture, which sits at a node between the nature of multiplication and addition, which don't usually have much to do with each other.) I actually wonder if US (and perhaps other) math education is harmful here: the focus on rote learning and just knowing that a thing is true (to mechanistically apply it) has conditioned people to not understand why the hesitance over proofs that humans don't understand -- for most of those people, they never understood the proofs anyway.
  - pacala 9y ago
    That is an excellent point. The future is mechanical proofs. Which will bring tools for proof search, proof refactoring, proof minimization, proof navigation, theorem generation. We'll be able to tackle _much_ harder problems, while still being able to get the gist of it. Sometimes I'm saddened that this future may come slower than we'd like due to imperfect funding structures. But I've grown a lot of patience over the years :)
    - SomeStupidPoint 9y ago
      I'm actually very pro-formalization and mechanical verification -- both for mathematics and computer science. $HOBBYPROJECT involves automated theorem proving, while I'm trying to convince $DAYJOB to adopt some formal methods. I was just pointing out that the person got flagged for commenting that "witness and dump" isn't actually very useful for mathematics as a field, except as a signal that we should investigate a topic further. But in the case of the ABC conjecture, we already have plenty of incentive to investigate. I think mathematics and science have a lot of learn from computer science in terms of managing large models, proofs, etc -- and that we'll get a lot of automatic tools. That will all be really great. But there are proofs that are basically just brute-forcing a solution for which we have no higher-level understanding, and those don't really add much by way of knowledge to mathematics. At the point that those are all we can generate for "big" problems, we may be in trouble.
      - pacala 9y ago
        Another excellent point. Right now it's a "winner takes all" competition. It matters to prove a result, and much less to provide an "elegant" proof. I can only hope for a future where we measure the algorithmic entropy of a proof [log proof length][0], and results like "ABC theorem proof using half the bits as best known proof" become notable. [0] https://en.wikipedia.org/wiki/Kolmogorov_complexity https://en.wikipedia.org/wiki/Kolmogorov_complexity
      - haskellandchill 9y ago
        I'm interested in your $HOBBYPROJECT. I'm hoping to develop some software similar to edukera.com, ie using proof assistants as educational tools for mathematics. Would love to swap some cool links and references. Thanks!
sanxiyn 9y ago
Indeed. We now actually have some math results of interest for which we have only formal proofs and no human proofs. https://arxiv.org/abs/1509.05468 https://arxiv.org/abs/1509.05468 is an example.
mikebenfield 9y ago
We are very far from the point where that is feasible for many new results in math.

deleted 9y ago

[deleted]

MikkoFinell 9y ago

>"If nobody understands a mathematical proof, does it count?" Just wait until general AI really kicks off, then all of new math will be like that. It's not that humans are bad at logical thinking, our weakness is memory. That won't be the case for an artificial agent with instantaneous perfect recall of everything it has ever seen.

LeifCarrotson 9y ago
Even an AI will have various levels of cache. Some memories will be register-level instant, some will be thousands of miles and quite a few servers away, and others in between.
- MikkoFinell 9y ago
  That's a good point. Lets throw "instantaneous" out, having the ability to store and perfectly recall data is a critical advantage for any thinking entity.
BucketSort 9y ago
lol. I think the resurgence of interest in constructionist mathematics via Homotopy Type Theory will lead to better proofs ( since all proofs in HoTT are like programs and can be computationally verified in a straightforward way ).
deleted 9y ago
[deleted]
KGIII 9y ago
Mathematics is a language. You don't really need to memorize it, you can read it. Unfortunately, most people aren't exposed to anything higher than arithmetic.
- posterboy 9y ago
  yeah, well, have fun reading e.g. the stacks project[1] of round about 4000 pages without remember the necessary steps leading up to a corollary. [1] https://stacks.math.columbia.edu/browse https://stacks.math.columbia.edu/browse - abstract algebra as far as I can tell