A separate paper challenges the correspondence between OpenAI’s written Navier-Stokes proof and its formal verification in Lean, software that checks mathematical logic. Valerio Capraro, describing the paper’s findings, identified two mismatches: one written estimate requires four additional input derivatives, while its Lean counterpart requires five; a pressure-flux estimate uses a different bound and argument. Capraro wrote, “It is not clear whether these mismatches invalidate the entire proof.”
Researchers have also reported further improvements to OpenAI’s theoretical integer multiplication result. A contributor publishing as 0xdoug validated and merged Rohan’s contribution, reporting an exponent saving parameter of κ = 2⁻¹⁵, up from OpenAI’s original 2⁻¹⁸². The reported 2¹⁶⁷-fold increase concerns that parameter, not practical multiplication speed, and the submitted bound remains conditional on OpenAI’s algorithmic interfaces. The latest result combined techniques from several contributors.