modéliser ton problème de math en LEAN est loin d'être simple et un cas particulier peut subtilement changer la donne.
Je n'ai pas dit qu'on pouvait se passer des mathématiciens (par exemple pour formaliser les problèmes à résoudre), je disais juste qu'on peut, dans le cas particulier des mathématiques, éviter/détecter les hallucinations.
[^] # Re: Un peu, beaucoup risqué
Posté par mahikeulbody . En réponse au lien ia openai affirme avoir resolu le probleme de navier-stoke ... ou pas. Évalué à 2 (+0/-0). Dernière modification le 14 septembre 2026 à 16:40.
Je n'ai pas dit qu'on pouvait se passer des mathématiciens (par exemple pour formaliser les problèmes à résoudre), je disais juste qu'on peut, dans le cas particulier des mathématiques, éviter/détecter les hallucinations.