Comment by rescrv

I'm not sure if this is real, but the abstract says machine-verified.