AI systems can now reach extraordinary scores on difficult mathematics benchmarks, but a correct answer is only one part of mathematical progress. The deeper challenge is preserving explanation, attribution, verification, and the human process that turns a result into reusable knowledge.
OpenAI says an AI-generated, Lean-checked construction establishes finite-time blowup for a forced three-dimensional Navier–Stokes flow. This explainer breaks down the equation, the precise Clay alternatives, the limits of the claim, and why data provenance matters.
Proofcraft’s August 2026 milestone adds a machine-checked confidentiality proof to seL4’s AArch64 functional-correctness and integrity story. Here’s what the result proves, why processor state makes the work challenging, and where the assumptions still matter.