Comment by matteoraso
18 hours ago
This is undeniably epochal, but I can't help but notice that this is yet another example of AI disproving rather than proving something. Is this just a coincidence, or does AI slightly struggle with proving theorems?[0]
[0] Struggle relative to its ability to disprove, not struggle relative to people's ability to prove theorems.
There has been the proof of the cycle double cover conjecture: https://news.ycombinator.com/item?id=48863490
I wouldn't call it "struggle", but it does seem better at proving "there exists" statements than proving "for all" statements.
I think you really have to squint to call this a disproof lol
It seems obvious what GP meant. It is, once again, an explicit construction (“disproving” that every initial state does not develop a singularity).
A bit of a hair-splitting, but isn't explicit construction the only way formal theorem provers can work? Of course you can still prove stuff with them, but certain axioms that more "human" proofs use may not be available, like law of excluded middle (every proposition is either true or false)
(Okay, they can be made available in a way similar to `unsafe` in rust)
1 reply →