4 ms·
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 researcher
by yaseer 4y ago
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.
- funcDropShadow 4y agoBut 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.
- deadbeef57 4y agoThat doesn't mean it is a proof that human have the slightest chance of understanding. It gets out of hand quickly.
- yaseer 4y agoExactly - 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.