6 ms·

I don't think this is a valid counterpoint at all. Math is cooperative, and comprehension is the point: the proof has value exactly because (and only to that ex

by zahlman 2mo ago

I don't think this is a valid counterpoint at all. Math is cooperative, and comprehension is the point: the proof has value exactly because (and only to that extent) it empowers humans to understand an abstract truth. Chess is competitive: the memorized line has value because it makes you incrementally more likely to defeat your opponent.

thechao 2mo ago
I hope I'm remembering this right: a mathematician claims to have a proof for the ABC conjecture, but can't conceive any other mathematician it's right — it's "too weird", so the proof is rejected?
- drdeca 2mo ago
  Not quite? It is more that 1) someone has gone through it, identified a step he thinks isn’t a valid step, and the author hasn’t been willing to work with that person 2) most consider the proof, due to its length combined with those doubts as to its validity, not worth their time and effort to work through and understand (because it would take a lot of time, and they have jobs to do, doing research and teaching, etc.)
- sanxiyn 2mo ago
  The consensus is that proof is in fact incorrect. People tried really hard (like putting in a year of effort) and most converged to the same place, that proof of 3.12 is incorrect or has a gap. Peter Scholze (who won Fields Medal) and Jakob Stix did a writeup. People seem to think Shinichi Mochizuki correctly reduced ABC conjecture to 3.12, but didn't prove 3.12, and also are doubtful about the whole program because 3.12 doesn't seem any easier than ABC conjecture while complicating everything. https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
- GPerson 2mo ago
  Some of the best mathematicians in the world tried to study his work, found flaws he did not address, and somehow there’s someone every week suggesting there’s a conspiracy against this guy. It’s really baffling. AI will probably help him move on by lean verifying his proof is wrong…
  - Paracompact 2mo ago
    By this point, he is very much nutso enough that a Lean certified counterexample to his theories would not dissuade him. His response would be either that the formalization is incorrect (with no coherent insights on how to fix it), or worse, Lean itself is a tool of Western imperialism and incapable of properly explicating his ideas. He has, in the past, ranted against such things as monotheism and English grammar as being the reason for his theories' lack of popularity. IIRC he has expressed support in the past for attempts to formalize IUT in Lean, but we'll see where that really goes, because he's absolutely not clearheaded enough to lead such a project himself.
    - zmgsabst 2mo ago
      Project LANA ran into the same roadblock as Scholze and Stix, when they attempted to formalize the proof in Lean.
- ziiinq 2mo ago
  [dead]
nilkn 2mo ago
Math that humans don't understand but nonetheless allows AI systems to develop breakthroughs in various fields of science, technology, physics, engineering, medicine, etc., would have great value to humanity even if it doesn't help humans understand abstract truth at all. Imagine if humans couldn't understand multivariable calculus, but we had access to an AI system that developed it, it initially seemed useless, then another AI system found a predictive model of electromagnetism using it.
- deleted 2mo ago
  [deleted]
- Jensson 2mo ago
  But at that point you have full AGI and its not just today's models. Today's models still need humans to understand things since it builds upon human knowledge. When you have full AGI of course you no longer need humans to understand math. > Imagine if humans couldn't understand multivariable calculus, but we had access to an AI system that developed it Developing multivariable calculus requires much more than just solving problems though, it requires defining an entirely new system and space. That is not the situation mathematicians face today, modern AI cannot do that. When talking about mathematicians and AI don't use fictive examples, we can look at what AI can do today and extrapolate that they can do more of that tomorrow, that is what we have to work with. In the case you posit where AGI exists there is no reason to even discuss what is left for humans to do, since AGI is defined as when humans are no longer needed for anything, the AGI can do every bit of thinking humans can.
  - spacebanana7 2mo ago
    It's reasonable to say that current or near future AI can find novel mathematical results and develop applications from those. The idea of AI stepping from a graph theory/combinatorics innovation to some new and useful algorithm isn't crazy.
    - a2ff6eeb0 2mo ago
      Exactly. Soon, human brains are going to be obsolete.
