6 ms·

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 st

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 3d 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 3d 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.
  - anonymouz 3d ago
    I recommend rereading the text.
    - auggierose 3d ago
      It is not that nicely written.
      - anonymouz 3d ago
        Maybe, but it's not worth discussing the content if you dont comprehend what the authors are actually saying.
        auggierose 3d ago
        Here is what they are saying: 1. AI really did solve a problem in mathematics. The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. Yes, it is sufficient. To say otherwise is just goalpost shifting because you don't like the answer. There are, in fact, two notions of proof: a logical notion and an intelligible notion. Wrong again, the only real notion of proof is logical. It is not even possible to say exactly what an "intelligible" notion would be, because that would make it logical. I would be very surprised if Tao couldn't extract a proof that he understands within a few months out of the formal proof. I would compare this to understanding a difficult proof in some math journal. In the end, all of this forth and back does not matter. A logical proof is a perfectly fine answer, and given that AI can provide that now, this is the future.
        anonymouz 3d ago
        There is a point in distinguished a formal proof from an intelligible one, notwithstanding the fact that one can, with effort, be extracted from another. That's a key point of the discussion that we mathematicians are having now, and fits into the bigger question as to what it means to gain mathematical understanding. In fact, Tao happens to have some older posts about this himself. The naive formalist reduction that you are making is not really bringing us forward in having a useful reflection about this, as the discussion is already beyond that.
        auggierose 3d ago
        > There is a point in distinguished a formal proof from an intelligible one, Fine, do that if you want. What you cannot do is call a logical and formal proof of a problem not solving the problem in mathematics. That is absurd, and mathematicians that insist on this are absurd, too. Note that Tao didn't say this, but two guests. I understand that you might want more than a formal proof generated by a machine, just like I want fries with my steak. But saying that the steak is not food, is just ridiculous. You are not further along in the discussion, you are having the wrong discussion. What is at stake here is nothing less than the question: Is mathematics subjective or objective? This mathematician thinks it is objective.

anonymouz 3d 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 3d 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.
- anonymouz 3d ago
  I recommend rereading the text.
  - auggierose 3d ago
    It is not that nicely written.
    - anonymouz 3d ago
      Maybe, but it's not worth discussing the content if you dont comprehend what the authors are actually saying.
      - auggierose 3d ago
        Here is what they are saying: 1. AI really did solve a problem in mathematics. The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not sufficient. Yes, it is sufficient. To say otherwise is just goalpost shifting because you don't like the answer. There are, in fact, two notions of proof: a logical notion and an intelligible notion. Wrong again, the only real notion of proof is logical. It is not even possible to say exactly what an "intelligible" notion would be, because that would make it logical. I would be very surprised if Tao couldn't extract a proof that he understands within a few months out of the formal proof. I would compare this to understanding a difficult proof in some math journal. In the end, all of this forth and back does not matter. A logical proof is a perfectly fine answer, and given that AI can provide that now, this is the future.
        anonymouz 3d ago
        There is a point in distinguished a formal proof from an intelligible one, notwithstanding the fact that one can, with effort, be extracted from another. That's a key point of the discussion that we mathematicians are having now, and fits into the bigger question as to what it means to gain mathematical understanding. In fact, Tao happens to have some older posts about this himself. The naive formalist reduction that you are making is not really bringing us forward in having a useful reflection about this, as the discussion is already beyond that.
        auggierose 3d ago
        > There is a point in distinguished a formal proof from an intelligible one, Fine, do that if you want. What you cannot do is call a logical and formal proof of a problem not solving the problem in mathematics. That is absurd, and mathematicians that insist on this are absurd, too. Note that Tao didn't say this, but two guests. I understand that you might want more than a formal proof generated by a machine, just like I want fries with my steak. But saying that the steak is not food, is just ridiculous. You are not further along in the discussion, you are having the wrong discussion. What is at stake here is nothing less than the question: Is mathematics subjective or objective? This mathematician thinks it is objective.