Can You Prove It Exists Without Finding It?

The Goldbach Puzzle and a Rule That Might Be Broken

In 1742, Christian Goldbach wrote a letter to the famous mathematician Leonhard Euler. He noticed that every even number bigger than 2 seemed to be the sum of two primes: 4=2+2, 6=3+3, 8=3+5, 10=5+5, 12=5+7… and so on. Goldbach asked: is this true for all even numbers? Almost 300 years later, nobody has proved it true or false for every even number. The Goldbach Conjecture remains one of the oldest unsolved problems in math.

Now imagine a mathematician saying, “Well, either the Goldbach Conjecture is true or it’s false.” That seems obvious—every statement must be either true or false, right? This idea is called the Law of Excluded Middle (LEM) : for any claim P, either P is true or its negation (not-P) is true. But here’s the catch: to assert that either P or not-P holds, a mathematician usually means they have a proof of P or a proof of not-P. They can decide which one. With the Goldbach Conjecture, we have neither. So should we really claim that the disjunction “Goldbach is true or Goldbach is false” is a proven fact? Some mathematicians, called constructivists, say no. They believe that asserting “P or Q” requires knowing which one holds. That leads to a giant crack in the foundation of classical mathematics.

What Does “Or” Really Mean? The Constructive Reinterpretation

Think of a detective who announces, “Either the butler committed the crime or the maid did.” If he can’t show which one, we wouldn’t call that a solved case. Constructivists feel the same way about mathematics. To them, the word “or” (∨) has a natural meaning: you can assert P ∨ Q only if you have a proof of P or a proof of Q. That’s the constructive interpretation of disjunction. Classical mathematics, however, got around the Goldbach problem by changing what “or” means. Classical logicians reinterpret P ∨ Q as “it’s contradictory that both P and Q are false.” This way, you can claim “Goldbach is true or Goldbach is false” without having a proof of either, because the idea of both being false would be nonsense. But constructivists argue this rewrite comes at a cost: you lose the ability to actually decide which side is right.

The constructive view doesn’t only affect “or”. It changes all logical words. The so-called BHK interpretation (after Brouwer, Arend Heyting, and Andrey Kolmogorov) says:

• To prove P ∧ Q (and), you need a proof of P and a proof of Q.
• To prove P ∨ Q, you need a proof of P or a proof of Q, and you must know which.
• To prove P → Q (implies), you need an algorithm that turns any proof of P into a proof of Q.
• To prove ¬P (not), you show that assuming P leads to a contradiction (like 0 = 1).
• To prove ∃x P(x) (there exists), you must construct a specific object x and prove P(x) holds.
• To prove ∀x P(x) (for all), you need an algorithm that, given any object x, proves P(x).

Under these rules, many classical theorems become suspect. You cannot prove something exists by showing it’s impossible for it not to exist; you must actually build it.

Existence Means You Can Build It

Here’s a classic trick that shows the difference. Consider √2, which is irrational (it cannot be written as a fraction). What about √2 raised to the power √2? A slick classical proof goes like this: Either √2^(√2) is rational, or it’s irrational. If it’s rational, we have an example of irrational a and b with a^b rational (a = b = √2). If it’s irrational, take a = √2^(√2) and b = √2. Then a^b = (√2^(√2))^(√2) = √2^(√2·√2) = √2^2 = 2, which is rational. So in either case, there exist irrational numbers a and b with a^b rational. But notice: the proof never tells you which pair actually works! We still don’t know whether √2^(√2) is rational. This is a nonconstructive existence proof : it shows something must exist without finding it.

Constructivists reject that as a valid existence claim. For them, you must present a specific pair and prove it works. This has deep consequences for real numbers. A constructive real number is essentially a computer program that produces rational approximations. If you claim “for every real x, either x = 0 or x ≠ 0,” that would mean you have a program that decides equality for any real number. But computers can misread tiny numbers as zero; there is no such decision procedure. So the statement is false under the constructive interpretation. That’s a Brouwerian counterexample to the law of excluded middle in real analysis. These counterexamples show that classical mathematics would require superhuman powers of decision—constructive math stays within what can actually be done algorithmically.

Different Flavors of Constructive Math: Brouwer, Bishop, and Beyond

Not all constructivists agree on the details. The first major figure, L.E.J. Brouwer (1881–1966), founded intuitionism. He believed mathematics is a creation of the human mind. For him, an object exists only if you can mentally construct it. Brouwer introduced radical ideas like free choice sequences: a real number could be built step by step, with each digit chosen freely, not predetermined by a rule. This leads to principles that make intuitionistic math very different from classical math. Brouwer’s followers developed a logic, intuitionistic logic, that captures the constructive interpretations we described.

In the mid-20th century, A.A. Markov in Russia developed a version called recursive constructive mathematics, where all objects are defined by recursive algorithms (the kind a computer can run). This style stays firmly within what a Turing machine can do, and it yields counterintuitive results, like a function that is pointwise continuous but not uniformly continuous—something impossible in classical smooth analysis.

Then in 1967, Errett Bishop dropped a bombshell. He showed that you could rebuild a huge chunk of modern analysis—theorems about integrals, Fourier series, and more—using only intuitionistic logic, without adopting Brouwer’s controversial free choice sequences or committing to recursive functions. Bishop’s constructive mathematics, often called BISH, is “neutral”: it doesn’t pick sides between intuitionism, recursive math, or even classical math. It simply avoids the law of excluded middle and demands constructive proofs. As a result, any theorem proved in BISH is automatically valid in all those interpretations. That makes BISH a kind of minimal, safe core of mathematics that everyone can read.

Bishop’s work also forged a crucial link to computer science. Since every constructive proof implicitly contains an algorithm, such proofs can often be translated directly into computer programs. Today, systems like Coq and Agda let mathematicians write constructive proofs and then automatically extract executable code. This has made constructive math a practical tool, not just a philosophical exercise.

Why It Still Matters: What Counts as a Real Proof?

So why should you care about a squabble over the meaning of “or”? Because it touches on what it means to know something. If a doctor says, “There exists a cure—it’s impossible for there not to be one,” you’d want to ask, “Okay, but what is it?” Constructive mathematics insists that a proof should give you a recipe, not just a negative guarantee. This mindset has shaped modern computing, where you need explicit algorithms, not abstract existence claims.

The debate also reveals that even basic logic isn’t settled once and for all. The law of excluded middle feels so natural, yet constructivists have built a rich, consistent mathematics without it—one that matches what computers can actually do. Philosophers still argue about whether constructive math is a correction to classical math or simply a different game with its own rules. Some point to the axiom of choice, a classical principle that, when interpreted constructively, turns out to imply the law of excluded middle—a surprising twist that shakes both sides.

Whether you side with the classical view or the constructive one, the fight over existence has forced mathematicians to be clearer about their assumptions. Next time you solve an equation and get a neat answer, ask yourself: did you really build that solution, or did you just argue that it must be there? That question, first asked over a century ago, is still making math sharper and more honest.

Think about it

1. If a mathematician tells you “there exists a number with property X” but can’t write it down, would you still believe them? Why or why not?
2. Imagine a video game proves a hidden treasure exists by logical reasoning, but the player can never find it. Is the treasure really in the game?
3. Could a proof that doesn’t give you a recipe ever be useful in real life, like in engineering or medicine?