Jeremy Avigad is a professor in the Department of Philosophy and the Department of Mathematical Sciences at Carnegie Mellon University, and a pioneer in using AI for mathematics.
He is the co-creator of the Lean Theorem Prover, director of the Hoskinson Center for Formal Mathematics at CMU, Dean’s Chair in Logic and Philosophy of Mathematics, and director of the newly-established Institute for Computer-Aided Reasoning in Mathematics under NSF.
Appearances
Key Contributions
- Co-creator of Lean: A theorem prover and programming language widely used for formal mathematics.
- Formal Mathematics: Leading research on formalization, computer-aided proof, and AI-assisted mathematics.