Kyle Miller

Email: kymiller@ucsc.edu
Office: E2-355
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.

Selected work

• 2025. Vin, Miller, and Fremont, LeanLTL: A unifying framework for linear temporal logics in Lean, ITP 2025. arXiv:2507.01780.
• 2025. Kovach, Kolichala, Miller, Broman, and Kjolstad, Fast Collection Operations from Indexed Stream Fusion, preprint. arXiv:2507.06456.
• 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.

Informalization

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)