PeopleofSuperintelligence

Researcher

Kyle Miller

Also known as Kyle A. Miller, kmill

Kyle Miller is an assistant professor at UC Santa Cruz who works on interactive theorem provers and maintains mathlib, the Lean library of formalized mathematics. Trained in low-dimensional topology, he began formalizing mathematics in 2020, coauthored a Lean formalization of Hall's marriage theorem for mathlib in 2021, and earned a PhD at UC Berkeley under Ian Agol in 2022. During the 2022–2023 academic year, he worked on formalized mathematics at Université Paris-Saclay with Patrick Massot and Floris van Doorn, and by 2024 he was developing the Lean theorem prover as a research software engineer at the Lean Focused Research Organization. In 2025, he gave a talk at ICERM's Autoformalization for the Working Mathematician and coauthored LeanLTL, a Lean 4 framework for linear temporal logics. At UC Santa Cruz, where he joined the Baskin School of Engineering in 2024, his academic interests are interactive theorem provers and artificial intelligence, and he remains affiliated with the Lean FRO.

Works
3
Citations
8
h-index
2

Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

  1. 2018

    Graphs in surfaces at Berkeley

    As a PhD student advised by Ian Agol in the Berkeley mathematics department, he studies low-dimensional topology, especially knots and spatial graphs. In 2018, he and Calvin McPhail-Snyder post "Planar diagrams for local invariants of graphs in surfaces", which defines a planar diagram category for graphs embedded in surfaces; the paper appears in the Journal of Knot Theory and Its Ramifications in 2020.

  2. 2020–2021

    Hall's marriage theorem in mathlib

    He begins formalizing mathematics in 2020, and in June 2020 he gives the talk "Doing math the Lean way" at the Berkeley Lean Student Seminar. With Alena Gusakov and Bhavik Mehta, he posts a Lean formalization of Hall's marriage theorem for mathlib in January 2021, along with a description of the design of mathlib's simple graph library.

  3. 2022

    A Berkeley PhD under Ian Agol

    UC Berkeley awards him a PhD in 2022 for the dissertation "Singularity Theory For Extended Cobordism Categories and Applications To Graph Theory", with Ian Agol as advisor. In July 2022, he posts "The homological arrow polynomial for virtual links", a single-author paper that generalizes the arrow polynomial to framed oriented virtual links with labeled components.

  4. 2022–2023

    Formalization at Paris-Saclay

    During the 2022–2023 academic year, he works on formalized mathematics at Université Paris-Saclay with Patrick Massot and Floris van Doorn. At the SLMath summer school on the formalization of mathematics in June 2023, he gives the talk "From Lean to Informal Mathematics".

  5. By 2024

    Mathlib maintainer and Lean FRO engineer

    Alongside a postdoctoral position in mathematics at UC Santa Cruz, he works as a research software engineer at the Lean Focused Research Organization (FRO). By 2024, he is a developer of the Lean theorem prover and a maintainer of mathlib, its formal mathematics library.

  6. 2024

    Joining Baskin Engineering

    The Baskin School of Engineering at UC Santa Cruz welcomes him as an assistant professor of engineering for the 2024–25 academic year. His academic interests are interactive theorem provers and artificial intelligence, and his research builds software tools for mathematics, engineering and education.

  7. 2025

    LeanLTL at ITP 2025

    In April 2025, he gives a talk at ICERM's Autoformalization for the Working Mathematician. With Eric Vin and Daniel J. Fremont, he posts LeanLTL in July 2025, a Lean 4 framework for linear temporal logics that appears at ITP 2025. A 2025 preprint with Scott Kovach and others, "Fast Collection Operations from Indexed Stream Fusion", implements a collection library for Lean, Morphic and Rust and proves its functional correctness in Lean.

  8. As of October 2026

    Assistant professor at UC Santa Cruz

    He is an assistant professor at UC Santa Cruz, working on formalized mathematics and interactive theorem provers. A maintainer of mathlib, he is also affiliated with the Lean FRO. Through informalization, the reverse of formalization, he turns formalized Lean proofs into structured informal documents that let a reader inspect a proof to any level of detail.

Career

  1. Since 2024University of California, Santa CruzPostdoctoral researcher
  2. Since 2024Lean Focused Research OrganizationResearch Software Engineer
  3. 2022–2023Université Paris-Saclay

Education

  1. 2022University of California, BerkeleyPhD

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Most-cited works

  1. Formalising Szemerédi’s Regularity Lemma in Lean2021 · 5 citationsWith Bhavik Mehta
  2. Planar diagrams for local invariants of graphs in surfaces2019 · Journal of Knot Theory and Its Ramifications · 3 citations
  3. The homological arrow polynomial for virtual links2022 · Journal of Knot Theory and Its Ramifications · 0 citations

From OpenAlex, as of 21 October 2026.

  1. The median h-index is 48 at universities and 14 at frontier AI labsIncludes University of California, Santa Cruz. The median h-index is 48 at universities and 14 at frontier AI labs. We compare publishing careers, recent citations, dual appointments and job moves across 2,420 university researchers and 308 frontier-lab researchers.
  2. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes University of California, Santa Cruz. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other university. We compare doctorate and 5+ year employment links, career timing and current workplaces for 187 major-prize and 1,111 best-paper winners.
  3. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes University of California, Santa Cruz. We estimate where the people shaping AI studied and where their careers led. Massachusetts Institute of Technology leads with 467 former students, including 291 recorded doctorates.
  4. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes University of California, Santa Cruz. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Kyle Miller yet. Send us a free-licensed photo.

  1. Kyle Miller (archived UC Berkeley page) kmill.github.io. Checked 20 October 2026.
  2. [1805.00575] Planar diagrams for local invariants of graphs in surfaces arxiv.org. Checked 20 October 2026.
  3. Mathlib maintainers leanprover-community.github.io. Checked 20 October 2026.
  4. [2101.00127] Formalizing Hall's Marriage Theorem in Lean arxiv.org. Checked 20 October 2026.
  5. Kyle Miller - The Mathematics Genealogy Project mathgenealogy.org. Checked 20 October 2026.
  6. [2207.02427] The homological arrow polynomial for virtual links arxiv.org. Checked 20 October 2026.
  7. Kyle Miller - UCSC Engineering kmill.github.io. Checked 20 October 2026.
  8. SLMath | From Lean to Informal Mathematics legacy.slmath.org. Checked 20 October 2026.
  9. New faculty join Baskin Engineering with expertise in AI, sustainability, health engineering, and more engineering.ucsc.edu. Checked 20 October 2026.
  10. [2507.01780] LeanLTL: A unifying framework for linear temporal logics in Lean arxiv.org. Checked 20 October 2026.
  11. [2507.06456] Fast Collection Operations from Indexed Stream Fusion arxiv.org. Checked 20 October 2026.