Category theory, formalised humanely (qtcat2026)

Formalisation is the process of expressing mathematical ideas in the language understood by a proof assistant, a computer program that enables the interactive construction of verified mathematical definitions, theorems, and proofs. The stereotypical understanding of formalisation is as the rote translation of pre-existing mathematics to a cumbersome formal language, done primarily as a means of certifying the correctness of an argument. This memetic conception as a chore standing in the way of a coveted result (guaranteed correctness) has long allowed the aesthetics of formalisation to be appropriated by adversarial actors to further their financial interests ("get paid for proving lemmas on the blockchain"/"our new LLM will totally solve All Of Maths, and we have the Lean to prove it"). I aim to challenge this understanding, presenting the process of formalisation, in itself, as a force for good. I will share some of my own experiences with free-and-libre, community-supported proof assistants as a tool for independent study; genuine mathematical insights revealed by developing category theory within formal univalent type theory; and a few challenges that come with maintaining a library of formalised mathematics. Licensed to the public under https://creativecommons.org/licenses/by/4.0/ about this event: https://pretalx.c3voc.de/qtcat-2026/talk/9F8KNH/