Outreach
Media
I was featured in an article in the New York Times:- A.I. Is Coming for Mathematics, Too, New York Times, July 2, 2023.
- AI could be about to completely change the way we do mathematics, New Scientist, July 7, 2025.
- Mathematical beauty and truth in the age of AI, Quanta, April 30, 2025
- 'Brutal' math test raises the bar for AI, Science, December 5, 2024.
- Google has created a maths AI that has already proved 1200 theorems, New Scientist, April 25, 2019.
- Mathematicians bridge finite-infinite divide, Quanta, May 24, 2016. (Reprinted in Wired Magazine.)
- In computers we trust?, Quanta, February 22, 2013. (Reprinted in Wired Magazine.)
- What in the name of Euclid is going on here?, Science, March 4, 2005.
- Is mathematics obsolete?, preprint
- Mathematics and the formal turn, Bulletin of the American Mathematical Society, 61:225-240, 2024.
- What we talk about when we talk about mathematics, in Karine Chemla, José Ferreirós, Lizhen Ji, Erhard Scholz, and Chang Wang, editors, The Richness of the History of Mathematics, Springer, 651-658, 2023.
- Varieties of mathematical understanding, Bulletin of the American Mathematical Society, 59:99-117, 2022.
- Principia, Aeon magazine, September 24, 2018.
- You want proof? I'll give you proof! Mathematical arguments from Euclid to Lean, National Museum of Mathematics, November 6, 2024.
Meetings and Workshops
These are some of the meetings and workshops I have organized or co-organized.Big Proof 2025
Isaac Newton Institute, June 2025, co-organized with Ursula Martin, Heather Macbeth, Patrick Massot, Natarajan Shankar. Web page: html.AI for Mathematics and Theoretical Computer Science
SLMath and the Simons Institute, April 2025, co-organized with María Inés de Frutos-Fernández, Marijn Heule, Floris van Doorn, Adam Wagner, Sean Welleck. Web page: html.Formalization of Mathematics
SLMath, June 2023, co-organized with Heather Macbeth and Patrick Massot. Web page: html.Machine Assisted Proof
IPAM, February 2023, co-organized with Terence Tao, Erika Abraham, Kevin Buzzard, Jordan Ellenberg, Timothy Gowers, and Marijn Heule. Web page: html.Lean for the Curious Mathematician 2022
ICERM, July 2022, co-organized with Kevin Buzzard, Johan Commelin, Yury Kudryashov, Heather Macbeth, and Scott Morrison. Web page: html.Formal Methods in Mathematics / Lean Together 2020
Carnegie Mellon, January 2020, co-organized with Robert Lewis. Web page: html.Applications of Formal Methods to Control Theory and Dynamical Systems
Carnegie Mellon, June 2018. Web page: html.Big Proof
Isaac Newton Institute, summer 2017, co-organized with Leonardo de Moura, Georges Gonthier, Ursula Martin, J Strother Moore, Lawrence Paulson, and Natarajan Shankar. Web page: html.Logic and Analysis
AMS-ASL special session, January 2011, co-organized with Ulrich Kohlenbach and Henry Towsner. Web page: html
Policy
In March, 2025, I participated in an NSF workshop on the future of AI and the mathematical and physical sciences, and I contributed to a whitepaper (still in preparation).
In July, 2023, I participated in a National Academies workshop on AI to assist mathematical reasoning, and I served as a reviewer of the associated report.
Other
With Teddy Seidenfeld, I founded the Carnegie Mellon Summer School in Logic and Formal Epistemology, and I served as co-director from 2006-2010.
I used to maintain a web page listing resources for using formal methods in education.
When I was in graduate school, I taught a summer course for high school students called An intuitive approach to higher mathematics, with the Academic Talent Development Program.