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

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