Adam Topaz


I am a mathematician working primarily in algebra and arithmetic / algebraic geometry. My research interests 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.

I am currently an Assistant 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 work 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 Lean3, which is built by the leanprover community. I am also a primary member of the Liquid Tensor Experiment, which was completed as of 2022-07-14.

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

In Fall 2023, I will be teaching 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.



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