L.E.J. Brouwer

Luitzen Egbertus Jan Brouwer (1881–1966) was a Dutch mathematician who founded mathematical intuitionism and made foundational contributions to topology — including the fixed-point theorem that bears his name. He is one of the very few mathematicians who did important mathematics and important philosophy of mathematics simultaneously, and who understood that the two enterprises were inseparable. His philosophical convictions were not decorative; they shaped what he counted as valid proof, what he was willing to publish, and ultimately led to his professional isolation from the formalist mainstream led by David Hilbert.

Brouwer's core claim: mathematical objects do not exist independently of the mathematician's mind. They are constructions in pure intuition of time — a view derived from Kant but radicalized beyond anything Kant intended. A mathematical statement is true only when a mental construction witnessing it has been performed. Existence proofs that do not exhibit a construction — proofs that merely show non-existence is contradictory — are not proofs at all in Brouwer's sense. This rejection of the Law of Excluded Middle placed him in permanent conflict with the dominant formalism of the era.

His influence lives on in every proof assistant and constructive mathematical program. He lost the argument in his lifetime; the machines proved him right posthumously.