TL;DR: It seems the AI wrote code in Lean that proves there are solutions to Nav... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

cs702 23 days ago | parent | context | favorite | on: Navier–Stokes Lost in Translation

TL;DR:

It seems the AI wrote code in Lean that proves there are solutions to Navier-Stokes that can blow up, but...

the AI's explanation of the code, in natural language, does not correspond to the Lean proof!

That is... so rich in irony.

Consider applying for YC's Winter 2027 batch! Applications are open till November 2.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact