Tout ce qu'écrit un LLM devrait être sujet à caution
Je n'ai pas lu l'article mais si l'IA produit une démonstration en langage LEAN (ce qui semble le cas ici), la validité de cette démonstration est vérifiable par un humain. En revanche, j'imagine que saisir l'essence de la démonstration est une autre paire de manche si cette démonstration fait des centaines de pages.
[^] # 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é à 4 (+2/-0).
Je n'ai pas lu l'article mais si l'IA produit une démonstration en langage LEAN (ce qui semble le cas ici), la validité de cette démonstration est vérifiable par un humain. En revanche, j'imagine que saisir l'essence de la démonstration est une autre paire de manche si cette démonstration fait des centaines de pages.