You're correct that nobody really understands what these huge Lean proofs actually say. However, the initial statement, even for Navier-Stokes, is not very long [0]. Still, you are also right that sometimes the problem statement can be wrong but it is highly unlikely here.
They said that a customer would have paid around 15 million for the required compute. I can't imagine that this was not a significant internal spending even with "free" tokens.
At Astra API prices that's 300B tokens (I saw 130B output tokens claimed elsewhere), large but not unheard of if you consider it across a few people doing random experiments with best-of-n type things. On my personal account, I've done a billion+ token days just on a normal pro 20x subscription. I know many others that wildly outpaced that by orders of magnitude. This was apparently 130B over 89 hours, so about 30x that rate. When things are free and you're expected to token max 30x seems fairly reasonable to me.
If you consider this as a cost to be compared against the question: "What does it take to be able to prove that you have a model that can solve the hardest problems that humans know about?", then spending a some amount of thousands/millions to know the boundaries of that seems not too important in comparison.
You've also got to consider this as compute that's allocated to pushing the frontier of what models can do, so while it's using GPUs that have been paid for etc., it's not like it's a cost that's supposed to be use less of this so that others can have capacity. If you made researchers afraid to use capacity like this, a lot of the things that improve would tend to do so significantly slower. (some may say that's a good thing ;)
A good way to think about this is when tokens are free, you get to choose whether you're optimizing for latency or intelligence rather than having to consider price.
If mathematicians aren't solving problems people are having (which your comment seems to imply), then putting them out of their job with AI is not a bad thing. Of course mathematicians are solving problems, just in a very different way than other professions.
Steam engines actually replaced what a horse does with a machine that could do the same job. So far LLMs aren't doing this - they're producing Lean proofs but very little to actually aid in understanding (again so far pretty much all of these proofs have been extremely difficult optimizations of known techniques). Mathematicians do solve a problem that people have: they build theories that explain the world and give us mental models to navigate questions in science, technology, etc., this just isn't a problem that LLMs solve.
So the issue isn't so much that LLMs will replace mathematicians, but that AI companies bragging constantly about how their machines "solve math" will convince people who don't understand the value of math research to no longer fund it, or students who don't yet understand why learning math is useful for developing their brains that it's a waste of time. That could put mathematicians out of a job without providing a useful replacement.
Motto: a mathematician's job isn't to solve the Hodge conjecture, it's to understand why the Hodge conjecture is or isn't true, and turn that understanding into something that makes it easier for the next person to grasp/use/enjoy.
LLMs absolutely have the potential to make this job easier, but the way in which these companies are using them right now risks being antithetical to that goal.
I mean, yes. But "it doesn't hold that <anything>" is equivalent to "it holds that <not anything>" and since not anything is also anything... Ah, I see.
You can also think of conditional convergence as convergence under the condition of a specific order. It then turns out that unconditional convergence (that is, convergence where it doesn't matter what order you choose) is equivalent to absolute convergence (that is, the sum over the absolute values converges).
If you know the authors of your specific area of research, arXiv is a nice way to read their new papers when they are (mostly) done but the submission to a journal is not finished yet.
This. In my experience, you have to replace peer review with reputation for preprints. That's highly imperfect, and it tends to lead to dismissing of good but work by less well-known researchers as "not peer reviewed", while well-known researchers (or researchers at well-known institutions) basically get a fast track to citations.
Despite the imperfections, I found arXiv indispensable for my research. In particular, mathematics has a slow peer review cycle (it's hard to read and understand, and many referees require that they fully understand a paper to accept it, which imo is a little flawed, but that's the culture). I had several papers that were under review for more than a year (single journal, only one round of revisions), and arXiv was my only showcase. Both works ended up very highly cited, but publication delays would have been an even bigger problem if arXiv wasn't there.
I'm in math, so I can't give you an answer on tech journals unfortunately. And for math, I don't really read any specific journal. It's so much work to read and get something out of a research paper in math that I pretty much only read papers that are directly related to my work or have been recommended to me.
This reminded me of the fact that one colleague of mine even updates the arXiv version if any errors are spotted and says himself that this makes the arXiv version better than the journal version.
Now I tested that too, it doesn't work that way for me, even if there's text highlighted (both regular text or a hyperlink) the menu remains contextualised.
[0] https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
reply