AlphaProof's Greatest Hits
rishimehta.xyz
AlphaProof's Greatest Hits
1–10 of 140 posts
Re: AlphaProof's Greatest Hits
#2[deleted]
Re: AlphaProof's Greatest Hits
#3If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.
Re: AlphaProof's Greatest Hits
#4More information about the language used in the proofs: https://en.wikipedia.org/wiki/Lean_(proof_assistant)
Re: AlphaProof's Greatest Hits
#5in the first question, why do they even specify ⌊n⌋ (and ⌊2n⌋ and so on) when n is an integer?
Re: AlphaProof's Greatest Hits
#6If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.
No one is focused on those. They're much more focused on more rote problems.
You might find them used to accelerate research math by helping them with lemmas and checking for errors, and formalizing proofs. That seems realistic in the next couple of years.
Re: AlphaProof's Greatest Hits
#7in the first question, why do they even specify ⌊n⌋ (and ⌊2n⌋ and so on) when n is an integer?
Alpha need not be an integer, we have to prove that it is
Re: AlphaProof's Greatest Hits
#8Re: AlphaProof's Greatest Hits
#9If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.
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.
Re: AlphaProof's Greatest Hits
#10If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.
The hard part is in the creation of new math to solve these problems not in the use of existing mathematics. So new objects (groups rings fields) etc have to be theorized, their properties understood, and then that new machinery used to crack the existing problems. I think we will get to a place (around 5 years) where AI will be able to solve these problems and create these new objects. I don’t think it’s one of technology I think it’s more financial. Meaning, there isn’t much money to be made doing this (try and justify it for yourself) and so the lack of focus here. I think this is a red herring and there is a gold mine in there some where but it will likely take someone with a lot of cash to fund it out of passion (Vlad Tenev / Harmonic, or Zuck and Meta AI, or the Google / AlphaProof guys) but in the big tech world, they are just a minnow project in a sea of competing initiatives. And so that leaves us at the mercy of open research, which if it is a compute bound problem, is one that may take 10-20 years to crack. I hope I see a solution to RH in my lifetime (and in language that I can understand)