Create software that will take a traditional mathematical proof expressed in natural language and output a formal proof.
On one hand, this seems so difficult as to probably constitute a holy grail of computing. Compare the length and human effort of formal proofs versus the original proof.
On the other hand, we can be optimistic. Mathematics is inherently a logically precise subject. The computer program can ask for help when it becomes confused about natural language or other understanding. Finally, the output formal proof does not need to be complete; instead, the program can output lemmas that still need to be proven.
One small step might be to encourage publishing mathematics papers in a more machine-readable form, avoiding two-dimensional layout that mathematics often uses for notation. Perhaps publish the raw LaTEX.
Previously on the formalization of mathematics.
Inspired by the difficulty of acceptance of the purported proof of the abc conjecture.
No comments :
Post a Comment