How I learned to stop worrying…
...about Plato and love the mind: a quiet rebellion in mathematics
A peculiar, rarely spoken anxiety that can haunt the advanced study of mathematics begins as a whisper in the grand cathedral of calculus and grows to a low hum in the vaulted halls of real analysis. We are taught to move with confidence through landscapes of infinite sets, to speak of the continuum as the most fundamental fabric of the mathematical universe, as if it were a completed, static tapestry. We learn the sacred language, we map the elegant relations, then a subtle disquiet takes root. We begin to feel like a curator in a museum of eternal, perfect forms or a clerk in a vast, celestial bureaucracy, processing truths that were stamped “approved” before the dawn of time. The numbers do not need us. The theorems simply are. Our intellectual labour risks being reduced to the work of a scribe, copying inscriptions from the walls of a Platonic eternity.
This unease is the silent prologue to a sincere intellectual rebellion. It asks the deceptively simple question: what are we doing when we do mathematics? Are we explorers discovering continents on a pre-existing globe or are we architects, builders and composers? The dominant, classical view suggests the former. Intuitionism, a philosophical tradition born in the early 20th century, chooses the latter with radical, thrilling consequences. It proposes that mathematics is not a description of a remote, perfect realm, but the recorded activity of the human mind constructing its own coherent world. This is the (shortened) story of that quiet rebellion: why it began, how it rebuilds the world from the ground up and why, in our digital era, its once-heretical principles have found a startling and powerful vindication.
To escape the metaphysical weight of Platonism, the founder of the intuitionistic concept, Dutch mathematician and philosopher L.E.J. (Bertus) Brouwer, performed a dramatic act of intellectual ground-clearing. He rejected the idea that mathematics should be founded on elaborate axiomatic systems about sets. Instead, he sought its origin in something more fundamental than any axiom: the structure of human consciousness itself. He called this the “primordial intuition of time.”
This does not refer to clock time, but to the bare, inescapable form of experience: the awareness of one moment and then a next. From this slender thread of “and then,” Brouwer spun the entire natural number sequence. The act is one of pure, willed attention: hold a single moment of awareness (call this ‘one’); let it fall away and enact a new, distinct act (‘and then’). This composite, a retained past and a living present, is the mental construct ‘two’. The process is iterative, open-ended and dynamic. ‘Four’ is not a freestanding celestial object; it is the location you arrive at after three successive applications of this “and then” operation. In this view, numbers cease to be nouns and become adverbs; they describe the manner of our counting, not pre-counted objects.
This shift from static object to mental activity rewrites the rulebook. If numbers are mental constructions, then operations like addition cannot be discovered relations. They must be defined as construction manuals. We stipulate rules: adding one means moving to the successor; adding a successor to a number means finding the successor of the sum. This recursive definition is the essence of the algorithm, a precise recipe.
Take the archetypal truth, “2 + 2 = 4.” Classically, this is an eternal fact. Constructively, it is a performative ritual. You follow the manual: 2 + 2 is 2 + (successor of 1), which by rule is the successor of (2+1). And 2+1 is the successor of 2, which is 3. So we need the successor of 3, which is 4. The equals sign here undergoes a metamorphosis. It no longer signals a static identity between two independent Platonic entities. It becomes a signpost marking the convergence of mental journeys: the constructive process initiated by “2+2” terminates at the exact same mental location as the simple construction “4.” Truth is no longer correspondence with a remote reality; it is the successful, verifiable completion of a construction.
This new foundation cracks the classical structures open at two critical junctures: the meaning of existence and the validity of logic.
In classical mathematics, you can prove something exists through a reductio ad absurdum: assume it doesn’t, derive a contradiction and therefore conclude it must. This proof offers a ghost, a guaranteed entity with no instructions for finding it. It is like being told, with logical certainty, that a specific priceless book must be somewhere in an infinite, dark library, yet receiving no shelf mark, no map, no flashlight. The intuitionist finds this hollow. To claim “there exists” is to claim you can, in principle, produce the thing. Existence is the correlate of a constructive act: a witness must be presented. A proof of existence is a discovery protocol, not a verdict from the bench of logic.
This demand for evidence leads directly to a confrontation with the most sacred law of classical reasoning: the Principle of the Excluded Middle. Mistaken for a law, it states that for any meaningful proposition P, either P is true or not-P is true. There is no middle ground. For finite, decidable statements, “There are seven perfect squares less than 50”, this is constructively sound. You can run the algorithm and get a yes or no.
But apply it to an unsolved problem about an infinite totality, like the Goldbach Conjecture (“Every even number greater than 2 is the sum of two primes”). The classicist, relying on the Excluded Middle, asserts: “It is either true or false, even if we never know which.” The intuitionist sees this as a towering metaphysical presumption. It assumes the infinite set of even numbers is a completed, determinate object where every property is already decided. Lacking both a constructive proof for all evens and a constructed counterexample, the intuitionist simply says the statement is undecided. To assert “true or false” anyway is to confuse the comforting bivalence of our language with a hidden fact about a finished universe. Logic, for the intuitionist, becomes a descriptive science of valid constructive reasoning, not a set of transcendent laws governing a Platonic realm.
Nowhere is the intuitionistic revolution more radical, or more beautiful, than in its re-engineering of the continuum, the mathematical analogue of the smooth, unbroken line. The classical real number line is a set of points, each corresponding to a completed, actually infinite decimal expansion. It is a frozen galaxy of finished processes.
From the constructive ground of temporal consciousness, this is incoherent. An infinite process cannot be a finished object. So, the intuitionist reimagines a real number as a becoming. It is a law or even a freely chosen path, that generates better and better rational approximations. The number π is not the mythical, infinite string “3.14159…”; it is the algorithm that, when asked for precision to *n* decimal places, reliably produces it. The continuum is not a set of static points but a “medium of free becoming,” a restless arena where numbers are lived trajectories of approximation.
This reconception has a stunning, elegant consequence: in the intuitionistic continuum, every total function is continuous. The monstrous, pathological functions of classical analysis, those that jump wildly at isolated points, vanish. This discards the classical monsters where a function, defined point-by-point, can make a discontinuous leap by checking an input against an infinitely long decimal expansion. An intuitionistic function cannot perform such a check; it can only transform how we build the input into how we will build the output. To know the output to any desired precision, you need only know the input to a sufficient precision. It is a universe inherently respectful of finite information and stepwise process, where discontinuity, requiring omniscient knowledge of a completed infinite, becomes a non-sequitur.
This is may appear a barren landscape of negation. It is however a different and strangely fertile ecology. Constructive algebra develops finer, more meaningful classifications (distinguishing between fields where you can find roots and those where you merely know they exist). Analysis cultivates positive relations like apartness, a demonstrable, finite separation between numbers that is stronger than mere abstract inequality. Theorems in this world carry more information because their proofs are inherently recipes; an existence proof delivers the object, a disjunction proof tells you which side is true.
For decades, intuitionism was viewed as a fascinating philosophical heresy, brilliant but impractical, shackled to Brouwer’s almost mystical view of the creative subject. Its redemption came through two paths: pragmatic moderation and technological inevitability.
The American mathematician Errett Bishop, in the 1960s, performed a monumental act of synthesis. In his Foundations of Constructive Analysis, he stripped away Brouwer’s more subjective elements while fiercely preserving the constructive core. He rebuilt vast tracts of advanced mathematics, analysis, algebra, measure theory, without appeals to the Excluded Middle or completed infinities. Bishop showed that the deep, useful content of mathematics was not reliant on classical metaphysics; it could be recovered through meticulous, constructive means. He turned a philosophy into a rigorous, practicable mathematical practice.
Then came the thunderclap of vindication from an unforeseen quarter: theoretical computer science. The Curry-Howard correspondence (or “proofs-as-programs” isomorphism) revealed a deep identity between intuitionistic logic and the theory of computation. In this paradigm:
- A logical proposition corresponds to a type (a specification for data).
- A proof of that proposition corresponds to a program that inhabits that type.
- The logical rules for constructing a proof correspond precisely to the rules for writing a valid program.
Suddenly, the intuitionistic dogma was transformed into computer science bedrock. A constructive proof of existence is a program that computes the witness. A proof of implication is a function that transforms input data into output data. Brouwer’s languageless mental construction found its perfect, executable expression in typed programming languages. Modern proof assistants like Coq, Agda and Lean are built directly on intuitionistic type theory. Formalising a theorem means writing a program; verifying a proof is to run the compiler. Our digital era, in its very logic, runs on intuitionistic principles.
The intuitionistic journey leads towards a more honest and human mathematics. It is a disciplined refusal to outsource the meaning of mathematical truth to a phantom realm. It insists that mathematics is not a cryptic inscription on the walls of eternity, but an ongoing, human conversation, a product of thought, time and attention.
Intuitionistic mathematics exchanges the oppressive (and frequently obsessive) grandeur of the Platonic cathedral, where we are mere visitors, for the luminous, collaborative workshop of the constructive mind, where we are architects. The weight of worrying about a finished, alien universe is lifted, replaced by the liberating responsibility of building a coherent, beautiful world whose solidity is guaranteed by the very act of its careful construction.
While in our days, the demarcation between abstract thought, algorithmic process and empirical science silently breaks down, this quiet rebellion offers a prescient framework. It presents a mathematics where truth carries the fingerprint of the intellect that forged it, where clarity is preferred to grandiose abstraction and where the infinite is no longer respected as a finished monument, making way for an open horizon of perpetual possibility. The mind, once anxious in the shadow of Plato’s perfect forms, finds its sovereignty and its serenity in the act of building.
*This is an abbreviated version of an article that will appear in a collection of essays on the subject later this year