Gentzen's 1936 proof that Peano Arithmetic is consistent proceeds by assigning ordinals below epsilon-zero to proof trees and showing that the cut-elimination procedure always terminates. The argument is nearly ninety years old, but formalizing it constructively — without classical logic's escape hatches — reveals gaps that informal mathematics papered over. Bryce and Gore provide the additional details and minor corrections necessary to make the well-foundedness of the cut-elimination argument hold in a constructive setting, machine-checked in Coq.
The corrections are not dramatic. They are the kind of details that vanish when a mathematician says “clearly” or “by a straightforward induction.” But constructive proof demands that every case be inhabited, every witness be produced, every descent be explicitly bounded. What was “clear” becomes a lemma. What was “straightforward” becomes a careful analysis of how ordinal assignments change under specific reduction steps.
Formalization doesn't just verify old results — it reveals where informal reasoning drew on principles it didn't declare. Every “minor correction” in a machine-checked proof is a place where human mathematics silently invoked an assumption that a constructive system refuses to grant for free. The consistency of arithmetic is not in question. What's in question is whether we can prove it using only the resources we claim to need.
(arXiv:2603.00487)