Recent and related. Others? OpenAI’s Navier-Stokes release included a Lean 4 formal proof - https://news.ycombinator.com/item?id=49650326 https://news.ycombina

Recent and related. Others? OpenAI’s Navier-Stokes release included a Lean 4 formal proof - https://news.ycombinator.com/item?id=49650326 https://news.ycombinator.com/item?id=49650326 - Sept 2026 (179 comments) More questions about whether researchers can trust OpenAI with unpublished math - https://news.ycombinator.com/item?id=49639408 https://news.ycombinator.com/item?id=49639408 - Sept 2026 (813 comments) The Navier–Stokes Millennium Prize Problem - https://news.ycombinator.com/item?id=49621697 https://news.ycombinator.com/item?id=49621697 - Sept 2026 (237 comments) Tao: Open math problems being non-renewably mined by AI - https://news.ycombinator.com/item?id=49616968 https://news.ycombinator.com/item?id=49616968 - Sept 2026 (420 comments) On the Navier–Stokes Millennium Prize Problem - https://news.ycombinator.com/item?id=49613262 https://news.ycombinator.com/item?id=49613262 - Sept 2026 (1134 comments) Navier-Stokes – Tristan Buckmaster [pdf] - https://news.ycombinator.com/item?id=49605915 https://news.ycombinator.com/item?id=49605915 - Sept 2026 (827 comments)