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