Jack McKoen

mckoen at cmu dot edu

About me

I am a Ph.D. student in the Pure and Applied Logic program at Carnegie Mellon University. Previously, I completed a master's degree in mathematics at the University of Alberta, supervised by Adam Topaz. You can find my CV here.

I'm interested in formalizing mathematics using the proof assistant Lean. I regularly contribute to Lean's library of mathematics, mathlib, with a focus on category theory. Some of my contributions are summarized here.

For my master's thesis, I formalized an important theorem about quasi-categories. You can find that project here, and you can watch an earlier talk about it here.

Publications

  1. A dataset of formalised theorem statements from the Annals of Mathematics
    with Thomas Browning, Katerina Hristova, David Ledvinka, Justus Springer, Hang Lu Su, and Kevin Buzzard
    [arXiv] [NeurIPS MATH-AI '26]