Zestryon 🐈⬛Pendant des millénaires, les théorèmes mathématiques ont été validés par une poignée d'experts. De nouveaux outils permettent désormais à des machines de vérifier formellement les démonstrations, transformant en profondeur la discipline.
L'article original est bien moins évasif https://www.newscientist.com/article/2518526-mathematics-is-undergoing-the-biggest-change-in-its-history/
Anne O'neam@Zestryon Je sais pas, franchement je pense que l'article de Slate est fondamentalement plus à propos de Lean (un concurrent de Coq que je ne connaissais pas) et donc les outils de preuves formelles. Des trucs pas nouveaux (première release de Coq il y a 36 ans quand même). Les preuves non relisibles par de humains ça fait 20 ans que ça existe...
@anneoneam Si j'ai bien compris, la nouveauté réside dans l'utilisation à la fois de l'IA pour proposer et de ces outils de preuve pour valider.
@Zestryon Je trouve que la vraie nouveauté c'est les vérificateurs de preuve du coup, l'IA va juste aider le vérificateur de preuve à savoir quoi tenter mais c'est plus du détail ça...