M. M. Adams, “Proof Auditing Formalised Mathematics”, JFR, vol. 9, no. 1, pp. 3–32, Jan. 2016.