Proof engineering, from the Four Color to the Odd Order Theorem by Dr Georges Gonthier
Thirty five years ago computers made a dramatic debut in mathematics with the famous proof of the Four Color Theorem by Appel and Haken. Their role has been expanding recently, from computational devices to tools that can tackle deduction and proofs too complex for (most) human minds, such as the Kepler conjecture or the Classification … Proof engineering, from the Four Color to the Odd Order Theorem by Dr Georges Gonthier