Most active commenters

    ←back to thread

    AlphaProof's Greatest Hits

    (rishimehta.xyz)
    248 points rishicomplex | 11 comments | 17 Nov 24 17:20 UTC | HN request time: 0.001s | source | bottom
    Show context
    nybsjytm ◴[17 Nov 24 20:34 UTC] No.42166977[source]▶
    Why have they still not released a paper aside from a press release? I have to admit I still don't know how auspicious it is that running google hardware for three days apiece was able to find half-page long solutions, given that the promise has always been to solve the Riemann hypothesis with the click of a button. But of course I do recognize that it's a big achievement relative to previous work in automatic theorem proving.
    replies(2): >>42167197 #>>42167309 #
    whatshisface ◴[17 Nov 24 21:00 UTC] No.42167197[source]▶
    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 average reasoning. Our society is structured around avoiding confronting people with difficult questions, except when they are intended to get the answer wrong.

    replies(3): >>42167281 #>>42167469 #>>42167489 #
    1. GregarianChild ◴[17 Nov 24 21:09 UTC] No.42167281[source]▶
    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 were run for 3 days. If it's somebody's laptop, it would be super impressive. If it's 1000s of TPUs, then less so.
    replies(3): >>42167389 #>>42167421 #>>42169885 #
    2. Onavo ◴[17 Nov 24 21:20 UTC] No.42167389[source]▶
    > 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?

    replies(4): >>42167461 #>>42167504 #>>42167773 #>>42168056 #
    3. zeroonetwothree ◴[17 Nov 24 21:28 UTC] No.42167461[source]▶
    It’s just an obvious statement. If a proof exists, you will eventually get to it.
    replies(1): >>42170467 #
    4. kadoban ◴[17 Nov 24 21:32 UTC] No.42167504[source]▶
    It's a direct consequence of the format of a proof. They're finite-length sequences of a finite alphabet of symbols, so of course they're enumerable (the same algorithm you use to count works to enumerate them).

    If you want a computer to be able to tell that it found a correct proof once it enumerates it, you need a bit more than that (really just the existence of automated proof checkers is enough for that).

    5. E_Bfx ◴[17 Nov 24 22:07 UTC] No.42167773[source]▶
    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)
    replies(1): >>42168075 #
    6. Xcelerate ◴[17 Nov 24 22:49 UTC] No.42168075{3}[source]▶
    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”)?

    replies(2): >>42172070 #>>42181838 #
    7. Davidzheng ◴[18 Nov 24 05:12 UTC] No.42169885[source]▶
    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)
    8. j16sdiz ◴[18 Nov 24 07:24 UTC] No.42170467{3}[source]▶
    Only if we take AC, I guess?
    replies(1): >>42171957 #
    9. Tainnor ◴[18 Nov 24 13:01 UTC] No.42171957{4}[source]▶
    No, this has nothing to do with choice.
    10. Tainnor ◴[18 Nov 24 13:19 UTC] No.42172070{4}[source]▶
    It's "obvious" in the sense that it's a trivial corollary of the completeness theorem (so it wouldn't be true for second order logic, for example).

    Hilbert's program failed in no contradiction to what GP wrote because the language of FOL theorems is only recursively enumerable and not decidable. It's obvious that something is true if you've found a proof, but if you haven't found a proof yet, is the theorem wrong or do you simply have to wait a little longer?

    11. Turneyboy ◴[19 Nov 24 10:15 UTC] No.42181838{4}[source]▶
    Yeah but width-first immediately gives you the solution for any finite alphabet. So in that sense it is trivial.