Jack McKoen

About me

I recently 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 higher category theory.

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.

My profiles