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.

I am also featured in Kevin Hartnett's book, The Proof in the Code: How a Truth Machine Is Transforming Math and AI, about the early history of Lean.

I have been quoted in articles for the general public, often about the impact of AI and formal methods on mathematics. (Note the singularity in June, 2026.)

What it means to be a mathematician when AI does the math, IEEE Spectrum, June 25, 2026.
Is mathematics obsolete? Researchers are rethinking their purpose in the age of AI (in Spanish), El País, June 16, 2026.
Humans outperform AI at this highly rigorous mathematics test, Nature, June 12, 2026.
Knowledge collapse, Boston Review, June 10, 2026.
They spent years on a math problem. Then they were scooped by A.I., New York Times, June 8, 2026.
Mathematicians warn of AI in their field (in Dutch), Trouw, June 3, 2026.
A golden age of maths is dawning and mathematicians are freaking out, New Scientist, June 1, 2026.
AI math proof milestone: DeepMind cracks 9 Erdös problems, Tech Times, May 30, 2026.
The AI revolution in math has arrived, Quanta, April 13, 2026.
Mathematics is undergoing the biggest change in its history, New Scientist, March 10, 2026.
Math in the age of AI, Communications of the ACM, February 17, 2026.
Mathematicians say Google's AI tools are supercharging their research, New Scientist, November 18, 2025.
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.
Machine-human collaborations accelerate math research, Notices of the American Mathematics Society, October, 2023.
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.)
Automating proofs: Math struggles with the usability of formal proofs, Communications of the ACM, April 1, 2016.
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.

Here are some panel discussions and podcasts:

"Proof in the Code: The Builders," Kevin Hartnett interview with Leonardo de Moura, Sebastian Ullrich, and me, June 12, 2026, YouTube.
"It's Our Mathematics: AI, Verification, and the Future of Math," The Augmented Mind Podcast, June 9, 2026, video.
Panel discussion on mathematics and AI with Jennifer Johnson-Leung, Jabob Tsimmerman, and Ravi Vakil, VanTAGe math, May 5, 2026, YouTube.

Here are some public presentations:

a short interview in the newly announced Institute for Computer-Aided Reasoning in Mathematics on a local TV station in Pittsburgh.
the Hoskinson Center inauguration

I am proud of a talk I gave at the National Museum of Mathematics in New York City:

You want proof? I'll give you proof! Mathematical arguments from Euclid to Lean, National Museum of Mathematics, November 6, 2024.

I was once interviewed by Richard Marshall for his 3:16 collection.

Essays and other writings

Several of my essays are aimed at a general audience. It is nice to see the medium appreciated in this blog post.

Mathematicians in the age of AI, unpublished.
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.
The mechanization of mathematics, Notices of the AMS, 65(06):681-690, 2018. Reprinted in Mircea Pitici editor, The Best Writing on Mathematics 2019, Princeton University Press, 2019, 150-170.
Principia, Aeon magazine, September 24, 2018.

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. Report: 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 the whitepaper.

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.