Hacker News Reader

Comment by iamgopal | Hacker News Reader

True, but could humans cross pollinating lean x prolog x A* ( or any search algorithm) could have solved such math problems with super computer ?

View on HN

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

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

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 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 on news.ycombinator.com