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).

▲

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-...