Lawrence C Paulson abre su crónica rechazando la tesis, defendida por Peter Thiel y varios influencers de YouTube, de que la ciencia lleva 50 años estancada. Su contraejemplo es su propio campo: los asistentes de demostración al estilo LCF.

La historia comienza en 1975 con Edinburgh LCF, el sistema de Robin Milner presentado en la conferencia de Arc-et-Senans. Estableció el patrón aún vigente: un núcleo de demostración encapsulado en un tipo abstracto en ML, de modo que solo las reglas de inferencia pueden producir valores de tipo thm. A ello se sumaron reglas de deducción natural, demostración dirigida por objetivos con tácticas y combinadores de tácticas, y teorías estructuradas. La lógica era mínima: cuantificación universal, conjunción e implicación, sin números negativos ni notación decimal. Paulson se unió a Milner y Mike Gordon en Cambridge en 1982, transformó el sistema en Cambridge LCF y verificó el algoritmo de unificación en 36 inducciones.

De 1985 a 1995, el compilador ML más rápido de Cambridge LCF alimentó el HOL88 de Gordon, y la verificación de hardware se hizo realidad: se verificaron diseños de chips de producción mientras la verificación de software se estancaba. El desarrollo de Isabelle comenzó en 1986, escrito en Standard ML desde el inicio. Surgió el cálculo de construcciones inductivas, el formalismo detrás de los actuales Rocq y Lean. Isabelle/HOL apareció por primera vez en 1991, obra principal de Tobias Nipkow.

El bug FDIV del Pentium en 1994, cuya retirada costó a Intel casi 500 millones de dólares, llevó a John Harrison a la verificación de aritmética de coma flotante. Su tesis de 1996 formalizó el análisis real en HOL: espacios métricos, límites, diferenciación, integración y demostraciones de coma flotante según la norma IEEE. La automatización mejoró con el demostrador Metis de Hurd y el simplificador de Isabelle. Proof General dio a varios sistemas una interfaz Emacs común.

En 2005 el campo tenía resultados emblemáticos: la demostración en Coq del teorema de los cuatro colores de Gonthier, la formalización del teorema de los números primos de Avigad en Isabelle, y la verificación del procesador ARM6 por Gordon, Birtwistle y Fox. Isabelle ganó el lenguaje de demostración Isar, clases de tipos, buscadores de contraejemplos y generación de código.

La década siguiente trajo seL4, el primer kernel de sistema operativo formalmente verificado, hoy respaldado por un millón de líneas de demostraciones en Isabelle/HOL. CompCert entregó un compilador verificado para un amplio subconjunto de C, y CakeML cerró el círculo del bootstrap con un compilador verificado hasta el lenguaje ensamblador. En matemáticas siguieron el segundo teorema de incompletitud de Gödel, el teorema central del límite, el proyecto Flyspeck y el teorema del orden impar.

La última década irrumpió en las matemáticas convencionales, impulsada por la promoción de Lean de Kevin Buzzard. En 2022, la asistencia automática confirmó por primera vez matemáticas nuevas que un medallista Fields había puesto en duda. En la industria, Isabelle contribuyó a la arquitectura de capacidades CHERI y a la especificación de WebAssembly, donde Conrad Watt encontró problemas corregidos a tiempo. El 4 de diciembre de 2025, AWS anunció el Nitro Isolation Engine para Graviton5: un kernel de separación escrito en Rust con 260.000 líneas de demostraciones en Isabelle/HOL que cubren confidencialidad e integridad, un proyecto en el que el propio Paulson participa.

Su comparación final: los smartphones fueron revolucionarios y hoy ya no congregan multitudes. La verificación formal aún no es algo ordinario, pero va en esa dirección.