5 ms·

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

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.