Proofs as Infrastructure
Formalization turns mathematical trust from a mood into a maintenance discipline.
A proof in a paper is a persuasive object. A proof in a proof assistant is an artifact with a supply chain.
This does not make the mechanized proof more holy. It makes it more industrial. It has dependencies. It has names. It has compile times. It has refactors. It breaks when a definition changes and, in breaking, tells you something precise about where your understanding was coupled to an old shape of the world.
For mathematics that wants to become infrastructure, this is a gift.
A proof in a paper is built to persuade a reader. Its dependency graph is real, but the edges are soft: a phrase like by the usual identification can hold a small cathedral of coercions and implicit transport. In a seminar this compression is humane. In infrastructure it is a liability.
The proof assistant asks the impolite question: which encoding, exactly, and injective with respect to what? Every soft edge becomes a typed boundary. The theorem statement stops being a paragraph and becomes an API, a promise you are allowed to build on.
A definition changes at the bottom of the graph. The proof breaks, but
it breaks precisely: only the lemmas that actually depended on the old
shape of encode fail, and everything else stands untouched. A paper
cannot tell you this. A mechanized proof can tell you nothing else.
While repairing the break, you notice that a dependency can be generalized, and a two-step detour collapses into one direct lemma. The proof gets shorter. The statement gets more honest.
The repaired lemma lands in a shared library, and now there is a lit route from the definitions to the theorem. The next person who needs this fact takes the route in one line instead of one week. A good lemma is public infrastructure.
The problem with elegant ambiguity
Mathematicians are good at compressing arguments. A phrase like “by the usual identification” can hold a small cathedral of coercions, equivalences, and implicit transport. In a seminar, this compression is humane. It keeps the conversation at the right altitude.
But infrastructure lives at low altitude.
A cryptographic standard cannot rely on the reader guessing which encoding is canonical. A verified implementation cannot leave a boundary case to taste. A security proof cannot wave at a distribution and hope every implementer samples from the same one.
The machine asks the impolite question:
If the answer is yes, prove it. If the answer is no, the protocol may still be fine, but the ambiguity has become visible.
A theorem as an API
One useful way to think about formalization is that every theorem is an API. It promises that, under some inputs, a certain output can be relied upon.
In informal mathematics, the type of that API is carried by prose. In Lean, the type is the theorem statement itself.
structure Encoding (Message Bytes : Type) where
encode : Message -> Bytes
injective : Function.Injective encode
theorem decode_unique
{Message Bytes : Type}
(E : Encoding Message Bytes)
{x y : Message}
(h : E.encode x = E.encode y) :
x = y :=
E.injective hThis example is tiny, but it has the flavor of the thing. The property is not hidden in a comment. It is not a paragraph two sections away. It is part of the object you are allowed to use.
The theorem becomes a maintenance boundary.
Cryptography wants boring edges
Cryptographic systems are full of places where a small informal mismatch can become a large operational bug.
- Is the challenge bound to the transcript or only to part of it?
- Is the domain separator unique across protocols?
- Are two byte encodings injective into the same parser?
- Does the verifier check the same statement the prover thinks it proved?
- Is an epoch a date, a timestamp, or a key version?
These are not glamorous questions. That is why they are dangerous. They live at the edges of the proof, where the theorem meets the code and the code meets the network.
Formalization rewards boring edges. It asks you to name them, type them, and carry them through the argument.
The library is the civilization
The most important part of a proof assistant is not the checker. The checker is small, severe, and essential. But the day-to-day experience of formalization is really an encounter with a library.
Can you reuse a theorem about finite sums? Is the algebraic hierarchy shaped well enough that your object inherits the facts it should? Does a previous formalizer’s lemma make your proof one line instead of one week?
This is why formalization has a civic quality. A good lemma is public infrastructure. It shortens future work. It teaches the library a new route through the city.
When a theorem lands in a shared corpus, it stops being only a result. It becomes a path.
Proofs that survive contact
There is a romance of the final proof: the clean derivation, the polished argument, the sense that the theorem was always waiting in marble. Mechanized proof has a different romance. It is closer to engineering: the proof survives contact with change.
A definition is improved. The proof breaks.
A dependency is generalized. The proof gets shorter.
A hidden assumption is removed. The theorem statement becomes honest.
This feedback loop is not a tax on the work. It is the work becoming real.
What should be formalized
Not everything needs to be in Lean. Some ideas are exploratory. Some arguments are too young. Some papers are valuable because they change how a community thinks, not because they pin down an interface.
But some mathematics is load-bearing. It sits under standards, compilers, cryptographic libraries, consensus protocols, proof systems, parsers, and safety-critical code. For that mathematics, informal confidence is not the right terminal state.
The question is not whether every proof should be mechanized.
The question is which proofs we are comfortable rebuilding by hand every time the world changes around them.