Mathematics & Computation
What a Proof Assistant Changes
Formal verification does not abolish trust in mathematics. It relocates it — into a small kernel, a short list of axioms, and one fragile sentence: whether the formal statement says what the mathematician meant.