The one thing that we should look at given recent advance in maths using lean is, computer science will ( and should be ) used to create appropriate language for other fields ( biology, process, chemistry, games, movies etc ). ( hammer / nail analogy ). Science <-> Engineering used to be about representing anything in math so as to define and solve it, now onwards it will be about representing it in a language.
Weird thing to say to a comment that explicitly says this is about warming the oceans. The original calculation, assuming all the energy is dumped directly into the ocean would be: 87B / (60*60*24*365*4) = 689.69 years.
Funny thing about the atmosphere though is that it requires ~1300x less energy to heat up by 1 degree, so if you dump all that energy into the atmosphere, the temperature would go up by ~2 degrees per year.
The reality is that global warming warms up both the oceans and the atmosphere to varying degrees (and the earth's crust, to much lesser degree), with the ocean absorbing most of that. The atmosphere only absorbs about 23% of that, and a significant amount of the of the excesses radiate back into space.
But even with a conservative estimate that only 1% of this heat is being stored in the atmosphere, that would still lead to a global atmospheric temperature increase of 1 degree Celsius every 50 years. The worst-case scenarios estimate 2% of this heat is retained, dropping that down to 25 years.
I'm going to go ahead and guess that waiting 2.5M years isn't the answer. That's geological time scales anyway, Humans could have gone extinct and been replaced with new intelligent life in that kind of time. Whatever math you did to reach that figure, it's completely wrong.
Either would have worked, but rust's fussy compiler & memory features is an advantage for LLMs. The more bug catching you can shift out of runtime and into compile time the better since the LLM can fix it
go is even more straightforward for llms imo. It's a dead simple language with a good garbage collector, where you can still do a lot memory management
That’s kinda my point - you don’t really want to trust the LLM to get any sort of memory management right. A system where hard constraints are baked into the language itself and the LLM fights the compiler at compile time removes a lot of hoping the LLM got it right.
Ultimately either works though so use whatever you enjoy
I wouldn't say it has lost. Big firms like Microsoft and Amazon are just afraid to use Go since it's by Google, a known evil firm. This doesn't hold back smaller firms that need to move fast.
You play White, and Jev plays Black. Rather than asking an LLM to generate move strings or JSON, the backend feeds all server-validated legal candidate moves into Vercel AI SDK's experimental_evaluate(). Jev picks Black's move and outputs its probability distribution across all legal candidates in a single forward pass (~300ms, ~$0.00004/move).
Once we start dividing, filtering, or moderating content, HN will just become Reddit. The current level of moderation is good enough, if not the best. It works because the community naturally filters itself—like-minded people find a home here, while those outside the bubble quickly get bored and move on.
I cannot say, math research isn’t my domain of expertise, I’m just trying to follow along :)
But I find it interesting that Lean, a validator/compiler made by humans, is what enables those discoveries. But somehow all the praise goes to the models
Yes! Thank you, this has been irritating me from day one with agentic AI, I don't think it could be nearly as good as it is without all the well-designed tools humans have spent decades developing from PLs, to VCS, to the Unix philosophy, to CLIs / REPLs.
I think that AI is very skilled and adept at using them, but without them it would just be flailing around in its own psychosis. The tools ground the AI in reality and allow them to make progress without going in hallucinated directions. I very much doubt AI could have solved this problem without Lean, and for AI to invent something like Lean it would have to use other tools made by humans.
This is also perfect evidence of why Python isn't the end-all-be-all of programming languages just because the AI was trained on vast amounts of Python, and proof that the right language for the job is more viable than ever with the aid of LLMs.
Frankly, the forecasting that programming languages are a dead field has baffled me because it seems like with LLMs, unique programming language semantics are more important than they've ever been.
I mean we don't instantly fall into ASI, hopefully. The problem with humans is every problem we solve the goal posts get kicked further down the road until they are reaching relativistic speeds. It starts around "well, the AI hasn't solved a novel problem" then moves to "well, they didn't write the validator" and suddenly humans are at the point of saying "Well AI hasn't rewrote the constants of the universe, what good are they".
Of course another way to look at this is, the people that wrote the validator got praise for that years ago. Now and up and coming actor is solving problems that took us 100s of years to create in insanely short time periods so of course it's going to get a lot of attention as it well should.
To be clear: I’m aware the LLMs are solving problems. I’m just saying that what enables that whole research revolution is Lean. We wouldn’t be seeing all those results without it. I would like to see it acknowledged when people are talking about LLMs solving maths. The same way I think we should acknowledge the humans who are guiding and prompting the LLMs. I don’t think that necessitates to move a goal post
I don't think so. People have been trying things like this with evolutionary algorithms for a very long time already. LLMs can interleave symbolic manipulation with empirical experiments and simulations and charts and thinking/reasoning text, and an LLM will much more efficiently search the space of candidate ideas than any handcrafted mutation algorithm. Any task with a cheaply verifiable goal that requires fanning out across a massive search space is ideal for contemporary LLM technology to make progress with.
reply