Summer 2018 was a busy time filled with interesting meetings and projects. I enjoyed helping celebrate Tom Hales’ 60th birthday at a meeting dedicated to Tom’s many contributions in representation theory, discrete geometry, and formalized mathematics (conference website). Many attendees work with interactive theorem provers like Coq and Isabelle and I had good conversations regarding my plans to formalize theories of polynomial rings with additional operators. Also in Pittsburgh that week was a delightful follow-up workshop organized by Jeremy Avigad at Carnegie Mellon on the theme of formal methods in control theory and dynamical systems.
Continuing the theme of formal methods, I was grateful for the opportunity to attend the 2018 DeepSpec Summer School at Princeton. The ambitious DeepSpec project seeks to build a fully verified computing system from the hardware level to the user level by employing technologies like the Coq theorem prover. I gained a deeper understanding of formal methods and I appreciate the many conversations and working sessions with other attendees and the organizers.