Oui je suis assez d'accord avec vous, la puissance de AlphaGeometry reside surtout à mon sens dans une généralisation de la méthode "Deductive Database" avec un pivot de Gauss pour automatiser certains calculs. Pas clair que le LLM ne puisse pas être remplacé par une heuristique.

Quand il y a des problèmes d'orientation (inégalités), alors il faut la CAD et la complexité théorique et en pratique ne permet pas de résoudre des problèmes avec beaucoup de points.

Oui les méthodes algébrique (Wu ou Gröbner) ou semi-algébrique (Méthode de aires) sont très efficaces pour les problèmes qui sont dans leur scope. Mais ces méthodes ne génèrent pas de preuve lisibles.

Et si tu veux t'en servir avec tes étudiants y a des interfaces comme Lean Verbose, Coq Waterproof et Yalep: gricad-gitlab.univ-grenoble-alpes.fr/yalep/Yalep

Je serais curieux de croiser les déclarations d'impôts avec les salaires moyens à la sortie annoncés par certaines formations.

C'est quand même bizarre que je ne puisse pas lire ce que mon ministre pense car c'est publié dans un journal auquel je n'ai pas accés.

L'IA rend les formations à la va-vite encore moins pertinentes, le marché va avoir besoin surtout de gens hypers qualifiés, les formations courtes pour maitriser une techno sans recul ni capactié d'analyse seront de plus en plus inutiles.

Même quand tu enseignes ?

Pour le logiciel on a www.softwareheritage.org/save-referen...