Peut-on comprendre cette preuve ? Un aperçu de la mathématique formalisée
Stephen Wolfram explore une énigme mathématique de longue date : la preuve d’un axiome étonnamment simple pour l’algèbre booléenne. Générée à l’aide d’une démonstration automatique de théorèmes, la preuve est incroyablement complexe et reste incompréhensible pour les humains. L’article explore les complexités de la preuve, dissèque ses opérations au niveau du « code machine » et propose un défi : humaniser cette preuve. Il discute du potentiel des grands modèles de langage (LLM) pour comprendre et simplifier la preuve, ainsi que des implications pour l’avenir des mathématiques. La conclusion suggère que certaines preuves mathématiques peuvent être intrinsèquement ininterprétables, ce qui indique que les mathématiques ressembleront de plus en plus à une science expérimentale.