The proof assistant verifies the theorem. Nobody else can read it.
The standard approach to formal mathematics (arXiv:2603.20893): proof assistants that verify every logical step, providing maximal correctness assurance. The cost — these systems are complex, based on logics unfamiliar to working mathematicians, difficult to learn, and far removed from mathematical practice. The gap between “formally verified” and “mathematically communicated” is wide.
The alternative: the “free approach,” which prioritizes accessibility and communication over complete verification. Implemented in Alonzo — a logic based on Church's simple type theory but adapted for mathematical practice. Instead of verifying all details, it provides a formal framework that mathematicians can use to communicate clearly, with verification as an optional layer rather than a requirement.
The tension is real and structural. Verification and communication optimize for different readers. Verification targets the machine: every inference explicit, every type annotation present, every lemma cited. Communication targets the mathematician: intuition first, formal detail compressed or omitted, the argument's shape prioritized over its complete logical scaffolding. Making the proof machine-readable makes it less human-readable. Making it human-readable leaves gaps the machine can't check.
The through-claim: correctness and clarity are in partial tension because they serve different verification authorities. A proof that convinces a mathematician relies on shared background, pattern recognition, and suppressed steps. A proof that convinces a checker relies on nothing shared — every step is explicit. The “free approach” bets that most mathematics needs to convince humans, not machines, and that the formalism should serve the communication rather than replace it.