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
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.
when you are large enough to allocate sufficient resource, you should go native, if not, go flutter/react native etc. Its very simple decisions I guess.
I had to create special checker/linter to analyze my code base ( and asked AI to loop it through it as some kind of test ), so as to avoid AI (mis)using tailwind class here and there. that was 2025, AI and linter both improved quite a lot since.
Running 10000 agents to solve hundred year old problems definitely shows capabilities of AI beyond doubt, but why leave the war when it is at its fiercest.
future is on the way, three to four generation ( one each year ?) will unfold this, primarily quantum computer improving material and battery, humanoids becomes standardised and modular enough to be easily replaceable ( think ibm pc ) ( most components are simple injection moulded advance plastics , mass produced in some corner of china, self detection of wear and tear and self replace that part ), other is optical computers ( 100x lower power x 100x speed = local inference ), problem is, when this will become reality, who will benefits more ? who will hold moat ?
reply