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

31–40 of 140 posts

Re: AlphaProof's Greatest Hits

#31

Post by nybsjytm »

zeroonetwothree wrote: post #26
whatshisface wrote: post #18

Earlier quoted context omitted.

I don't know why so few people realize this, but by solving any of the problems their performance is superhuman for most reasonable definitions of human. Talking about things like solving the Reimman hypothesis in so many years assumes a little too much about the difficulty of problems that we can't even begin to conceive of a solution for. A better question is what can happen when everybody has access to above avera…

Well, multiply two large numbers instantly is a superhuman feat a calculator can do. I would hope we are going for a higher bar, like “useful”. Let’s see if this can provide proofs of novel results.

It's worth emphasizing that it's been possible for years to use an automatic theorem prover to prove novel results. The whole problem is to get novel interesting results.

Re: AlphaProof's Greatest Hits

#32

Post by wslh »

uptownfunk wrote: post #29
wslh wrote: post #12

Earlier quoted context omitted.

I understand that a group of motivated individuals, even without significant financial resources, could attempt to tackle these challenges, much like the way free and open-source software (FOSS) is developed. The key ingredients would be motivation and intelligence, as well as a shared passion for advancing mathematics and solving foundational problems.

Ok but how do you get around needing a 10k or 100k h100 cluster

It is well known that cloud services like Google Cloud subsidizes some projects and we don't even know if in a few years improvements will arise.

Re: AlphaProof's Greatest Hits

#33

Post by whatshisface »

zeroonetwothree wrote: post #26
whatshisface wrote: post #18

Earlier quoted context omitted.

I don't know why so few people realize this, but by solving any of the problems their performance is superhuman for most reasonable definitions of human. Talking about things like solving the Reimman hypothesis in so many years assumes a little too much about the difficulty of problems that we can't even begin to conceive of a solution for. A better question is what can happen when everybody has access to above avera…

Well, multiply two large numbers instantly is a superhuman feat a calculator can do. I would hope we are going for a higher bar, like “useful”. Let’s see if this can provide proofs of novel results.

The ability to multiply two numbers superhumanly has already transformed society.

Re: AlphaProof's Greatest Hits

#34

Post by whatshisface »

nybsjytm wrote: post #28
whatshisface wrote: post #18

Earlier quoted context omitted.

I don't know why so few people realize this, but by solving any of the problems their performance is superhuman for most reasonable definitions of human. Talking about things like solving the Reimman hypothesis in so many years assumes a little too much about the difficulty of problems that we can't even begin to conceive of a solution for. A better question is what can happen when everybody has access to above avera…

> A better question is what can happen when everybody has access to above average reasoning. Our society is structured around avoiding confronting people with difficult questions, except when they are intended to get the answer wrong. What does this have to do with a hypothetical automatic theorem prover?

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

Re: AlphaProof's Greatest Hits

#35

Post by nybsjytm »

whatshisface wrote: post #34
nybsjytm wrote: post #28

Earlier quoted context omitted.

> A better question is what can happen when everybody has access to above average reasoning. Our society is structured around avoiding confronting people with difficult questions, except when they are intended to get the answer wrong. What does this have to do with a hypothetical automatic theorem prover?

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!)

Re: AlphaProof's Greatest Hits

#36

Post by E_Bfx »

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?

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)

Re: AlphaProof's Greatest Hits

#37

Post by ccppurcell »

wslh wrote: post #11
zarzavat wrote: post #9

Earlier quoted context omitted.

Probably a bad example, P vs NP is the most likely of the millennium problems to be unsolvable, so the answer may be "never". I'll bet the most technical open problems will be the ones to fall first. What AIs lack in creativity they make up for in ability to absorb a large quantity of technical concepts.

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 I find it difficult to imagine them inventing new tools and objects that are really useful.

Re: AlphaProof's Greatest Hits

#38

Post by rowanG077 »

zeroonetwothree wrote: post #26
whatshisface wrote: post #18

Earlier quoted context omitted.

I don't know why so few people realize this, but by solving any of the problems their performance is superhuman for most reasonable definitions of human. Talking about things like solving the Reimman hypothesis in so many years assumes a little too much about the difficulty of problems that we can't even begin to conceive of a solution for. A better question is what can happen when everybody has access to above avera…

Well, multiply two large numbers instantly is a superhuman feat a calculator can do. I would hope we are going for a higher bar, like “useful”. Let’s see if this can provide proofs of novel results.

That superhuman capability of "multiplying two large numbers instantly" has transformed human society like not even plumbing has. I really can't see how this you could not consider this useful.
Post reply on HN