Email: kymiller@ucsc.edu

Office: BE-353A

Pronouns: he/him

I am an assistant professor at UC Santa Cruz. I work on formalized mathematics and interactive theorem provers, and previously I studied low-dimensional topology (especially knot theory) and combinatorics. I am a maintainer for the mathlib, the Lean mathematical library. I am also affiliated with the Lean FRO.

I spent the 2022-2023 academic year at Université Paris-Saclay, working on formalized mathematics with Patrick Massot and Floris van Doorn. Before that, I completed my PhD at UC Berkeley, supervised by Ian Agol.

I am interested in making tools for education and research:

- KnotFolio, for drawing and recognizing knots
- PyQuiz, for creating sophisticated, randomized Canvas quizzes for mathematics courses
- Toys and demonstrations (on my UC Berkeley page)
- arrow_poly, for calculating arrow polynomials of virtual knots
- planalg, for working with planar algebras and diagrammatic categories

Older software projects:

- Plover, a language for linear algebra on embedded systems, at Swift Navigation
- news_crowdsourcer, for crowdsourcing questions about news articles, at Microsoft Research New England

CV: (pdf)

This page is under construction. You can also see my old UC Berkeley page.

- 2023.
*The homological arrow polynomial for virtual links*, Journal of Knot Theory and Its Ramifications. arXiv:2207.02427. - 2022. PhD thesis, "Singularity theory for extended cobordism categories and an application to graph theory". (pdf)
- 2021. Anderson, Baker, Gao, Kegel, Le, Miller, Onaran, Sangston, Tripp, Wood, and Wright,
*L-space knots with tunnel number >1 by experiment*, Experimental Mathematics. arXiv:1909.00790. - 2018. McPhail-Snyder and Miller,
*Planar diagrams for local invariants of graphs in surfaces*, Journal of Knot Theory and Its Ramifications. arXiv:1805.00575.

Where *formalization* is the process of taking mathematics and creating a machine-checkable formal treatment (for example, Lean code),
*informalization* is the reverse, taking formalized mathematics and creating an informal document.
With informalization, we can author structured proofs that allow the reader to inspect a proof to any level of detail.

**Examples:**

- Rudin, open iff complement is closed: Lean, informalization
- Bourbaki, extension to continuous function: Lean, informalization

Slides for talk at UCSC CSE Colloquium, 2024/01/24: (pdf)