Recent research


  1. (with W. Kusner) Packings of Regular Pentagons in the Plane, preprint 2016, arxiv:1602.07220. {D}{R}
  2. (with J. Gordon) Endoscopic transfer of orbital integrals in large residual characteristic, Amer. J. Math. 138(1), February 2016, pp. 109–148, arxiv:1502.07368. {M}{L}{R}
  3. (with 21 other coauthors including A. Solovyev and Hoang Le Truong) A Formal proof of the Kepler conjecture, preprint 2014, arxiv:1501.02155. {D}{F}{R}{T}
  4. Developments in Formal Proofs, Bourbaki, year 66, number 1086, June 2014, arxiv:1408.6474. {F}{E}{R}
  5. The NSA back door to NIST, Notices of the AMS, 61(2), February 2014, pdf-link. {O}{E}{R}
  6. Mathematics in the Age of the Turing Machine, in Turing’s Legacy, Lecture Notes in Logic, 42, Cambridge, 2014, arxiv:1302.2898. {F}{E}{R}
  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}{R}
  8. The Strong Dodecahedral Conjecture and Fejes Toth’s Contact Conjecture, in Discrete Geometry and Optimization Series: Fields Institute Communications, Vol. 69 Bezdek, Karoly; Deza, Antoine; Ye, Yinyu (Eds.) 2013, arxiv:1110.0402. {D}{R}
  9. On the Reinhardt Conjecture, Vietnam Journal of Mathematics, 39(3), 2012, arxiv:1103.4518. {D}{R}
  10. Dense Sphere Packings: a blueprint for formal proofs, Cambridge University Press, LMS volume 400, 2012, pdf-link. {F}{D}{B}{R}{T}