Georges Gonthier - Computer Proofs - Teaching Computers Mathematics, and Conversely
Explore a comprehensive lecture on the progress of computer-assisted mathematical proofs, from the four-color puzzle to the Kepler conjecture. Delve into how computer science and software engineering methods have been applied to mathematical language, leading to new insights like synthetic homotopy type theory. Examine various landmarks in computer proofs, including the Odd Order theorem and its implications for finite groups. Investigate the challenges and benefits of formalizing mathematical proofs, the development of proof algorithms, and the implementation of algebraic notation in digital formal texts. Learn about interactive mathematics, algebraic interfaces, and the emergence of Homotopy Type Theory. Gain insights into the future of computer-assisted mathematics and its potential to revolutionize mathematical research and education.