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

81–90 of 140 posts

Re: AlphaProof's Greatest Hits

#81

Post by Davidzheng »

GregarianChild wrote: post #19
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…

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…

The shortcut vs enumeration is definitely enormous right? just take average shannon entropy to the exponent of the length for example will be probably > heat death (or whatever death) of universe on all of human compute (I'm assuming I didn't bother to check but it seems intuitively true by a margin)

Re: AlphaProof's Greatest Hits

#82

Post by jamilton »

thesz wrote: post #71
samweb3 wrote: post #63

Earlier quoted context omitted.

I am building Memelang (memelang.net) to help with this as well. I'd love your thoughts if you have a moment!

You are building an SQL in disguise. First, you need to encode "memes" and relations between them at scale. This is not a language problem, it is data handling problem. Second, at some point of time you will need to query memes and relations between them, again, at scale. While expression of queries is a language problem, an implementation will heavily use what SQL engines does use. And you need to look at Cyc: https…

The PHP implementation works by converting it to SQL, so I'm sure they're aware.

Re: AlphaProof's Greatest Hits

#83

Post by nybsjytm »

Davidzheng wrote: post #80
nybsjytm wrote: post #64

Earlier quoted context omitted.

No, nobody has proved it. Side point, there is no existing AI which can prove - for example - the Poincaré conjecture, even though that has already been proved. The details of the proof are far too dense for any present chatbot like ChatGPT to handle, and nothing like AlphaProof is able either since the scope of the proof is well out of the reach of Lean or any other formal theorem proving environment.

what does this even mean? Surely an existing AI could reguritate all of Perelman's arxiv papers if we trained them to do that. Are you trying to make a case that the AI doesn't understand the proof it's giving? Because then I think there's no clear goal-line.

You don't even need AI to regurgitate Perelman's papers, you can do that in three lines of python.

What I meant is that there's no AI you can ask to explain the details of Perelman's proof. For example, if there's a lemma or a delicate point in a proof that you don't understand, you can't ask an AI to clarify it.

Re: AlphaProof's Greatest Hits

#84

Post by abrookewood »

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 mean ... calculators can do better at mathematics than most of us. I don't think they are going to threaten us anytime soon.

Re: AlphaProof's Greatest Hits

#86

Post by nybsjytm »

nine_k wrote: post #76
nybsjytm wrote: post #68

Earlier quoted context omitted.

If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking. For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving…

You can't talk about formally verifiable truthiness until you solve epistemology. This can be achieved formally in mathematics, with known principal limitations. Here strict theorem-proving, Lean-style, is viable. It can also be achieved informally and in a fragments way in barely-mathematical disciplines, like biology, linguistics, and even history. We have chains of logical conclusions that do not follow strictly,…

Hmmm I think even in something very nominally nearby like theoretical physics, there's very little that's similar to theorem proving. I don't see how AlphaProof could be a stepping stone to anything like what you're describing.

Generally, I think many people who haven't studied mathematics don't realize how huge the gulf is between "being logical/reasonable" and applying mathematical logic as in a complicated proof. Neither is really of any help for the other. I think this is actually the orthodox position among mathematicians; it's mostly people who might have taken an undergraduate math class or two who might think of one as a gateway to the other. (However there are certainly some basic commonalities between the two. For example, the converse error is important to understand in both.)

Re: AlphaProof's Greatest Hits

#87

Post by benlivengood »

nybsjytm wrote: post #68
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.

If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking. For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving…

Probabilistic reasoning is possible in a formal setting; It produces a probability distribution over answers. To ground probabilistic logic itself I'm not aware of much progress beyond the initial idea of logical induction[0].

[0] https://arxiv.org/abs/1609.03543

Re: AlphaProof's Greatest Hits

#88

Post by auggierose »

thesz wrote: post #70
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.

So, you looking for Cyc [1], practically. [1] https://en.wikipedia.org/wiki/Cyc

Does Cyc have proofs?

Re: AlphaProof's Greatest Hits

#89

Post by nybsjytm »

benlivengood wrote: post #87
nybsjytm wrote: post #68

Earlier quoted context omitted.

If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking. For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving…

Probabilistic reasoning is possible in a formal setting; It produces a probability distribution over answers. To ground probabilistic logic itself I'm not aware of much progress beyond the initial idea of logical induction[0]. [0] https://arxiv.org/abs/1609.03543

This takes for granted a formal setting, which is what I'm questioning in any of these 'real world' contexts.

Re: AlphaProof's Greatest Hits

#90

Post by nybsjytm »

Davidzheng wrote: post #79
nybsjytm wrote: post #16

Earlier quoted context omitted.

There are some AI guys like Christian Szegedy who predict that AI will be a "superhuman mathematician," solving problems like the Riemann hypothesis, by the end of 2026. I don't take it very seriously, but that kind of prognostication is definitely out there.

link to this prediction? The famous old prediction of Szegedy was IMO gold by 2026 and that one is basically confirmed right? I think 2027/2028 personally is a breakeven bet for superhuman mathematician.

I consider it unconfirmed until it happens! No idea where I saw it but it was probably on twitter.
Post reply on HN