Communications of the ACM, vol. 57, no. 4, pp. 66-75 (2014).
@ARTICLE{avigad-fvm, author = "Jeremy Avigad and John Harrison", title = "Formally Verified Mathematics", journal = "Communications of the ACM", year = 2014, volume = 57, number = 4, pages = "66--75"}