Les ordinateurs en mathématiques : une nouvelle mathématique

Les mathématiciens sont des gens méfiants. Peut-être pas dans la vie de tous les jours, mais dans son travail. “On ne travaille pas avec des gens qu’on ne connaît pas”, explique Leonardo de Moura. “Cette personne est-elle vraiment sérieuse ? Est-ce qu’elle sait ce qu’elle fait ?” Dans la structure mentale du mathématiques Les phrases et les théorèmes s’appuient les uns sur les autres comme les pierres individuelles d’un édifice : si l’une de ces pierres est défectueuse, la cathédrale entière peut s’effondrer. La confiance personnelle est centrale.

Ce serait différent s’il existait un processus automatisé qui vérifie l’exactitude du travail mathématique – ce qui est le cas aujourd’hui. Cela s’appelle Lean, et de Moura, d’origine brésilienne, actuellement employé comme informaticien dans le département de recherche d’Amazon, le co-développe depuis 2013. Une grande partie des connaissances mathématiques a déjà été traduite dans une sorte de langage informatique pour le Lean. Si un mathématicien propose maintenant une nouvelle preuve mathématique et la formule en Lean, le système peut la reproduire étape par étape puis la qualifier de « vraie » ou de « pas vraie ». Tout le monde peut faire confiance au résultat une fois qu’il a été vérifié avec succès.