Kyle Miller

Assistant Professor of Engineering, UC Santa Cruz

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.

Selected work

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)