Nori's construction in Lean, or the many ways that a formalization project can fail.

Abstract: Nori's construction, also known as Nori's universal factorization, is a 2-universal construction in category theory. Though it looks very abstract and can be deduced from existing results in a few lines, it underlies the construction of the far from trivial category of Nori motives. The goal of this talk is to briefly explain what Nori's construction is and why I wanted to formalize it, then to report on the many things that went wrong (and a couple that went right). Familiarity with categories would be helpful to follow the details.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

Lean Together 2026