je serais curieux de savoir si cette discussion a dissipé nos différences de point de vue, ou si tu continues à ne pas être convaincu par l'idée que les assistants de preuve pourraient un jour apporter du confort à la pratique de la recherche en mathématiques.
Honnêtement je ne sais pas. Voevodsky pensait que la complexité de la recherche en géométrie algébrique était devenue telle qu'il fallait absolument changer le paradigme et utiliser ces assistants de preuve pour être certains de ne pas faire d'erreur dans les démonstrations. D'après ce que j'ai lu ses collègues ne semblent pas convaincus et ils continuent de faire leur recherche et de publier leurs démonstrations de façon classique.
Peut-être qu'il faudra attendre que ces assistants deviennent plus puissants, plus simples à utiliser et qu'ils s'appuient sur des bibliothèques bien plus complètes de résultats déjà démontrés.
Ou peut-être qu'il y aura une séparation du travail et qu'on va assister à l'émergence d'une nouvelle classe de mathématiciens. Ces nouveaux chercheurs prendront les résultats démontrés classiquement et feront le travail de vérification formelle. Un peu ce qu'à fait Gonthier avec la vérification du théorème de Feit-Thompson.
Mais ça lui a pris 6 ans, il était entouré d'une équipe de chercheurs et c'était pour prouver un théorème vieux de plus de 50 ans.
Autrement dit c'est pas gagné...
[^] # Re: Math
Posté par patrick_g (site web personnel) . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 4.
Honnêtement je ne sais pas. Voevodsky pensait que la complexité de la recherche en géométrie algébrique était devenue telle qu'il fallait absolument changer le paradigme et utiliser ces assistants de preuve pour être certains de ne pas faire d'erreur dans les démonstrations. D'après ce que j'ai lu ses collègues ne semblent pas convaincus et ils continuent de faire leur recherche et de publier leurs démonstrations de façon classique.
Peut-être qu'il faudra attendre que ces assistants deviennent plus puissants, plus simples à utiliser et qu'ils s'appuient sur des bibliothèques bien plus complètes de résultats déjà démontrés.
Ou peut-être qu'il y aura une séparation du travail et qu'on va assister à l'émergence d'une nouvelle classe de mathématiciens. Ces nouveaux chercheurs prendront les résultats démontrés classiquement et feront le travail de vérification formelle. Un peu ce qu'à fait Gonthier avec la vérification du théorème de Feit-Thompson.
Mais ça lui a pris 6 ans, il était entouré d'une équipe de chercheurs et c'était pour prouver un théorème vieux de plus de 50 ans.
Autrement dit c'est pas gagné...