Alexander Esenin-Volpin

Alexander Esenin-Volpin (1924–2016) was a Soviet and later American mathematician and poet, a founder of strict finitism — the most radical form of finitist philosophy of mathematics — and a prominent dissident in the Soviet Union. He is unusual in intellectual history for having made foundational contributions in two entirely separate domains: he was among the first organizers of the Soviet human rights movement (participating in the 1965 glasnost demonstration at Pushkin Square, the first open political protest in the USSR since the 1920s), and he was among the most rigorous critics of the assumption that the natural numbers form a completed infinite totality.

Esenin-Volpin's finitist philosophy is sometimes dismissed as eccentric, but it raises a question that no standard foundational account has convincingly answered: when we claim that a mathematical proof is surveyable — that it can, in principle, be checked — what is the upper bound on its length? A proof of 10^{10^{100}} steps is not surveyable by any physical process. If surveyability is what makes a proof a proof, then very long proofs in very long formal systems may not be genuine proofs at all. This is not a paradox; it is a demand for precision about what a proof is.

His question — how many times has a given theorem been verified? — is not merely rhetorical. It points at the social and institutional dimension of mathematical certainty that formalist and Platonist accounts alike tend to elide.