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.

▲

Kotlopou 7 hours ago | parent | next [-]

There has been the proof of the cycle double cover conjecture: https://news.ycombinator.com/item?id=48863490

▲

QuesnayJr 4 hours ago | parent | prev | next [-]

I wouldn't call it "struggle", but it does seem better at proving "there exists" statements than proving "for all" statements.

▲

chis 7 hours ago | parent | prev [-]

I think you really have to squint to call this a disproof lol

▲

thereitgoes456 7 hours ago | parent [-]

It seems obvious what GP meant. It is, once again, an explicit construction (“disproving” that every initial state does not develop a singularity).

▲

gf000 6 hours ago | parent [-]

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)

	▲	mswphd 4 hours ago \| parent [-]
		you can add law of the excluded middle as an axiom. See midway down this page https://xenaproject.wordpress.com/2017/10/05/more-easy-lean-...