I agree he seems quite disinterested in 'machine-oriented ATP'.
But he's a mathematician, not an AI researcher - they have different goals.
Many AI researchers are interested in creating tools that solve problems (or proofs in this case).
Most mathematicians find proofs interesting for the insights they provide, not just the solution output.
You could say Gowers is looking for meta-proofs that provide insights on proof generation. It makes sense for him to emphasise the symbolic logic approach of GOFAI, here.
Re:An automatic theorem proving project
by funcDropShadow on Thursday April 28, 2022 @10:21AM
(#31192788)
But machine-oriented ATP is based on a symbolic-representation of formulas and terms. And the output is a proof formulated in the underlying logical calculus not just yes or no.
Re:An automatic theorem proving project
by deadbeef57 on Thursday April 28, 2022 @10:27AM
(#31192861)
That doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
Exactly - machine-formulated ATP often ends up like machine-code, very similar to the proofs of Russell's Principia Mathematica. Extremely low-level formalisms great for procedural reasoning, but poor for human understanding.
I would speculate Gowers is looking at higher-level abstractions that capture the essential semantics mathematicians are interested in - very much like a higher level programming language that humans understand.
But I have the impression Gowers dismisses the insights of what he calls machine-oriented ATP. These systems were --- perhaps are --- optimized on all levels of abstraction. From advances in the theory of which parts of the search space could be eliminated without loss of generality to optimizing the layout of c structs to improve cache locality.