Hugging Face 联创 Thomas Wolf 在 OpenAI 宣布用一组智能体给出 Navier-Stokes 问题解之后表示,这不足以说明 AI 已经解决数学。他指出这次是通过证明猜想为假(反例)而非完整证明取胜,近期 AI 数学的前沿成果也多是反例或大海捞针。他认为模型仍缺少数学家依赖的数学品味,难以区分优美论证与仅仅正确的论证,并希望这类工具的访问能被尽可能广泛共享。
Hugging Face 联创从数学品味角度提出,AI 在数学上的前沿成果多是反例式搜索,尚不足以判定领域已被解决。
friends are regularly surprised when i say i don’t think math is (yet) “solved,” so in the wake of the ns result i figured i’d explain this take a bit more widely.
first, this is massively impressive and clearly an example of AI being, in some respects, far more powerful than the human mind. the team deserves huge praise for attempting and succeeding at this. i’d love to read a technical report on the project (one can always hope :)
but second, here again we ended up with a counterexample rather than a full proof: option C won the NS problem by proving the conjecture false (which was one valid way to solve the problem for sure)
notice a pattern in many of the recent frontier results in ai for math? a striking number involve counterexamples or finding a needle in a haystack.
now don’t get me wrong: this is extraordinarily hard and commendable. but it is only one aspect of mathematicians’ work.
Math is also about:
- finding deep, general mathematical understanding and explanations within proofs
- revisiting proven results to find more « elegant » proofs
- proposing new conjectures and hypotheses that might open « fruitful » directions
- taking the leap of faith of proposing entirely new, « exciting » research programs that may take decades to bear fruit
you may say these are simply further increments on the same intelligence scale, and perhaps point 2 above is already within the reach of current models. possibly
but you could also see this string of results as an extraordinarily powerful, massively parallel extension of search: explore the haystack, find the needle i.e. the counterexample that breaks the conjecture.
that would already be remarkable. but it would still leave open whether models understand the words I emphasized above: « elegant », « fruitful », « exciting ».
as tristan put it in his brief report: “the first llm generated proof levent sent me was the most horrendous i have ever read.”
despite their formidable technical abilities, models still seem to lack something mathematicians rely on constantly: a type of mathematical taste. the ability to distinguish a beautiful argument from a merely valid one, a fertile idea from a sterile one.
i’d be very curious to ask gpt or claude what they think of the result they just proved. do they find it elegant? if they ignore all the human noise about it on the web and history of math, do they appreciate the result and the path to it more than other proofs?
my suspicion is that, outside of the human knowledge that this is an important millennium prize problem, it may not 100% register it as fundamentally different from thousands of other proofs.
or, more intriguingly, perhaps the beauty they find in mathematics is actually alien to our own sense of mathematical beauty, some « horrendous » proof to us might be deeply satisfying to them…
all this to say that we might have significant progress to make in ai for math before declaring the field “solved,” (as too many are posting).
in the meantime, ai will be an extraordinary collaborator for mathematicians. i just hope access to these tools be as widely shared as possible (so that you don’t need a Leven or Sebastien working in a big lab to help you), and that companies stop using mathematics primarily as a demonstration of prowess in their private race.
We’re sharing a solution to the Navier-Stokes Millennium Prize Problem, one of the deepest problems at the frontier of mathematics. The proof was produced by a group of agents, using an OpenAI next-generation model significantly more capable than GPT-6 Astra. The problem concerns whether the description of smooth three-dimensional fluid motion modeled by the Navier-Stokes equations can break down. It has remained unresolved for roughly 90 years.在 X 查看被引用的帖子
来源:@Thom_Wolf · x.com