Jack McKoen

About me

I am a Ph.D. student in logic/mathematics 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.