Adam Topaz


I am a mathematician working primarily in formalized mathematics, algebra, and arithmetic / algebraic geometry. I am currently an Associate Professor in the department of Mathematical and Statistical Sciences at the University of Alberta. I previously held postdoctoral positions at Oxford and Berkeley. I completed my Ph.D. in 2013 at the University of Pennsylvania.




The best way to contact me is through email, using the following address:

Mailing Address

Mathematical and Statistical Sciences
University of Alberta
632 Central Academic Building
Edmonton, Alberta
Canada T6G 2G1



Formalization of pure mathematics

A large part of my research since 2020 has been related to the formalization of pure mathematics, primarily using the Lean interactive theorem prover. I am one of the maintainers of mathlib, the mathematics library of Lean, which is built by the leanprover community. I am also a primary member of the Liquid Tensor Experiment, which was completed on 2022-07-14.

Here is a (incomplete) list of repositories containing formal mathematics where I was/am a contributor:

In Fall 2023, I taught a PIMS network-wide graduate course on the formalization of mathematics. Information about this course can be found on the PIMS webpage, and some additional comments can be found in this PDF.

Pure mathematics

My research interests in pure mathematics mostly revolve around Galois theory, with an emphasis on anabelian geometry and other related topics in arithmetic/algebraic geometry. I am also interested in various other topics, such as algebraic cycles, Hodge theory (Archimedean and p-adic), valuation theory, differential Galois theory, model theory of fields, etc.



My papers are mostly all available on the arXiv. Here is my listing on mathscinet. The PDF links below are always the most up-to-date.