For more than half a century, computers have become essential research tools in many areas of fundamental mathematics. They have dramatically expanded the scope of experimentation and visualization, thereby becoming valuable assistants in the formulation of conjectures. They also play an increasing role in the discovery and verification of proofs. This phenomenon largely predates the rise of AI, although recent advances in artificial intelligence considerably amplify its impact. This talk will discuss the role of computer tools in contemporary mathematics, with a particular focus on the potential impact of the rise of interactive theorem proving.

Automath est un projet collectif pour faire communauté en région parisienne autour de l’informatisation des mathématiques