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/
"Using machines to solve the types of problem posed in First Proof may produce concrete proofs, says Anna Marie Bohmann at Vanderbilt University in Tennessee, but we lose the “learning opportunity”, she says. “Struggling to create and formulate new ideas and to solve new problems is one of the main ways in which both students and mathematics professionals consolidate their knowledge”."
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...