4 ms·

>The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. What is m

>The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. What is missing is an intelligible proof that human mathematicians can understand and use to advance the aims of mathematics. This makes a bad assumption that humans need to be the one to advance the aims of mathematics. LLMs could be what advances the aims of mathematics and we just have to worry on making it so LLMs can digest these proofs. >Nevertheless, if it turns out that what OpenAI has provided is a mere answer It has a proof attached. Saying that it "doesn't provide understanding" does not invalidate that there is a formal proof. It fundamentally is trying to expand the requirements of proof to be something more than is required.

robotpepi 20d ago
For the moment, AI is not capable of advancing mathematics _in the sense_ you're describing. AI is very bad at designing stuff, asking questions, etc. Maybe in the future you'll be able to ask the AI "cure cancer" and it'll do it, but for now we're very far away from that (this doesn't mean the current achievements aren't impressive).
- charcircuit 20d ago
  This is why we may see the role of people wanting to advance mathematics instead of trying to do proofs themselves to push the frontier instead focus on improving these models to be capable of advancing mathematics.
  - robotpepi 20d ago
    I don't think the essay was proposing that mathematicians should continue to focus on proving everything by themselves forever. It's mostly a critic of how the discussion is focusing too much on that mere "yes/no" answers is the same as makign mathematics advance.
anonymouz 20d ago
The authors discuss the dual roles of proofs, and the new need to differentiate them better, clearly in the article.
- charcircuit 20d ago
  I disagree with the idea that they require serving both roles in order to be considered a proof.
  - anonymouz 20d ago
    You can, mathematicians generally don't. That's what the article is partially about - a purely formal proof doesn't get us much.
    - charcircuit 20d ago
      Because most mathematicians have not migrated to being AI native like most software engineers did. My post is trying to point out that these people's mind is still fixed in how the old world works and is not focused on the future where LLMs are doing a lot of the work.
      - anonymouz 20d ago
        No, because knowing a proof exists is just a small part of math. It's value is rather limited to actual math, as the article explains quite eloquently and nicely.
        auggierose 20d ago
        The article is eloquent and nicely written, and it is also wrong. To say that "1. AI really did solve a problem in mathematics." is wrong, is just wrong. No matter how nice and eloquent you try to explain it afterwards.
        20d ago
QuesnayJr 20d ago
This is exactly backwards. Mathematics predates the idea of formal proof by millenia. The purpose of proofs since Euclid is to explain to your fellow human why something is true. The idea that the purpose of math is formal proof alone is a new idea that (some) computer programmers want to impose on the field (for the understandable reason that it makes computers primary). Formal proof only emerged early in the 20th century, and the standard became that in theory a proof should be formalizable to answer any skepticism, but the real goal in Euclid's time and ours has been to communicate why a theorem is true to your fellow humans. There were a few theorems that are only known via computer proof, like the Four Color Theorem, but this has always been regarded as disappointing or even controversial, and the fact that there hasn't been any conceptual breakthrough has meant that we didn't learn anything other than the sheer fact that the Four Color Theorem is true. Theorems that produce understanding, on the other hand, typically produce many new ideas that lead to more theorems. The purpose of scholarship is understanding. This is just as true for science as it is for math. If AI produces a unified theory of fundamental physics, but it's just an opaque blob, physicists will find it just as unsatisfying.
- pcfwik 20d ago
  I broadly agree with your sentiment and am saddened (outraged?) to see the financially motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing. However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong: > Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...] You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.) What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic. Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.

robotpepi 20d ago

For the moment, AI is not capable of advancing mathematics _in the sense_ you're describing. AI is very bad at designing stuff, asking questions, etc. Maybe in the future you'll be able to ask the AI "cure cancer" and it'll do it, but for now we're very far away from that (this doesn't mean the current achievements aren't impressive).

charcircuit 20d ago
This is why we may see the role of people wanting to advance mathematics instead of trying to do proofs themselves to push the frontier instead focus on improving these models to be capable of advancing mathematics.
- robotpepi 20d ago
  I don't think the essay was proposing that mathematicians should continue to focus on proving everything by themselves forever. It's mostly a critic of how the discussion is focusing too much on that mere "yes/no" answers is the same as makign mathematics advance.

