A Lean-verified proof can still prove the wrong version of a problem
A user is exploring the AI/Navier-Stokes story, specifically what was proved. They used Apodex, an OpenAI write-up, and the Clay problem statement to map official requirements to the new result. The goal was to check if initial conditions, forcing, energy bounds, and singularity claims aligned. This led to a question for formal proof practitioners: how do they ensure a theorem encoded in Lean accurately reflects the intended human-proved theorem?
This report uniquely highlights the critical challenge of verifying that a formal proof in Lean accurately reflects the human-intended theorem, unlike typical discussions focusing solely on proof correctness.
时间与来源
时间显示为 UTC
显示时区：UTC
本地时区尚不可用，暂时显示 UTC。
发布当时偏移：UTC+02026年9月19日 03:48 UTC
收录当时偏移：UTC+02026年9月19日 11:00 UTC
- 发布
- 2026年9月19日 03:48
- 收录
- 2026年9月19日 11:00
- 来源类型
- 开发者社区
- 档位
- 社区
- 信源状态
- 正常
档位是按信源手工设定的编辑判断，不是逐条打分。
I've been following the AI/Navier-Stokes story, and I'm still trying to understand exactly what was proved.
OpenAI says its system constructed a smooth three-dimensional fluid that starts at rest, has a smooth external force applied, and develops a singularity in finite time. It also released a formal proof checked in Lean.
Lean checks that a conclusion follows from the encoded definitions and assumptions.
Someone still has to confirm that those definitions accurately represent the original Clay problem.
It's like software passing every test while still failing the requirement because the tests measured the wrong thing.
So I gave Apodex the OpenAI write-up, the Clay problem statement and a few explanations, and asked it to map each official requirement to the corresponding part of the new result. I wanted to see whether the initial conditions, forcing, energy bounds and singularity claims lined up.
There's checking each logical step, checking that the Lean statement matches the analytical paper, and checking that the paper answers the question Clay posed
Mathematicians still need to understand and independently scrutinize the construction.
"Lean checked it, so it's officially solved" goes too far. But "it uses external forcing, so it doesn't count" might also be wrong, because parts of the official formulation allows smooth forcing under specified conditions.
Clay's prize rules requires publication in a qualifying outlet, at least two years after publication, and general acceptance by the mathematical community before consideration.
For people working with formal proofs: how do you check that the theorem encoded in Lean is the theorem humans intended to prove?