glimshe 2mo ago
Math isn't "cooperative". Math is about truths. The length of circumference. The area of a triangle. The formulas for these are true in an objective sense irrespective of whether you understand them. That said, without understanding, Math can't evolve. Comprehension of a proof is very important, but not what Math is fundamentally about. Computer programs are Math. You can use them without understanding how they work.
- gsinclair 2mo ago
  First of all, mathematics is about so much more than the area of a triangle etc. that any analogy based on such simple things is overwhelmingly likely to be too simple to be of value. Secondly, there is no truly objective truth to the area of a triangle. At bottom, this “truth” is simply “everyone is convinced, and for good reason”. Without persuading other people of the “truths” that you discover, there is no real mathematics.
  - d4v3 2mo ago
    > Without persuading other people of the “truths” that you discover, there is no real mathematics. Why? If I sat around and studied math by myself and discovered something true yet not yet known but didn't share it, it's still true. Are you saying I didn't "do math" because I didn't share the result? Math exists on another plane and it has 'truths' that we haven't discovered, yet are still 'true', no?
    - chongli 2mo ago
      No, they're saying that what is true in mathematics is contingent, not absolute. It all depends on which set of axioms use, what assumptions you make. The area of a triangle doesn't have 1 unique formula, it has many, depending on the system you use. A triangle in plane geometry has a different area than a triangle in spherical geometry, and different again in hyperbolic geometry. When you get to studying the geometry of manifolds, you realize the area of a triangle can be any damn thing you want, depending on how you construct the manifold you embed it in.
noosphr 2mo ago
Math is also useful. If someone showed that p = np tomorrow in a formally verified proof I don't care if no one can understand it.
- chongli 2mo ago
  A proof by contradiction that p = np is of no use to anyone, given that it wouldn't help you find any polynomial time algorithms for np-hard problems.
  - ziiinq 2mo ago
    I don’t recall anything specific off the top of my head but I am confident that such a proof would have immediate actionable implications. Furthermore, careful analysis of the latter would as likely as not yield further understanding and, actually /would/ help finding such algorithms. Finally, it has been observed time and time again that often (again, nothing comes up and i don’t want to ask AI) the certainty that something is possible and has been done is motivation and inspiration enough for people to independently solve a problem. Sometimes it is even enough for someone new to simply not know that something is “hard” to solve. It even “motivates” llms, it seems (eg https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...) Of course this is all pure speculation concerning a hypothetical proof that most likely doesn’t exist, or indeed might be so complicated as to not be approachable even after hundreds of lifetimes of study. Nevertheless your conclusion does not follow from the premise
  - Jensson 2mo ago
    A proof that they are the same is of no use either, since it too wouldn't help you find algorithms that are faster. You would need an algorithm that finds solutions, not just a proof they exist. So the value here would almost entirely come from how you proved p = np, since that proof will probably be the first step towards finding the polynomial solutions. But if humans don't understand it good luck finding any.
  - zmgsabst 2mo ago
    Abstract polynomial algorithms are of no use either, eg, translation may require galactic constants or high powers that are still intractable. We only compute with two kinds of things: - small data; or, - extremely lower power and coefficient algorithms We lack the power to, eg, use a quintic algorithm in anything but nearly trivial cases.
thatjoeoverthr 2mo ago
Yes, this. Comprehension is the point. We could map this to something like physics. If a man on a horse can shoot another man with a bow, empirically he makes correct predictions on gravity, wind and relative motion. But he can’t explain it. It’s not any different if your model has some “embodied” or demonstrable understanding; the model is not part of the discourse.
- deleted 2mo ago
  [deleted]
- zmgsabst 2mo ago
  I’m not convinced. In history, we made much more use of hitting things with bows than abstractly comprehending arrow flight.
