Comment by auggierose | Hacker News Reader

Comment by auggierose | Hacker News Reader

Parent Full thread

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.

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.

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

Reply on news.ycombinator.com