Mathématiques assistées par ordinateur: le futur de la recherche?

«Grâce aux progrès en informatique, les ordinateurs peuvent à présent nous aider, nous, chercheurs en mathématiques théoriques, non plus seulement à effectuer des calculs mais bel et bien à raisonner.» Kevin Buzzard ne mâche pas ses mots. En juillet 2022, lors du Congrès international des mathématiciens – le prestigieux événement au cours duquel sont décernées les médailles Fields –, ce chercheur britannique a donné une conférence remarquée, intitulée «La montée du formalisme en mathématiques», promouvant avec enthousiasme l’utilisation des «assistants à la preuve».