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.