The proof is written in the HOL4 proof assistant. The idea here is the same as any LCF derivative- there is a type, thm, and the constructors of that type are c

The proof is written in the HOL4 proof assistant. The idea here is the same as any LCF derivative- there is a type, thm, and the constructors of that type are constructed such that only valid theorems can be created. So, by creating a value of type thm, with that corresponding to your goal, you've proven the theorem. My proof works by creating such a value. There are obviously lots of places where this can go wrong, but good progress has been made towards most of them - http://materials.dagstuhl.de/files/15/15182/15182.KonradSlind.Slides2.pdf http://materials.dagstuhl.de/files/15/15182/15182.KonradSlin... is a decent explanation. As a handwavey argument, the proof could be incorrect, but if it were incorrect, the incorrectness would be more interesting than the current proof (i.e. a serious bug would have been located in the theorem prover).