Adams, M. M. Proof Auditing Formalised Mathematics. JFR 2016, 9, 3-32.