301–310 of 564 posts
Earlier quoted context omitted.
Sure but if an AI can prove e.g the Goldbach conjecture then that is a bfd.
What if the proof were incomprehensible to humans?
Earlier quoted context omitted.
Or the simultaneous discovery of thousands of cryptographic exploits...
Still waiting for the first one. I'm not holding my breath - just like fuzzing found a lot of vulnerabilities in low-level software, I expect novel automated analysis approaches will yield some vulnerabilities - but that won't be a catastrophic event just like fuzzing wasn't.
Earlier quoted context omitted.
formal definition of first theorem already contain answer of the problem "{α : ℝ | ∃ k : ℤ, Even k ∧ α = k}" (which mean set of even real numbers).if they say that they have translated first problem into formal definition then it is very interesting how they initially formalized problem without including answer in it
I would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like {Formal description of the set in question} = ? And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above. I doubt they would claim to solve the problem if they provided half of the answer.
Stranger things have happened
Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
Sure but if an AI can prove e.g the Goldbach conjecture then that is a bfd.
Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
> Everyone's busy watching Magnus Carlsen. Actually, I was looking up Elo ratings of the top computer chess players, and learned that it is not that trivial to compare these, due to differences in hardware requirements and whatnot.
Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
Are all of these specialized models available for use? Like, does it have an API? I wonder because on one hand they seem very impressive and groundbreaking, on the other it’s hard to imagine why more than a handful of researchers would use them
If you could automatically prove that your concurrency protocol is safe, or that your C program has no memory management mistakes, or that your algorithm always produces the same results as a simpler, more obviously correct but less optimized algorithm, I think that would be a huge benefit for many programmers.
Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.
I don't think this principle extends to math proofs. It's much, much easier to verify a proof than to create it, and a second proof will just be a footnote. Not many mathematicians will want to work on that. That said, there is a lot of distance between IMO and the frontiers of research math.