Formal-proof

  1. Introduction to the Flyspeck project. Mathematics, Algorithms, Proofs, 05021, Dagstuhl Seminar Proceedings, Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany, 2006, pdf-link. {F}{D}
  2. Formal proof. Notices Amer. Math. Soc. 55 (2008), no. 11, 1370–1380, AMS-link. {F}
  3. Computational Discrete Gemetry, extended abstract in Mathematical Software — ICMS 2010, Proc. Third International Congress on Mathematical Software, 2010, LNCS 6327, pp. 1-3, Springer, 2010, pdf-link. {D}{F}
  4. Linear Programs for the Kepler Conjecture, extended abstract in Mathematical Software — ICMS 2010, Proc. Third International Congress on Mathematical Software, 2010, LNCS 6327, pp. 149–151, Springer, 2010, pdf-link. {D}{F}
  5. (with A. Solovyev) Efficient formal verification of bounds of linear programs, LNCS 6824, 2011, pdf-link. {F}
  6. Dense Sphere Packings: a blueprint for formal proofs, Cambridge University Press, LMS volume 400, 2012, pdf-link. {F}{D}
  7. (with A. Solovyev) Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations, proceedings of the fifth NASA Formal Methods Symposium (NFM) 2013, arxiv:1301.1702. {F}
  8. Mathematics in the Age of the Turing Machine, in Turing’s Legacy, Lecture Notes in Logic, 42, Cambridge, 2014, arxiv:1302.2898. {F}
  9. Developments in Formal Proofs, Bourbaki, year 66, number 1086, June 2014, arxiv:1408.6474. {F}
  10. (with 21 other coauthors) A Formal proof of the Kepler conjecture, preprint 2014, arxiv:1501.02155. {D}{F}
Advertisements