3 ms·
> Gowers makes a point to contrast their GOFAI approach with ML - they're interested in insights, not black-boxes But I have the impression Gowers dismisses th
by funcDropShadow 4y ago
> Gowers makes a point to contrast their GOFAI approach with ML - they're interested in insights, not black-boxes
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.
- yaseer 4y agoI 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.