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

41–50 of 140 posts

Re: AlphaProof's Greatest Hits

#41

Post by airstrike »

nybsjytm wrote: post #27
dash2 wrote: post #22

Earlier quoted context omitted.

Though, if you start solving problems that humans can't or haven't solved, then questions of capacity won't matter much. A speedup in the movement of the maths frontier would be worth many power stations.

For some time a 'superhuman math AI' could be useful for company advertising and getting the attention of VCs. But eventually it would be pretty clear that innovative math research, with vanishingly few exceptions, isn't very useful for making revenue. (I am a mathematician and this is meant with nothing but respect for math research.)

"Making revenue" is far from being the only metric by which we deem something worthy.

Re: AlphaProof's Greatest Hits

#42

Post by [deleted] »

Onavo wrote: post #23
GregarianChild wrote: post #19

Earlier quoted context omitted.

We know that any theorem that is provable at all (in the chosen foundation of mathematics) can be found by patiently enumerating all possible proofs. So, in order to evaluate AlphaProof's achievements, we'd need to know how much of a shortcut AlphaProof achieved. A good proxy for that would be the total energy usage for training and running AlphaProof. A moderate proxy for that would be the number of GPUs / TPUs that…

> We know that any theorem that is provable at all (in the chosen foundation of mathematics) can be found by patiently enumerating all possible proofs. Which computer science theorem is this from?

[deleted]

Re: AlphaProof's Greatest Hits

#43

Post by nemonemo »

ccppurcell wrote: post #37
wslh wrote: post #11

Earlier quoted context omitted.

Thank you for the response. I have a follow-up question: Could these AIs contribute to advancements in resolving the P vs NP problem? I recall that the solution to Fermat’s Last Theorem relied on significant progress in elliptic curves. Could we now say that these AI systems might play a similar role in advancing our understanding of P vs NP?

Just my guess as a mathematician. But if LLMs are good for anything it will be for finding surprising connections and applying our existing tools in ways beyond human search. There's a huge space of tools and problems, and human intuition and brute force searching can only go so far. I can imagine that LLMs might start to find combinatorial proofs of topological theorems, maybe even novel theorems. Or vice versa. But…

Do you have a past example where this already-proven theorem/new tools/objects would have been only possible by human but not AI? Any such example would make your arguments much more approachable by non-mathematicians.

Re: AlphaProof's Greatest Hits

#44

Post by Xcelerate »

E_Bfx wrote: post #36
Onavo wrote: post #23

Earlier quoted context omitted.

> We know that any theorem that is provable at all (in the chosen foundation of mathematics) can be found by patiently enumerating all possible proofs. Which computer science theorem is this from?

I guess it is tautological from the definition of "provable". A theorem is provable by definition if there is a finite well-formulated formula that has the theorem as consequence ( https://en.wikipedia.org/wiki/Theorem paragraph theorem in logic)

Not sure it’s a tautology. It’s not obvious that a recursively enumerable procedure exists for arbitrary formal systems that will eventually reach all theorems derivable via the axioms and transformation rules. For example, if you perform depth-first traversal, you will not reach all theorems.

Hilbert’s program was a (failed) attempt to determine, loosely speaking, whether there was a process or procedure that could discover all mathematical truths. Any theorem depends on the formal system you start with, but the deeper implicit question is: where do the axioms come from and can we discover all of them (answer: “unknown” and “no”)?

Re: AlphaProof's Greatest Hits

#45

Post by whatshisface »

nybsjytm wrote: post #35
whatshisface wrote: post #34

Earlier quoted context omitted.

Logic is pretty much absent from our culture and daily life, but that could be due to its limited supply.

Being logical in social life is pretty much completely different from being logical in a mathematical argument, especially in a formal theorem proving environment. (Just try to write any kind of cultural proposition in a formal language!)

That's the way things are now, but this regime came about when proving things took intense concentration and specialized skills that very few people had. Contrast going to look something up in a library with googling something during a conversation.

Re: AlphaProof's Greatest Hits

#46

Post by andrepd »

auggierose wrote: post #17
nybsjytm wrote: post #15

Earlier quoted context omitted.

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…

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.

Re: AlphaProof's Greatest Hits

#47

Post by margorczynski »

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.

Re: AlphaProof's Greatest Hits

#48

Post by raincole »

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.

Re: AlphaProof's Greatest Hits

#49

Post by nybsjytm »

airstrike wrote: post #41
nybsjytm wrote: post #27

Earlier quoted context omitted.

For some time a 'superhuman math AI' could be useful for company advertising and getting the attention of VCs. But eventually it would be pretty clear that innovative math research, with vanishingly few exceptions, isn't very useful for making revenue. (I am a mathematician and this is meant with nothing but respect for math research.)

"Making revenue" is far from being the only metric by which we deem something worthy.

As a mathematician, of course I agree. But in a sentence like:

> A speedup in the movement of the maths frontier would be worth many power stations

who is it 'worth' it to? And to what end? I can say with some confidence that many (likely most, albeit certainly not all) mathematicians do not want data centers and power stations to guzzle energy and do their math for them. It's largely a vision imposed from without by Silicon Valley and Google research teams. What do they want it for and why is it (at least for now) "worth" it to them?

Personally, I don't believe for a second that they want it for the good of the mathematical community. Of course, a few of their individual researchers might have their own personal and altruistic motivations; however I don't think this is so relevant.

Re: AlphaProof's Greatest Hits

#50

Post by seizethecheese »

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.

Both comments can be right. People don’t need to know HTML to use the internet.
Post reply on HN