kim morrison — programming mathematics & mathematics for programming.

I work at the Lean Focused Research Organization. I am a maintainer of the Mathlib formal mathematics library, which aims to curate and perfect mathematical knowledge as a coherent formal library. Mathlib is a large open-source community project, which serves as the foundation for all mathematical formalization in the Lean ecosystem. I helped found the Mathlib Initiative, and am a member of the strategic advisor board there. I'm the founder and maintainer of Tau Ceti, a library of reusable formalized mathematics which uses AI implementors and reviewers to follow human curated roadmaps.

I build automation for the Lean language, making it easier for humans and AIs to write difficult proofs. I also have time for experiments building Lean libraries and tactics using AI, to demonstrate what is possible when we combine the power of generative AI, the Lean language for automation, and the Lean kernel for reliable verification.

Recent posts:

• Exact algebraic numbers and number fields in Lean — exact arithmetic with algebraic numbers, and factoring, splitting and flattening in number field towers, with Mathlib proofs that the executable code is right.

• Certified graph isomorphism in Lean — HexGraphIso brings verified graph canonization and a graph_iso tactic to Lean.

• Announcing the Palomar Registry — an index of formalized mathematics repositories, with automatic checks on the formal statements and the metadata.

• Tau Ceti: ten theorems from the first month — ten highlights from a formal-mathematics library built by AIs following human-written roadmaps.

• Certified integer polynomial factorization in Lean — Berlekamp-Zassenhaus with van Hoeij reconstruction, formally verified for the first time.

• Why Lean is faster than Rust — a verified DEFLATE implementation that outcompresses miniz_oxide, faster.

• Lattice basis reduction using the Hex Lean library — a walkthrough of the Hex computational algebra library, culminating in a Coppersmith attack on RSA.

• Verified linear programming — a proof-carrying LP solver and a lp tactic, with no dependency on Mathlib.

• A sum of squares tactic — discharging nonlinear real inequalities via Harrison's sum-of-squares algorithm.

The full archive lives at /blog.