leonidasrup 2mo ago
The goals of Chess and Math may be different, but they follow the same principle of exploration large search space according to fixed rules. In case of Chess these are chess rules, in case of Math these rules of mathematical logic. Memorized proof patterns have value because they lead you to a final proof.

by zahlman 2mo ago

thechao 2mo ago

I hope I'm remembering this right: a mathematician claims to have a proof for the ABC conjecture, but can't conceive any other mathematician it's right — it's "too weird", so the proof is rejected?

drdeca 2mo ago
Not quite? It is more that 1) someone has gone through it, identified a step he thinks isn’t a valid step, and the author hasn’t been willing to work with that person 2) most consider the proof, due to its length combined with those doubts as to its validity, not worth their time and effort to work through and understand (because it would take a lot of time, and they have jobs to do, doing research and teaching, etc.)
sanxiyn 2mo ago
The consensus is that proof is in fact incorrect. People tried really hard (like putting in a year of effort) and most converged to the same place, that proof of 3.12 is incorrect or has a gap. Peter Scholze (who won Fields Medal) and Jakob Stix did a writeup. People seem to think Shinichi Mochizuki correctly reduced ABC conjecture to 3.12, but didn't prove 3.12, and also are doubtful about the whole program because 3.12 doesn't seem any easier than ABC conjecture while complicating everything. https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture.pdf https://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
GPerson 2mo ago
Some of the best mathematicians in the world tried to study his work, found flaws he did not address, and somehow there’s someone every week suggesting there’s a conspiracy against this guy. It’s really baffling. AI will probably help him move on by lean verifying his proof is wrong…
- Paracompact 2mo ago
  By this point, he is very much nutso enough that a Lean certified counterexample to his theories would not dissuade him. His response would be either that the formalization is incorrect (with no coherent insights on how to fix it), or worse, Lean itself is a tool of Western imperialism and incapable of properly explicating his ideas. He has, in the past, ranted against such things as monotheism and English grammar as being the reason for his theories' lack of popularity. IIRC he has expressed support in the past for attempts to formalize IUT in Lean, but we'll see where that really goes, because he's absolutely not clearheaded enough to lead such a project himself.
  - zmgsabst 2mo ago
    Project LANA ran into the same roadblock as Scholze and Stix, when they attempted to formalize the proof in Lean.
ziiinq 2mo ago
[dead]

nilkn 2mo ago

Math that humans don't understand but nonetheless allows AI systems to develop breakthroughs in various fields of science, technology, physics, engineering, medicine, etc., would have great value to humanity even if it doesn't help humans understand abstract truth at all. Imagine if humans couldn't understand multivariable calculus, but we had access to an AI system that developed it, it initially seemed useless, then another AI system found a predictive model of electromagnetism using it.

deleted 2mo ago
[deleted]
Jensson 2mo ago
But at that point you have full AGI and its not just today's models. Today's models still need humans to understand things since it builds upon human knowledge. When you have full AGI of course you no longer need humans to understand math. > Imagine if humans couldn't understand multivariable calculus, but we had access to an AI system that developed it Developing multivariable calculus requires much more than just solving problems though, it requires defining an entirely new system and space. That is not the situation mathematicians face today, modern AI cannot do that. When talking about mathematicians and AI don't use fictive examples, we can look at what AI can do today and extrapolate that they can do more of that tomorrow, that is what we have to work with. In the case you posit where AGI exists there is no reason to even discuss what is left for humans to do, since AGI is defined as when humans are no longer needed for anything, the AGI can do every bit of thinking humans can.
- spacebanana7 2mo ago
  It's reasonable to say that current or near future AI can find novel mathematical results and develop applications from those. The idea of AI stepping from a graph theory/combinatorics innovation to some new and useful algorithm isn't crazy.
  - a2ff6eeb0 2mo ago
    Exactly. Soon, human brains are going to be obsolete.

glimshe 2mo ago

