Kim Morrison

Timeline

1. 2007–2012

   Berkeley PhD and Station Q

   After first class honours and the University Medal in pure mathematics at the University of New South Wales, Kim Morrison completes a PhD at the University of California, Berkeley, in March 2007, studying with Vaughan Jones; the thesis wins the Herbert Alexander Prize for Outstanding Dissertation in Pure Mathematics. They spend 2007 to 2009 as a postdoc at Microsoft Station Q at UC Santa Barbara and 2009 to 2012 as a Miller Fellow in Berkeley's mathematics department.

2. September 2009

   Co-founding MathOverflow

   Working with Berkeley colleagues Anton Geraschenko and David Zureick-Brown, they start MathOverflow, a mathematics question-and-answer website, in September 2009.

3. 2012–2020

   Professor at ANU

   They join the Australian National University in 2012 as a Senior Lecturer with an ARC Discovery Early Career Research Award. Promotion to Associate Professor follows in 2016, an ARC Future Fellowship begins in 2018, and they become a Professor in 2020. Their research covers topological quantum field theories, Khovanov homology, and the classification of subfactors and tensor categories.

4. 2015

   The Heyde and AustMS medals

   In 2015, they receive the Christopher Heyde Medal from the Australian Academy of Science and the Australian Mathematical Society Medal.

5. Since 2017

   Formalizing mathematics in Lean

   Formalization work in Lean and Mathlib begins in 2017, and they serve as one of Mathlib's maintainers. Their papers include The Lean Mathematical Library, the Mathlib paper at CPP 2020, and Schemes in Lean, published in Experimental Mathematics in 2022.

6. August 2023–July 2024

   Omega and machine-learning tools

   At the Lean Focused Research Organization, formed in July 2023, they lead work on Lean's continuous integration during its first year, from August 2023 to July 2024, and develop omega, a tactic for linear integer arithmetic in Lean 4. They also take the lead on tools for machine-learning research, including data extraction and a Lean REPL that they maintain for ML applications.

7. July 2026–August 2026

   Tau Ceti and Palomar

   In July 2026, they found Tau Ceti, a library of reusable formalized mathematics in which AI implementors and reviewers follow human-curated roadmaps, and describe it at a National Academy of Sciences meeting in Washington, DC. In August 2026, they help launch the Palomar Registry of Lean-verified mathematics, incubated by the Lean FRO and ICARM, and serve as a moderator, scientific advisory board member and its initial point of contact.

8. As of October 2026

   Senior engineer at the Lean FRO

   As a senior research software engineer at the Lean FRO, they build automation that makes it easier for humans and AIs to write difficult proofs in Lean, and they remain a Mathlib maintainer. With Leonardo de Moura, they describe grind, an SMT-inspired proof automation tactic for Lean 4, in a paper published at IJCAR 2026. A co-founder of the Mathlib Initiative, they sit on its strategic advisory board.