Take a look at https://github.com/leanprover/comparator https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossi

Take a look at https://github.com/leanprover/comparator https://github.com/leanprover/comparator which was used to verify the result. It's of course not impossible that they're hitting some bug, but way harder than one would intuitively think. For starters, they'd have to hit two bugs in two independently written Lean kernels.