Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AlphaProof's Greatest Hits

rishimehta.xyz

Post reply on HN
Print view View original

51–60 of 140 posts

Re: AlphaProof's Greatest Hits

#51

Post by raincole »

throwaway713 wrote: post #39

Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?

If "better than humans" means when you give it a real world problem, it gives you a mathematical model to describe it (and does it better than human experts), then yes, it's the end game.

If it just solves a few formalized problems with formalized theorems, not so much. You can write a program that solves ALL the problems under formalized theorems already. It just runs very slowly.

Re: AlphaProof's Greatest Hits

#52

Post by exe34 »

margorczynski wrote: post #47
throwaway713 wrote: post #39

Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?

I doubt it. Math has the property that you have a way to 100% verify that what you're doing is correct with little cost (as it is done with Lean). Most problems don't have anything close to that.

to be fair, humans also have to run experiments to discover whether their models fit nature - AI will do it too.

Re: AlphaProof's Greatest Hits

#53

Post by auggierose »

andrepd wrote: post #46
auggierose wrote: post #17

Earlier quoted context omitted.

Certainly an interesting information that AlphaProof needed three days. But does it matter for evaluating the importance of this result? No.

More or less. Modern theorem provers, even fully automatic ones, can prove incredibly difficult problems if given enough time. With 3 days and terabytes of memory, perhaps they could? Would be interesting to compare Alphaproof with a standard theorem prover that is given similarly astronomical computing resources.

That is an interesting thought. But I doubt that standard automated theorem proving techniques would have solved this in a 100 years, even with immense resources, as all they do is (basically) brute force search, and it remains an exponential search space. Therefore 3 days does not really matter, indeed, 3 months would still be a result that 10 years ago I would have thought impossible.

Re: AlphaProof's Greatest Hits

#54

Post by margorczynski »

exe34 wrote: post #52
margorczynski wrote: post #47

Earlier quoted context omitted.

I doubt it. Math has the property that you have a way to 100% verify that what you're doing is correct with little cost (as it is done with Lean). Most problems don't have anything close to that.

to be fair, humans also have to run experiments to discover whether their models fit nature - AI will do it too.

These kind of experiments are many times orders of magnitude more costly (time, energy, money, safety, etc.) than verifying a mathematical proof with something like Lean. That's why many think math will be one of the first to crack with AI as there is a relatively cheap and fast feedback loop available.

Re: AlphaProof's Greatest Hits

#55

Post by nickpsecurity »

raincole wrote: post #48
sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

It's obviously not the future (outside of mathematics research). The whole LLM boom we've seen in the past two years comes from one single fact: peopel don't need to learn a new language to use it.

Natural language -> Formal Language with LLM-assisted tactics/functions -> traditional tools (eg provers/planners) -> expert-readable outputs -> layperson-readable results.

I can imagine many uses for flows where LLM’s can implement the outer layers above.

Re: AlphaProof's Greatest Hits

#57

Post by Groxx »

sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

The difficulty then will be figuring out if the proof is relevant to what you want, or simply a proof of 1=1 in disguise.

Re: AlphaProof's Greatest Hits

#58

Post by letitgo12345 »

nybsjytm wrote: post #15
Robotenomics wrote: post #13

“Only 5/509 participants solved P6”

This has to come with an asterisk, which is that participants had approximately 90 minutes to work on each problem while AlphaProof computed for three days for each of the ones it solved. Looking at this problem specifically, I think that many participants could have solved P6 without the time limit. (I think you should be very skeptical of anyone who hypes AlphaProof without mentioning this - which is not to suggest…

Think more is made of this asterix than necessary. Quite possible adding 10x more GPUs would have allowed it to solve it in the time limit.

Re: AlphaProof's Greatest Hits

#59

Post by est »

sega_sai wrote: post #40

I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.

> formalized languages is really the future

Hmm, maybe it's time for symbolism to shine?

Re: AlphaProof's Greatest Hits

#60

Post by titanomachy »

raincole wrote: post #51
throwaway713 wrote: post #39

Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?

If "better than humans" means when you give it a real world problem, it gives you a mathematical model to describe it (and does it better than human experts), then yes, it's the end game. If it just solves a few formalized problems with formalized theorems, not so much. You can write a program that solves ALL the problems under formalized theorems already. It just runs very slowly.

I don’t think you can gloss over the importance of computational tractability here. A human could also start enumerating every possible statement in ZFC, but clearly that doesn’t make them a mathematician.
Post reply on HN