There has been the proof of the cycle double cover conjecture: https://news.ycombinator.com/item?id=48863490
replyI wouldn't call it "struggle", but it does seem better at proving "there exists" statements than proving "for all" statements.
replyI think you really have to squint to call this a disproof lol
replyIt seems obvious what GP meant. It is, once again, an explicit construction (“disproving” that every initial state does not develop a singularity).
replyA 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)
reply(Okay, they can be made available in a way similar to `unsafe` in rust)
you can add law of the excluded middle as an axiom. See midway down this page
replyhttps://xenaproject.wordpress.com/2017/10/05/more-easy-lean-...