2026.11.03 11:10:34 (Mastodon 117552200697262338, Twitter 2117575168101093702) from Daniel J. Bernstein:
John Harrison used Claude to auto-formalize OpenAI's Navier-Stokes results in HOL Light (simpler TCB than Lean): https://github.com/hol-light-family/Navier_Stokes I've posted a trace of the HOL Light proofs, and a script that rechecks the proofs in 30 seconds on a typical CPU core: https://cr.yp.to/2026/20261102-quick-check-navierstokes-trace