• Computer Assisted Proofs and the Kelvin Problem ICMS 2012.
  • Formal Proof Joint Math Meetings, January 2016.  Two slides have particular significance
  • Formal Abstracts , AITP, Obergurl, March 2017.
  • Big Conjecture Newton Institute, July 2017.  I need to make two corrections to the presentation.  First, a graduate student is already working on the proposed formalization project dealing with sphere packings.  Please do not undertake this formalization project without clearing it through Hales.  Second, my description of the Kelvin problem omits Huff’s work “Soap Films and Kelvin’s Curved, Truncated Octagon” which gives an elegant existence proof of Kelvin’s foam.  I am well aware of Huff’s work, and I regret my faulty description during my presentation.