131–140 of 291 posts
Earlier quoted context omitted.
The Lean proof is published, you can download it. The clock definitely is ticking. Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.
Publish in academic language means accepted peer-reviewed paper.
Earlier quoted context omitted.
Wouldn't the proof be attributed to the people who operated the AI? After all, it took more than writing a "prove the navier Stokes Clay problem" prompt.
> After all, it took more than writing a "prove the navier Stokes Clay problem" prompt. Yes, but it took far less than using your meat brain to prove the Navier-Stokes Clay problem.
I assume that the mathematicians outside Anthropic were hoping to publish an actual human-understandable paper. That could be one way to draw line: you can use AI, but you must also have an intelligible explanation at the end.
Earlier quoted context omitted.
If the Lean initial-problem-setup/statements/assumptions/etc. aren't correct then the proof is meaningless. Lean does not know what it is that it is proving i.e. it does not have any semantic understanding but only executes formal logic. Humans need to verify everything.
Also, and sorry if it's been discussed to death (pointers welcome), but, what is the probability that the proof holds in lean becaude of... A bug in lean ?
Finally, you can export your proofs from Lean and have them re-verified by other independently developed theorem provers/proof checkers.
To get an idea of what is involved in a Theorem Prover see;
Introduction to Automated Theorem Provers - https://pqnelson.github.io/2020/03/27/automated-theorem-prov...
Towards a simple theorem prover - https://medium.com/@maiavictor/towards-a-simple-theorem-prov...
In my opinion, I think the Clay Mathematics Institute deserves some criticism for all the drama surrounding these problems. Mathematicians know that you can make problems arbitrarily complex, and declaring problems with large prizes attached to them can lead to a lot of competition and drama. I feel that mathematics should be free from competitions and the pursuit of glory. However, after reading the open letter sign…
It's not a large prize though. OpenAI spent many multiples of the prize money in just a few days to get there and even if one solves a problem in the traditional way, that person is most likely already an accomplished professor at a reputable university where a million dollars doesn't mean as much as the eternal fame that comes with it.
It is a large prize if you're just an academic.
Earlier quoted context omitted.
I really like this style of writing for some reason. Not sure how to put it but it’s a rare combination of a vague post and confidence
It's optimistic and grounded in knowledge seeking. I like it too. It's easy to get caught in the details of today. Our skepticism, our distrust, our loathing. For people, for companies. This is a nice pull in the other direction, a silver lining. In the grand scheme of things, we're solving these frontier problems: Somebody did it and that's amazing. That's what it was all about when this started of in 2000.
Earlier quoted context omitted.
"In recent years there has been an increasing sense of anticipation as breakthroughs in the surrounding field (some recognised by the Clay Research Award) have raised hopes that the Navier-Stokes problem might soon be resolved. The increasing ability of new technologies to accelerate mathematical research has heightened this sense of anticipation." Keyword: New Technologies
That is so vague you might as well call Windows NT new technologies
Earlier quoted context omitted.
> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs. It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.
LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.
Earlier quoted context omitted.
Can you elaborate on what constitutes a vacuous proof?
I present to you my new theorem as follows: If 1 == 3 then 3 == 3 ---- This statement is 100% logically coherent internally. But it also doesn't matter because we know that 1 does not equal 3 so this proof is completely pointless. I could also say 3 == 5 and it would still be logically sound but completely useless information.
Are you proving for some arbitrary definition of == that isn't what we commonly consider the definition? How is it logically coherent? You mean only in the sense that you say it is and you haven't provided any rules to disprove it?
Earlier quoted context omitted.
OpenAI has stated that they will not claim the prize. https://openai.com/index/navier-stokes-solution/ While the scandal is still unraveling, it seems that OpenAI did a rush job to steal other mathematicians' thunder and finish the proof first. OpenAI released a statement that their work does not relate to the work of the other team, but it clearly does. They use the same niche smooth-forcing mechanism. Altman and Bu…
1) OpenAI and Buckmaster did not solve the same problem. Per https://x.com/IlinVasily29521/status/2097554700321329393 , here is a breakdown of who solved what. Tristan + Levent: 3D incompressible Euler with forcing OpenAI: 3D incompressible Euler without forcing OpenAI: Navier-Stokes with forcing No one: Navier-Stokes without forcing Euler equations = Navier-Stokes without viscosity. Forcing means external force. Abs…