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