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:

• 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.