I feel that we don’t praise Lean enough. AFAIU it’s what enables LLMs to brute force those problems

YeGoblynQueenne 3 hours ago | parent | next [-]

The brute-forcing is a good, old-fashioned generate-and-test approach like in Simon and Newell's Logic Theorist, which was presented in the Dartmouth convention in 1956, where AI was named by John McCarthy. Logic Theorist caused a big stir by (re) proving several of the theorems in Principia Mathematica by Russel and Whitehead.

There was much excitement, then, as now, for this kind of approach and there were several systems that followed along the same lines, e.g. Automated Mathematician by Doug Lenat.

Eventually it became clear that this approach is limited by what it can generate: you may have a sound and complete verifier, but if the generator, i.e. the first step in the generate-and-test pipeline, is incomplete, then the entire thing will run out of steam sooner or later.

The difference with LLMs is that they are... well, large. They are the most powerful generators ever created. That means their limits are not in sight and it will probably take us a very long time to find them.

Which is all to say that, yes of course, automatic verification is indispensable. But without an LLM generating an unprecedentedly large number of plausible theorems, there would be no AI mathematics, or in any case AI mathematics wouldn't have gone as far as it has.

▲

iamgopal 4 hours ago | parent | prev | next [-]

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

▲

dgellow 4 hours ago | parent | next [-]

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

▲

pixl97 4 hours ago | parent [-]

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.

	▲	dgellow 4 hours ago \| parent [-]
		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

▲

gwerbin 4 hours ago | parent | prev | next [-]

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.

▲

4 hours ago | parent | prev [-]

[deleted]

▲

ForHackernews an hour ago | parent | prev [-]

How long until we find out that some AI has quietly buried an exploit in Lean to cheat at proofs?