Given a long formal proof of a theorem, find a shorter proof in an automated or semi-automated fashion. On one hand, this seems an easier task than the original proof because you can terminate any automated search when the length exceeds the original, and maybe you can use the original proof as a scaffold to search for shortcuts.
On the other hand, a shorter proof could require even more "creativity" and "imagination" than the original proof.
Inspired by Feit-Thompson theorem. Is there a short proof of Fermat's Last Theorem?
No comments :
Post a Comment