LÓGICA · Del binario a la prueba automática

Gottfried Wilhelm Leibniz construye la Stepped Reckoner entre 1672 y 1674 en París: primera calculadora mecánica capaz de las cuatro operaciones. En paralelo, formaliza el sistema binario en Explication de l'Arithmétique Binaire (1679). Su motivación es explícita: "Es indigno que hombres excelentes pierdan horas como esclavos en la labor de cálculos." El aparato no es confiable en la práctica, pero la notación binaria que publica es perfecta. Pasarán 168 años antes de que Boole le dé estructura algebraica.

George Boole publica The Mathematical Analysis of Logic (1847) y Laws of Thought (1854) desde Cork (Irlanda). Sin doctorado, enseña en el Queen's College. Formaliza la lógica clásica como un álgebra de dos valores: AND, OR, NOT como operaciones cerradas. La motivación es teológica y filosófica — busca "las leyes del pensamiento" — pero el armazón matemático es ajedrez puro. No hay máquina que lo ejecute. Muere en 1864 a los 49 años sin ver ninguna aplicación técnica.

Gottlob Frege publica Begriffsschrift ("escritura conceptual") en 1879, con 31 años, en Jena. Es la primera notación lógica que incluye cuantificadores (∀, ∃) y permite expresar enunciados sobre objetos y sus propiedades con precisión matemática completa. Boole podía formalizar "A y B implica C"; Frege puede formalizar "para todo x, si x es par entonces x no es primo (salvo el 2)". La notación bidimensional de Begriffsschrift es ilegible — Russell y Peano ignoran el formato pero absorben las ideas. El trabajo directo de Frege influye en Hilbert, en Russell y, a través de ellos, en Gödel y Turing.

David Hilbert plantea el Entscheidungsproblem en 1928: ¿existe un procedimiento mecánico capaz de decidir, para cualquier enunciado matemático, si es verdadero o falso? Kurt Gödel responde en 1931, desde Viena, con dos teoremas de incompletitud: en cualquier sistema formal suficientemente potente, hay verdades que no se pueden probar dentro de ese sistema. El edificio que Hilbert quería construir tiene fisuras estructurales por definición. El resultado de Gödel no destruye las matemáticas, pero traza un perímetro: hay preguntas que ningún axioma resuelve desde dentro.

Alonzo Church publica el cálculo lambda en 1936 en Princeton. Define una notación formal para funciones y su aplicación: cualquier función computable puede expresarse como combinación de abstracciones lambda. Ese mismo año, simultáneamente e independientemente de Turing, demuestra que el Entscheidungsproblem es indecidible. Church y Turing trabajan en el mismo departamento; Turing lee el paper de Church antes de publicar el suyo. La tesis Church-Turing: cualquier función computable por un proceso mecánico es computable por una Máquina de Turing, y también por el cálculo lambda — son equivalentes.

Claude Shannon, con 21 años, escribe su tesis de máster en el MIT en 1937. Título: A Symbolic Analysis of Relay and Switching Circuits. La tesis central: los relés eléctricos se comportan exactamente como los operadores del álgebra de Boole. Un relé abierto = 0, un relé cerrado = 1. AND = relés en serie, OR = relés en paralelo. Llevó 90 años desde Boole (1847) hasta que alguien hiciera esta conexión. Shannon lo vio porque trabajaba simultáneamente con circuitos físicos en Bell Labs y con lógica matemática en sus clases del MIT. La tesis no tiene más de 60 páginas. Es posiblemente la tesis de máster más influyente del siglo XX.

Claude Shannon publica A Mathematical Theory of Communication en julio-octubre de 1948, en el Bell System Technical Journal. Dos artículos en dos entregas. Define el bit como unidad de información, establece la entropía de Shannon como medida de incertidumbre, y prueba los límites teóricos de transmisión sobre cualquier canal con ruido. La Scientific American lo llamará "la Magna Carta de la era de la información". El biólogo James Gleick sostiene que este paper es más importante que el transistor. Sin él no hay compresión de datos, no hay criptografía moderna, no hay codificación de canal, no hay cálculo de capacidad de redes neuronales.

The Univalent Foundations Program — 40 autores reunidos en el Institute for Advanced Study (IAS) de Princeton — publica el HoTT Book en 2013. Vladimir Voevodsky (ganador de la Medalla Fields en 2002, ahora en IAS) aporta el axioma de univalencia: dos estructuras matemáticamente equivalentes son, en este sistema, literalmente idénticas. HoTT conecta la teoría de tipos de Martin-Löf con la topología algebraica. El resultado práctico: un sistema donde las pruebas matemáticas pueden verificarse automáticamente por ordenador. Voevodsky se convierte al HoTT tras encontrar un error en uno de sus propios teoremas que pasó años sin detectarse — la formalización mecánica como corrector de errores humanos.

Leonardo de Moura (Microsoft Research) lanza Lean 4 en 2021: lenguaje de programación y asistente de pruebas simultáneamente. La clave es mathlib: una biblioteca matemática colaborativa mantenida por cientos de matemáticos. En 2022-2023, Peter Scholze (Medalla Fields 2018) pide ayuda para formalizar su "liquid tensor experiment" — una prueba de 100+ páginas que él mismo no está seguro de que sea correcta. La comunidad Lean la formaliza en meses. El ordenador confirma: la prueba es correcta. Herramientas similares: Isabelle, Coq, Agda. Lean domina por su ergonomía y por mathlib.

DeepMind publica AlphaProof y AlphaGeometry en julio de 2024. En la IMO 2024 (International Mathematical Olympiad), el sistema resuelve 4 de 6 problemas, incluyendo dos de los tres más difíciles. Medalla de plata equivalente — el primer resultado de plata para un sistema automatizado en la olimpiada más exigente del mundo. AlphaProof combina un modelo de lenguaje con el asistente de pruebas Lean: el LLM propone pasos de prueba, Lean verifica cada uno formalmente. AlphaGeometry usa un sistema diferente (cálculo simbólico + LLM) para los problemas de geometría.