Mastodon Feed
Boosted by cstanhope@social.coop ("Your weary 'net denizen"):
FabMusacchio ("Fabrizio Musacchio") wrote:
RE: https://mastodon.social/@h4ckernews/117400527816149038
NaviesStokes lost in translations: #Lean can verify a formal proof perfectly well, while the #AI may have changed the actual #mathematical argument during translation. The authors find exactly this in #OpenAI’s recent #NavierStokes work: Different bounds, different proof strategies, but still valid Lean code.