3 ms·
It was interesting. One of the reviewers noted that one of the generated proofs didn’t seem that elegant in his opinion. Given enough compute, I wonder how muc
by WhitneyLand 3y ago
It was interesting. One of the reviewers noted that one of the generated proofs didn’t seem that elegant in his opinion.
Given enough compute, I wonder how much this would be improved by having it find as many solutions as possible within the allotted time and proposing the simplest one.
- spookie 3y agoElegance would require more than this. Reasoning, for one.
- jacobolus 3y agoThe issue is that the computer-generated proofs operate at a very low level, step by step, like writing a program in assembly language without the use of coherent structure. The human proof style instead chunks the parts of a solution into human-meaningful "lemmas" (helper theorems) and builds bodies of theory into well-defined and widely used abstractions like complex numbers or derivatives, with a corpus of accepted results. Some human proofs of theorems also have a bit of this flavor of inscrutable lists of highly technical steps, especially the first time something is proven. Over time, the most important theorems are often recast in terms of a more suitable grounding theory, in which they can be proven with a few obvious statements or sometimes a clever trick or two.