Artificial intelligence is enjoying a renaissance based on a combination of increasing computational power and enhanced theoretical insights.
While much of the focus is on machine learning and the automation of human labour, artificial intelligence has also fundamentally been affecting how mathematical theorems are proven.
In particular, computer-assisted proofs are flourishing, often successfully addressing long-standing open problems. The use of computers as mathematical proof tools has raise many questions, though.
What constitutes an elegant mathematical proof? Is mathematics becoming an experimental science? How to establish the validity of proofs too large or too complicated to be understood by humans?
In this talk, drawing on my research in automated reasoning I present different scenarios involving computer-assisted proofs, discuss the associated challenges, and present a recently developed approach how to ensure validity of large-scale proofs.