Kyle Miller

Email: kymiller@ucsc.edu
Office: McHenry 4176
Pronouns: he/him

University of California Santa Cruz
Department of Mathematics (website)
1156 High Street
Santa Cruz, CA 95064

I am a postdoc in the mathematics department at UC Santa Cruz. I study low-dimensional topology (especially knot theory), combinatorics, and formalizing mathematics with proof assistants. 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)