What is “intuition” but any set of heuristic approaches to generating conjectures, proofs, etc., and judging their correctness, which isn’t a naive search algorithm through formulas/proofs in some formal logical language? At a low level, all mathematics, including even the judgment of whether a given proof is correct (or “rigorous”), is done by intuition (at least, when it is done by humans). I think in everyday usage we reserve “intuition” for relatively high level heuristics, guesses, hunches, and so on, which we can’t easily break down in terms of simpler thought processes, and this is the sort of “intuition” that Terence Tao is discussing in those quotes. But we should recognize that even regarding the very basics of what it means to accept a proof is correct, we are using the same kinds of thought processes, scaled down.
Few mathematicians want to bother with actual formal logical proofs, whether producing them or reading them.
(And there’s an even subtler issue, that logicians don’t have any one really convincing formal foundation to offer, and Godel’s theorem makes it hard to know which ones are even consistent—if ZFC turned out to be inconsistent, would that mean that most of our math is wrong? Probably not, but since people often cite ZFC as being the formal logical basis for their work, what grounds do we we have for this prediction?)
What is “intuition” but any set of heuristic approaches to generating conjectures, proofs, etc., and judging their correctness, which isn’t a naive search algorithm through formulas/proofs in some formal logical language? At a low level, all mathematics, including even the judgment of whether a given proof is correct (or “rigorous”), is done by intuition (at least, when it is done by humans). I think in everyday usage we reserve “intuition” for relatively high level heuristics, guesses, hunches, and so on, which we can’t easily break down in terms of simpler thought processes, and this is the sort of “intuition” that Terence Tao is discussing in those quotes. But we should recognize that even regarding the very basics of what it means to accept a proof is correct, we are using the same kinds of thought processes, scaled down.
Few mathematicians want to bother with actual formal logical proofs, whether producing them or reading them.
(And there’s an even subtler issue, that logicians don’t have any one really convincing formal foundation to offer, and Godel’s theorem makes it hard to know which ones are even consistent—if ZFC turned out to be inconsistent, would that mean that most of our math is wrong? Probably not, but since people often cite ZFC as being the formal logical basis for their work, what grounds do we we have for this prediction?)