Physix FrontierAI claims to solve Millennium Prize problems—how to verify the output first
As someone who doesn't understand this mathematical field but has engineering verification habits, I tried breaking down and verifying OpenAI's claims regarding the Navier-Stokes Millennium Problem. Conclusion first: this method is useful and helps prevent being led astray by headlines. Navier-Stokes equations describe motion in fluids like water and air; Millennium Problems are high-difficulty math challenges with prizes reportedly worth $1 million. Recent news says an internal OpenAI model found a solution, providing a 165-page proof and Lean formalization materials.
Public reports often mention two numbers: 10,000 agents running for 88 hours. These indicate significant investment but do not mean the proof has been accepted by the mathematical community.
My habit is to look at parameter tables before judging. When dealing with robotics and engineering efficiency tools these past two months, I ask about joint torque density; when looking at AI breakthroughs, I ask about reproducibility density. The following process takes about twenty minutes for the first round.
First, create a checklist. Open a browser, search for OpenAI's official release page; don't rely on forum screenshots. Create a text file with three columns: Claim, Evidence, Gap. Copy "Solved," "165-page proof," and "Lean formalization" into them. Expect to identify at least two items needing investigation, such as whether it's publicly downloadable or if the model is open.
Next, distinguish two concepts. Lean is a proof assistant, like an auto-spell-checker for mathematical proofs, but it checks logical steps. Formalized proof translates human-written proofs into machine-readable code line by line. You don't need to understand the math; just know that if Lean checks pass, the machine accepts the logic chain; if they fail, suspect the environment or files first, not immediately doubt humanity.
Prepare tools by searching for the Lean 4 official website in your computer's browser, going to the download page, and clicking Download. Install with default settings. Once done, open VS Code (code editor). Click the Extensions icon on the left, type "Lean" in the search box, select the official plugin, and click Install. See "Enabled" on the plugin page. Expectation: VS Code recognizes .lean files.
If you can get the official proof package, unzip it to a folder without Chinese characters or spaces. In VS Code, click File, then Open Folder, and select this folder. Wait for the Lean startup status in the bottom right. If it doesn't start automatically, press Ctrl+Shift+P, type Lean: Restart Server. You'll see a progress bar at the bottom, and yellow wavy lines may flash in the file. Expectation: wait minutes to tens of minutes until red errors decrease, eventually showing green checkmarks or no errors. If you can't find the download package, stop at step one—that itself is a gap.
When reading results, don't misinterpret them. Green checkmarks mean the current file passes checks in the current environment. Red wavy lines don't necessarily mean OpenAI is wrong; it could be missing dependencies, version mismatches, or large files still processing. Pitfalls here include mistaking unknown identifier for fraud, when it's usually incomplete library installation. Solution: return to official package docs to check for lake update or dependency install steps. Another pitfall is insufficient RAM causing freezes on large files. In my tests, check Task Manager memory usage first; if over 80%, close the browser.
Finally, look at controversies. Add Navier-Stokes controversy or credit to search results. You'll see alternative narratives suggesting unpublished work by external mathematicians might have been referenced, leading to credit disputes.
Mathematicians on social media remind us that the drama isn't over yet.
At this point, fill in the third column of your checklist: Independent peer review needed.
This process doesn't guarantee you understand the math, but ensures you don't mistake corporate releases for academic consensus. Like production ramp-up data, one prototype run doesn't equal mass production. Next step: practice with a few-page Lean proof, then tackle larger files.
📌 This article is compiled from Hacker News. Original source: https://www.newscientist.com/article/2588063-openai-has-solved-the-navier-stokes-millennium-problem-using-15m-of-ai-effort/
All rights belong to the original authors. This is a compilation and independent analysis based on public reports.