anonymouz 20d ago

The authors discuss the dual roles of proofs, and the new need to differentiate them better, clearly in the article.

charcircuit 20d ago
I disagree with the idea that they require serving both roles in order to be considered a proof.
- anonymouz 20d ago
  You can, mathematicians generally don't. That's what the article is partially about - a purely formal proof doesn't get us much.
  - charcircuit 20d ago
    Because most mathematicians have not migrated to being AI native like most software engineers did. My post is trying to point out that these people's mind is still fixed in how the old world works and is not focused on the future where LLMs are doing a lot of the work.
    - anonymouz 20d ago
      No, because knowing a proof exists is just a small part of math. It's value is rather limited to actual math, as the article explains quite eloquently and nicely.
      - auggierose 20d ago
        The article is eloquent and nicely written, and it is also wrong. To say that "1. AI really did solve a problem in mathematics." is wrong, is just wrong. No matter how nice and eloquent you try to explain it afterwards.
        20d ago

QuesnayJr 20d ago

This is exactly backwards. Mathematics predates the idea of formal proof by millenia. The purpose of proofs since Euclid is to explain to your fellow human why something is true. The idea that the purpose of math is formal proof alone is a new idea that (some) computer programmers want to impose on the field (for the understandable reason that it makes computers primary). Formal proof only emerged early in the 20th century, and the standard became that in theory a proof should be formalizable to answer any skepticism, but the real goal in Euclid's time and ours has been to communicate why a theorem is true to your fellow humans. There were a few theorems that are only known via computer proof, like the Four Color Theorem, but this has always been regarded as disappointing or even controversial, and the fact that there hasn't been any conceptual breakthrough has meant that we didn't learn anything other than the sheer fact that the Four Color Theorem is true. Theorems that produce understanding, on the other hand, typically produce many new ideas that lead to more theorems. The purpose of scholarship is understanding. This is just as true for science as it is for math. If AI produces a unified theory of fundamental physics, but it's just an opaque blob, physicists will find it just as unsatisfying.

pcfwik 20d ago
I broadly agree with your sentiment and am saddened (outraged?) to see the financially motivated cheapening of (destruction of?) what mathematics truly is. I agree that formal logic is merely a model of one aspect of what mathematicians do, in the same sense that a computer simulation of a roller coaster can never bring the same value to us as the real thing. However, I would be remiss if I didn't question your historical claim, which seems to me a bit too strong: > Mathematics predates the idea of formal proof by millenia [...] Formal proof only emerged early in the 20th century [...] You seem to associate the start of "Mathematics" with Euclid, but (as far as I know) he worked at approximately the same time as Aristotle. Aristotle's syllogisms are perhaps the most famous formal logic system: their correctness relates only to their form, not their content. All deductions of the form "All X are Y, All Z are X, hence All Z are Y" are valid (assuming the premises are), regardless of the meanings of X, Y, and Z. (Outside of Greece, my understanding is that a few hundred years earlier Panini had also developed a system of formal manipulations, but for representing grammars.) What, to my understanding, "emerged" only the 19th and 20th century was 'merely' a formal logic both expressive and sound enough to properly express modern mathematics (the Beggriffsschrift in the 19th century and FOL+ZFC in the 20th). Between Euclid and the 19th century the development of calculus was probably the biggest advance in mathematics, and my understanding is that Leibniz himself spent significant time working on formal logic. Perhaps I have the wrong definition in mind of 'formal logic' or 'mathematics,' but I do think the history of formal logic is much more closely tied to the history of mathematics than your post makes it seem on first glance. Though I certainly agree that "mainstream mathematics" has never felt it necessary (or necessarily that useful) to express proofs in a formal logic carefully enough that they could be checked by computers; this was a fringe focus of a minority group of mathematicians and computer scientists that was co-opted as a marketing stunt into 'what mathematics is' for major corporations trying to justify their money burn.