Math isn't "cooperative". Math is about truths. The length of circumference. The area of a triangle. The formulas for these are true in an objective sense irrespective of whether you understand them. That said, without understanding, Math can't evolve. Comprehension of a proof is very important, but not what Math is fundamentally about. Computer programs are Math. You can use them without understanding how they work.

gsinclair 2mo ago
First of all, mathematics is about so much more than the area of a triangle etc. that any analogy based on such simple things is overwhelmingly likely to be too simple to be of value. Secondly, there is no truly objective truth to the area of a triangle. At bottom, this “truth” is simply “everyone is convinced, and for good reason”. Without persuading other people of the “truths” that you discover, there is no real mathematics.
- d4v3 2mo ago
  > Without persuading other people of the “truths” that you discover, there is no real mathematics. Why? If I sat around and studied math by myself and discovered something true yet not yet known but didn't share it, it's still true. Are you saying I didn't "do math" because I didn't share the result? Math exists on another plane and it has 'truths' that we haven't discovered, yet are still 'true', no?
  - chongli 2mo ago
    No, they're saying that what is true in mathematics is contingent, not absolute. It all depends on which set of axioms use, what assumptions you make. The area of a triangle doesn't have 1 unique formula, it has many, depending on the system you use. A triangle in plane geometry has a different area than a triangle in spherical geometry, and different again in hyperbolic geometry. When you get to studying the geometry of manifolds, you realize the area of a triangle can be any damn thing you want, depending on how you construct the manifold you embed it in.

noosphr 2mo ago

Math is also useful. If someone showed that p = np tomorrow in a formally verified proof I don't care if no one can understand it.

chongli 2mo ago
A proof by contradiction that p = np is of no use to anyone, given that it wouldn't help you find any polynomial time algorithms for np-hard problems.
- ziiinq 2mo ago
  I don’t recall anything specific off the top of my head but I am confident that such a proof would have immediate actionable implications. Furthermore, careful analysis of the latter would as likely as not yield further understanding and, actually /would/ help finding such algorithms. Finally, it has been observed time and time again that often (again, nothing comes up and i don’t want to ask AI) the certainty that something is possible and has been done is motivation and inspiration enough for people to independently solve a problem. Sometimes it is even enough for someone new to simply not know that something is “hard” to solve. It even “motivates” llms, it seems (eg https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...) Of course this is all pure speculation concerning a hypothetical proof that most likely doesn’t exist, or indeed might be so complicated as to not be approachable even after hundreds of lifetimes of study. Nevertheless your conclusion does not follow from the premise
- Jensson 2mo ago
  A proof that they are the same is of no use either, since it too wouldn't help you find algorithms that are faster. You would need an algorithm that finds solutions, not just a proof they exist. So the value here would almost entirely come from how you proved p = np, since that proof will probably be the first step towards finding the polynomial solutions. But if humans don't understand it good luck finding any.
- zmgsabst 2mo ago
  Abstract polynomial algorithms are of no use either, eg, translation may require galactic constants or high powers that are still intractable. We only compute with two kinds of things: - small data; or, - extremely lower power and coefficient algorithms We lack the power to, eg, use a quintic algorithm in anything but nearly trivial cases.

thatjoeoverthr 2mo ago

Yes, this. Comprehension is the point. We could map this to something like physics. If a man on a horse can shoot another man with a bow, empirically he makes correct predictions on gravity, wind and relative motion. But he can’t explain it. It’s not any different if your model has some “embodied” or demonstrable understanding; the model is not part of the discourse.

deleted 2mo ago
[deleted]
zmgsabst 2mo ago
I’m not convinced. In history, we made much more use of hitting things with bows than abstractly comprehending arrow flight.

leonidasrup 2mo ago

The goals of Chess and Math may be different, but they follow the same principle of exploration large search space according to fixed rules. In case of Chess these are chess rules, in case of Math these rules of mathematical logic. Memorized proof patterns have value because they lead you to a final proof.