Science explainedCiencia explicada / MathematicsMatemática
MathematicsMatemática
What makes a proof a proof?¿Qué hace que una demostración sea una demostración?
Checking a billion billion cases is not enough for a mathematician. A proof is something stronger: an argument that leaves no room for exceptions.Para un matemático, comprobar trillones de casos no basta. Una demostración es algo más fuerte: un argumento que no deja espacio para excepciones.
In 1742 Christian Goldbach suggested that every even number greater than 2 is the sum of two primes: 4 = 2 + 2, 10 = 3 + 7, 100 = 47 + 53. Computers have since checked the claim for every even number up to 4 × 1018, four billion billion of them. Not a single exception has turned up.
Goldbach's conjecture is still not a theorem. To a mathematician, four billion billion confirmations prove nothing about the even numbers that come after them, and there are infinitely many. A single counterexample, anywhere, would break the claim. What mathematics demands instead is a proof.
From agreed starting points
A proof is a chain of reasoning that starts from statements everyone accepts, called axioms, and moves forward only by steps that follow strictly by logic. Around 300 BC, Euclid's Elements organized all of Greek geometry this way: a handful of postulates, a few definitions, and hundreds of results, each one justified by what came before. The book was used to teach mathematics for more than two thousand years.
A proof you can hold in your head
Euclid also proved that there are infinitely many prime numbers, with an argument that still delights students. Suppose there were only finitely many primes. Multiply all of them together and add 1. The new number leaves a remainder of 1 when divided by any prime on the list, so none of them divides it. But every whole number larger than 1 has at least one prime factor. That factor must be a prime missing from the list, which contradicts the assumption that the list was complete.
Notice what happened. We did not check any cases. The argument works for every possible list at once, and that is exactly the kind of certainty that checking cannot provide.
When rigor got stricter
For centuries, proofs relied partly on intuition and pictures. In the 1800s, intuition about infinity and continuity began to fail: there turned out to be functions that are continuous everywhere yet have no smooth tangent anywhere. Mathematicians such as Augustin-Louis Cauchy and Karl Weierstrass responded by giving precise definitions of limits and continuity. Later, Gottlob Frege and David Hilbert went further and described proofs as sequences of symbols that could, in principle, be checked mechanically, step by step.
Proofs that need computers
In 1976 Kenneth Appel and Wolfgang Haken proved the Four Color Theorem: any map can be colored with four colors so that neighboring regions never share a color. Their proof reduced the problem to nearly two thousand configurations that a computer checked one by one. Many mathematicians were uneasy, because no human could verify every case by hand. In 2005 Georges Gonthier and Benjamin Werner settled the doubt by checking the entire proof with Coq, a program built to verify mathematical reasoning.
Something similar happened with Kepler's conjecture, which says that the familiar pyramid of oranges at a grocery store is the densest way to stack equal spheres. Thomas Hales announced a computer-assisted proof in 1998, but the referees could not check all of it. His Flyspeck project then completed a fully formal, machine-checked proof in 2014.
Proof assistants
Programs such as Lean, Coq (now called Rocq) and Isabelle are known as proof assistants. A mathematician writes the argument in a precise language, and the software refuses to accept any step that does not follow from the previous ones. In 2022 a community of Lean users verified a central and difficult theorem by Peter Scholze and Dustin Clausen, at Scholze's own invitation. More and more mathematicians now formalize their work this way.
So what is a proof?
A proof is an argument that convinces experts beyond reasonable doubt and that could, if needed, be expanded into fully formal steps that a machine can check. The best proofs do something more: they explain why a statement is true. That is why mathematicians keep looking for new proofs of old theorems, and why a conjecture like Goldbach's, however well tested, still waits for one.
En 1742, Christian Goldbach propuso que todo número par mayor que 2 es la suma de dos números primos: 4 = 2 + 2, 10 = 3 + 7, 100 = 47 + 53. Desde entonces, las computadoras han comprobado la afirmación para todos los números pares hasta 4 × 1018, es decir, cuatro trillones de casos. No ha aparecido ni una sola excepción.
La conjetura de Goldbach todavía no es un teorema. Para un matemático, cuatro trillones de confirmaciones no prueban nada sobre los números pares que vienen después, y hay infinitos. Un solo contraejemplo, en cualquier lugar, derrumbaría la afirmación. Lo que la matemática exige, en cambio, es una demostración.
Desde puntos de partida aceptados
Una demostración es una cadena de razonamientos que parte de afirmaciones que todos aceptan, llamadas axiomas, y avanza solo mediante pasos que se siguen estrictamente por la lógica. Hacia el año 300 a. C., los Elementos de Euclides organizaron así toda la geometría griega: unos pocos postulados, algunas definiciones y cientos de resultados, cada uno justificado por lo anterior. El libro se usó para enseñar matemática durante más de dos mil años.
Una demostración que cabe en la cabeza
Euclides también demostró que existen infinitos números primos, con un argumento que todavía encanta a los estudiantes. Supongamos que hubiera solo una cantidad finita de primos. Multiplicamos todos entre sí y sumamos 1. El nuevo número deja resto 1 al dividirlo por cualquier primo de la lista, así que ninguno de ellos lo divide. Pero todo número entero mayor que 1 tiene al menos un factor primo. Ese factor tiene que ser un primo que no estaba en la lista, lo que contradice la suposición de que la lista estaba completa.
Fíjese en lo que pasó. No comprobamos ningún caso. El argumento funciona para todas las listas posibles a la vez, y esa es justamente la clase de certeza que ninguna comprobación puede dar.
Cuando el rigor se volvió más estricto
Durante siglos, las demostraciones se apoyaron en parte en la intuición y en los dibujos. En el siglo XIX, la intuición sobre el infinito y la continuidad empezó a fallar: resultó que existen funciones continuas en todas partes que no tienen una tangente suave en ningún punto. Matemáticos como Augustin-Louis Cauchy y Karl Weierstrass respondieron dando definiciones precisas de límite y de continuidad. Más tarde, Gottlob Frege y David Hilbert fueron más lejos y describieron las demostraciones como secuencias de símbolos que, en principio, podían verificarse mecánicamente, paso a paso.
Demostraciones que necesitan computadoras
En 1976, Kenneth Appel y Wolfgang Haken demostraron el teorema de los cuatro colores: cualquier mapa puede colorearse con cuatro colores sin que dos regiones vecinas compartan color. Su demostración redujo el problema a casi dos mil configuraciones que una computadora revisó una por una. Muchos matemáticos se sintieron incómodos, porque ningún ser humano podía verificar todos los casos a mano. En 2005, Georges Gonthier y Benjamin Werner despejaron la duda al verificar la demostración completa con Coq, un programa creado para comprobar razonamientos matemáticos.
Algo parecido ocurrió con la conjetura de Kepler, que afirma que la conocida pirámide de naranjas de los mercados es la forma más densa de apilar esferas iguales. Thomas Hales anunció una demostración asistida por computadora en 1998, pero los árbitros no pudieron revisarla completa. Su proyecto Flyspeck terminó en 2014 una demostración totalmente formal, verificada por máquina.
Asistentes de demostración
Programas como Lean, Coq (hoy llamado Rocq) e Isabelle se conocen como asistentes de demostración. El matemático escribe el argumento en un lenguaje preciso, y el programa rechaza cualquier paso que no se siga de los anteriores. En 2022, una comunidad de usuarios de Lean verificó un teorema central y difícil de Peter Scholze y Dustin Clausen, por invitación del propio Scholze. Cada vez más matemáticos formalizan así su trabajo.
Entonces, ¿qué es una demostración?
Una demostración es un argumento que convence a los especialistas más allá de toda duda razonable y que, si hiciera falta, podría desarrollarse en pasos totalmente formales que una máquina puede verificar. Las mejores demostraciones hacen algo más: explican por qué una afirmación es verdadera. Por eso los matemáticos siguen buscando nuevas demostraciones de viejos teoremas, y por eso una conjetura como la de Goldbach, por muy comprobada que esté, todavía espera la suya.
Further readingPara leer más
- Euclid, Elements, Book IX, Proposition 20 (the infinitude of primes).
- Georges Gonthier, “Formal Proof—The Four-Color Theorem,” Notices of the American Mathematical Society 55 (2008).
- Thomas Hales et al., “A Formal Proof of the Kepler Conjecture,” Forum of Mathematics, Pi 5 (2017).
Do you research these questions?¿Investiga usted estas preguntas?
Fundamental Science Journal publishes peer-reviewed research in physics, mathematics, chemistry and logic, in English or Spanish.Fundamental Science Journal publica investigación arbitrada en física, matemática, química y lógica, en inglés o en español.