Je n'ai pas lu l'article mais si l'IA produit une démonstration en langage LEAN
Attention une autre partie du problème consiste a s'assurer que l'exposé de base en LEAN correspond bien à l’énoncé; je me souviens de m'être planté dans un exercice de pivot de gausse où je m'était planté en recopiant l’énoncé (j'avais mis un - à la place du +); et là on est dans un cas simple.
modéliser ton problème de math en LEAN est loin d'être simple et un cas particulier peut subtilement changer la donne.
Il ne faut pas décorner les boeufs avant d'avoir semé le vent
[^] # Re: Un peu, beaucoup risqué
Posté par fearan . En réponse au lien ia openai affirme avoir resolu le probleme de navier-stoke ... ou pas. Évalué à 6 (+3/-0).
Attention une autre partie du problème consiste a s'assurer que l'exposé de base en LEAN correspond bien à l’énoncé; je me souviens de m'être planté dans un exercice de pivot de gausse où je m'était planté en recopiant l’énoncé (j'avais mis un - à la place du +); et là on est dans un cas simple.
modéliser ton problème de math en LEAN est loin d'être simple et un cas particulier peut subtilement changer la donne.
Il ne faut pas décorner les boeufs avant d'avoir semé le vent