El paraíso de Hilbert: Demostración automática en matemáticas
José A. Alonso

Índice

1. El paraíso de Hilbert

  • Desde principios del siglo XX se sabe que la mayor parte de las matemáticas ordinarias son, en principio, formalizables.
  • Con la ayuda de los sistemas de razonamiento, las matemáticas son formalizables en la práctica.
  • La tecnología nos permite representar definiciones, enunciados y pruebas en formatos digitales, con todos los detalle y precisión.
  • Esto es coherente con los objetivos tradicionales de rigor y precisión en matemáticas.

2. Necesidad de verificación formal de demostraciones en matemáticas

3. Formalización de los 100 principales teoremas

  • The hundred greatest theorems.
    • Lista con motivo del año de las matemáticas.
  • Formalizing 100 theorems.
    • The top 100 theorems in Isabelle.

      • Teorema de Cantor: Cantors_paradox. 

        theorem Cantors_paradox: "∄f. f ` A = Pow A"
proof
  assume "∃f. f ` A = Pow A"
  then obtain f where f: "f ` A = Pow A" ..
  let ?X = "{a ∈ A. a ∉ f a}"
  have "?X ∈ Pow A" by blast
  then have "?X ∈ f ` A" by (simp only: f)
  then obtain x where "x ∈ A" and "f x = ?X" by blast
  then show False by blast
qed
    • 100 theorems in Lean.

      • Infinitud de los números primos: exists_infinite_primes. 

        theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Prime p :=
  let p := minFac (n ! + 1)
  have f1 : n ! + 1 ≠ 1 := ne_of_gt <| succ_lt_succ <| factorial_pos _
  have pp : Prime p := minFac_prime f1
  have np : n ≤ p :=
    le_of_not_ge fun h =>
      have h₁ : p ∣ n ! := dvd_factorial (minFac_pos _) h
      have h₂ : p ∣ 1 := (Nat.dvd_add_iff_right h₁).2 (minFac_dvd _)
      pp.not_dvd_one h₂
  ⟨p, np, pp⟩

4. Sistemas de razonamiento con grandes librerías matemáticas

Sistema Fundamento
ACL2 Aritmética primitiva recursiva
Agda Teoría constructiva de tipos dependientes
Coq Teoría constructiva de tipos dependientes
HOL Light Teoría de tipos simples
Isabelle Teoría de tipos simples
Lean Teoría de tipos dependientes
Metamath Teoría de conjuntos
Mizar Teoría de conjuntos
PVS Teoría clásica de tipos dependientes

5. Formalizaciones de teoremas famosos

5.1. Primer teorema de incompletitud de Gödel (1986)

  • En 1931, Gödel demostró el primer teorema de incompletitud:

    Cualquier sistema formal consistente \(F\) en el cual se pueda desarrollar una cierta cantidad de aritmética elemental es incompleto; es decir, hay afirmaciones del lenguaje de \(F\) que no pueden ser probadas ni refutadas en \(F\).

  • En 1986, Natarajan Shankar lo formalizó en Nqthm (o el demostrador de Boyer-Moore).
  • Plan de la prueba:
    • Construir la teoría Z2 de los conjuntos hereditariamente finitos; es decir, conjuntos que son finitos y todos sus elementos, elementos de elementos, etc., también son finitos.
    • Enumerar las pruebas de Z2 usando una aplicación inyectiva de las pruebas de Z2 a los números naturales.
    • Definir un predicado Lisp que busque la primera prueba o refutación de la fórmula dada en esta enumeración de pruebas, y devuelva T o F. Sea este "verificador de teoremas" de la forma (THEOREM X), donde X es la fórmula dada.
    • Construir una sentencia U que afirme que "(THEOREM u) = F", donde u es la representación Lisp de U.
    • Demostrar que si U es demostrable o refutable en Z2, entonces es tanto demostrable como refutable.

  • La demostración tiene sobre 2.000 definiciones y lemas. 

    (PROVE-LEMMA INCOMPLETENESS-THEOREM
             (REWRITE)
             (AND (FORMULA (UNDECIDABLE-SENTENCE GIVEN) (THM-SYMBS))
                  (NOT (MEMBER VAR (COLLECT-FREE (UNDECIDABLE-SENTENCE GIVEN) 0)))
                  (IMPLIES (OR (PROVES PF
                                       (UNDECIDABLE-SENTENCE GIVEN)
                                       GIVEN
                                       (THM-DEFNS)
                                       (THM-SYMBS))
                               (PROVES PF
                                       (F-NOT (UNDECIDABLE-SENTENCE GIVEN))
                                       GIVEN
                                       (THM-DEFNS)
                                       (THM-SYMBS)))
                           (OR (AND (PROVES (SOME-PROOF1 GIVEN PF)
                                            (UNDECIDABLE-SENTENCE GIVEN)
                                            GIVEN
                                            (THM-DEFNS)
                                            (THM-SYMBS))
                                    (PROVES (SOME-DISPROOF1 GIVEN PF)
                                            (F-NOT (UNDECIDABLE-SENTENCE GIVEN))
                                            GIVEN
                                            (THM-DEFNS)
                                            (THM-SYMBS)))
                               (AND (PROVES (SOME-PROOF2 GIVEN PF)
                                            (UNDECIDABLE-SENTENCE GIVEN)
                                            GIVEN
                                            (THM-DEFNS)
                                            (THM-SYMBS))
                                    (PROVES (SOME-DISPROOF2 GIVEN PF)
                                            (F-NOT (UNDECIDABLE-SENTENCE GIVEN))
                                            GIVEN
                                            (THM-DEFNS)
                                            (THM-SYMBS))))))
             ((USE (INCOMPLETENESS-MAIN-PART)) (DISABLE A-UNDEC
                                            SUBST
                                            G-ISTHMN
                                            G-PROVESN-GCODE
                                            INV-CODE-DECIPHER
                                            FIND-PROOFN
                                            UNDEC-COUNT-LESSP
                                            INV-CODE-DECIPHER-NUMCODE
                                            INCOMPLETENESS-MAIN-PART
                                            EXP-COUNT)))
  • Las definiciones y lemas se construyeron mediante un proceso de interacción con Nqthm, que fue capaz de demostrar automáticamente un gran número de lemas no triviales.
  • La principal dificultad a la hora de verificar estas pruebas fue el hecho de que tuvieron que ser construidas casi por completo desde cero.
  • Excluido el tiempo dedicado a pensar, planificar y escribir sobre la prueba, la verificación del teorema de incompletitud le ocupó unos dieciocho meses de esfuerzo con Nqthm.
  • Más información en Metamathematics, machines and Gödel's proof

5.2. Conjetura de Robbins (1996)

  • Noticias en la prensa:

  • En 1933, E. V. Huntington presentó los siguientes axiomas para las álgebras de Boole:

    x + y = y + x. [conmutativa]
    (x + y) + z = x + (y + z). [asociativa]
    n(n(x) + y) + n(n(x) + n(y)) = x. [ecuación de Huntington ]

  • Poco después, Herbert Robbins conjeturó que la ecuación de Huntington puede sustituirse por otra más sencilla:

    n(n(x + y) + n(x + n(y))) = x. [ecuación de Robbins]
  • Robbins y Huntington no pudieron demostrarlo, y el problema fue estudiado más tarde por Tarski y sus alumnos.
  • Las álgebras que satisfacen la conmutatividad, la asociatividad y la ecuación de Robbins pasaron a denominarse álgebras de Robbins.
  • Está claro que toda álgebra booleana es un álgebra de Robbins, así que el problema interesante era si toda álgebra de Robbins es booleana. En otras palabras, ¿puede derivarse la ecuación de Huntington a partir de la conmutatividad, la asociatividad y la ecuación de Robbins?

  • En 1992, Winker demostró que cada uno de los axiomas siguientes es condición suficiente para que un álgebra de Robbins satisfaga la ecuación de Huntington y, por tanto, sea un álgebra booleana.

    exists C exists D, C+D=C [primera condición de Winker]
    exists C exists D, n(C+D)=n(C) [segunda condición de Winker]
  • En 1996, McCune con EQP demostró que las álgebras de Robbins cumplen las condiciones de Winker. Por tanto, las álgebras de Robbins son álgebras de Boole.
  • La prueba consta de

    • Fichero de entrada. 

      assoc_comm(+).
op(500, xfy, +).

list(sos).
n(n(n(y)+x)+n(x+y))=x.  % Robbins axiom
end_of_list.

list(passive).
x+y != x.         % denial of Winker condition 1
n(x+y) != n(x).   % denial of Winker condition 2
end_of_list.

    • Prueba obtenida. 

      ----- EQP 0.9, June 1996 -----
The job began on eyas09.mcs.anl.gov, Wed Oct  2 12:25:37 1996
UNIT CONFLICT from 17666 and 2 at 678232.20 seconds.

---------------- PROOF ----------------

2 (wt=7) [] -(n(x + y) = n(x)).
3 (wt=13) [] n(n(n(x) + y) + n(x + y)) = y.
5 (wt=18) [para(3,3)] n(n(n(x + y) + n(x) + y) + y) = n(x + y).
6 (wt=19) [para(3,3)] n(n(n(n(x) + y) + x + y) + y) = n(n(x) + y).
24 (wt=21) [para(6,3)] n(n(n(n(x) + y) + x + y + y) + n(n(x) + y)) = y.
47 (wt=29) [para(24,3)] n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + z) + n(y + z)) = z.
48 (wt=27) [para(24,3)] n(n(n(n(x) + y) + n(n(x) + y) + x + y + y) + y) = n(n(x) + y).
146 (wt=29) [para(48,3)] n(n(n(n(x) + y) + n(n(x) + y) + x + y + y + y) + n(n(x) + y)) = y.
250 (wt=34) [para(47,3)] n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + n(y + z) + z) + z) = n(y + z).
996 (wt=42) [para(250,3)] n(n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + n(y + z) + z) + z + u) + n(n(y + z) + u)) = u.
16379 (wt=21) [para(5,996),demod([3])] n(n(n(n(x) + x) + x + x + x) + x) = n(n(x) + x).
16387 (wt=29) [para(16379,3)] n(n(n(n(n(x) + x) + x + x + x) + x + y) + n(n(n(x) + x) + y)) = y.
16388 (wt=23) [para(16379,3)] n(n(n(n(x) + x) + x + x + x + x) + n(n(x) + x)) = x.
16393 (wt=29) [para(16388,3)] n(n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) + x) = n(n(x) + x).
16426 (wt=37) [para(16393,3)] n(n(n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) + x + y) + n(n(n(x) + x) + y)) = y.
17547 (wt=60) [para(146,16387)] n(n(n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) + n(n(n(x) + x) + x + x + x) + x) + x) = n(n(n(x) + x) + n(n(x) + x) + x + x + x + x).
17666 (wt=33) [para(24,16426),demod([17547])] n(n(n(x) + x) + n(n(x) + x) + x + x + x + x) = n(n(n(x) + x) + x + x + x).

------------ end of proof -------------
  • La búsqueda duró unos 8 días en un procesador RS/6000 y utilizó unos 30 megabytes de memoria.
  • Más información en Robbins algebras are boolean ~ William McCune.

5.3. Teorema de los números primos (2004)

  • El teorema de los números primos afirma que si \(π(x)\) es la cantidad de primos hasta x; es decir, \[π(x) = |\{ p | \text{primo}(p) ∧ 0 ≤ p ≤ x\}|,\] entonces \[π(x) ∼ \dfrac{x}{\ln(x)}\] o, en otras palabras, \[\lim_{x \to \infty}\dfrac{π(x)\ln(x)}{x} = 1\]
  • En 1792, Gauss lo conjeturó.
  • En 1798, Legendre lo conjeturó indicando que π(x) parecía tener la forma a/(A ln(a) + B), donde A y B son constantes no especificadas.
  • En 1896, Hadamard y de la Vallée Poussin lo demuestra usando análisis complejo.
  • En 1948, Selberg y Erdös lo demuestra sin usar análisis complejo.
  • En 2004, Avigad la formalizó en Isabelle basándose en la prueba de Selberg y Erdös.

    • La prueba es 

      lemma PrimeNumberTheorem: "(%x. pi x * ln (real x) / (real x)) ----> 1";
  apply (rule theta_limit_imp_pi_limit);
  apply (rule PrimeNumberTheorem2);
done;
  • Más información en A formally verified proof of the prime number theorem.

5.4. Teorema de los cuatro colores (2004)

  • El teorema de los cuatro colores (T4C) establece que las regiones de cualquier mapa plano simple pueden ser coloreadas con sólo cuatro colores, de tal manera que dos regiones adyacentes cualesquiera tengan colores diferentes.
  • En 1852, Francis Guthrie lo conjeturó.
  • En 1860, De Morgan lo planteó.
  • En 1879, Alfred Kempe publicó una supuesta prueba del T4C, cuya validez como prueba fue aceptada durante once años antes de ser refutada por Percy Heawood.
  • En 1889, Peter Guthrie Tait presentó otra prueba incorrecta del T4C que Julius Petersen refutó en 1891.
  • En 1976, Kenneth Appel y Wolfgang Haken demostraron el T4C.
    • La demostración tiene 139 páginas.
    • Usa de largos cálculos informáticos.
  • En 1995, Robertson, Sanders, Seymour, and Thomas simplificaron la demostración del T4C.
  • En 2005. Gonthier formalizó en Coq la prueba del T4C.
  • Demostración en Coq:

    • Prueba en fourcolor.v 

      Variable Rmodel : Real.model.
Let R := Real.model_structure Rmodel.
Implicit Type m : map R.

Theorem four_color_finite m : finite_simple_map m -> colorable_with 4 m.
Proof.
intros fin_m.
pose proof (discretize.discretize_to_hypermap fin_m) as [G planarG colG].
exact (colG (combinatorial4ct.four_color_hypermap planarG)).
Qed.

      con 60.000 líneas de código en el proyecto.

    • Se define real_model como un tipo de objetos con operaciones que satisfacen un conjunto bastante estándar de axiomas para los números reales.
    • Se demuestra el T4C para un real_model.
    • También se proporciona una construcción explícita de un modelo (archivo dedekind.v) y una prueba de que este modelo es único salvo isomorfismos (archivo realcategorical.v).
    • Aunque el enunciado del T4C utiliza nociones de análisis, el T4C es esencialmente un resultado de combinatoria: la esencia del teorema es un enunciado de propiedades de ciertos ordenamientos finitos de objetos finitos.
    • Colorear un mapa es equivalente a colorear el grafo obtenido tomando las regiones del mapa como nodos y enlazando cada par de regiones adyacentes.

  • Comentarios de Gonthier:

    "El aspecto más prometedor de una prueba formal no es simplemente un método para estar absolutamente seguros de que no nos hemos equivocado en una demostración, sino también una herramienta que nos muestra y nos obliga a entender por qué funciona una demostración."

  • Más información en

5.5. Teorema de Dirichlet sobre los primos en progresión aritmética (2009)

  • El teorema de Dirichlet afirma que para todos los pares de enteros positivos \(k\) y \(d\) que son coprimos, existen infinitos primos \(p\) tales que \(p ≡ k(\text{mod } d)\); es decir, que la progresión aritmética infinita \[k, k+d, k+2d, k+3d,\dots\] contiene infinitos primos.
  • En 1808, Legendre publicó un intento de demostración.
  • En 1859, Dupré señaló que uno de los lemas utilizados por Legendre es falso.
  • En 1837, Dirichlet presentó una demostración completa.

  • En 2009, Harrison la formalizó en HOL Light. 

    (`!d k. 1 <= d /\ coprime(k,d)
       ==> INFINITE {p | prime p /\ (p == k) (mod d)}
  • Más información en A formalized proof of Dirichlet’s theorem on primes in arithmetic progression.

5.6. Teorema de Feit-Thompson (2012)

  • El teorema de Feit-Thompson establece que todo grupo finito de orden impar es resoluble .
  • En 1963, Walter Feit y John Griggs Thompson lo demostraron.
  • Su demostración ocupa 255 páginas.
  • En 2012, Gonthier y sus colaboradores lo formalizaron en Coq

  • La demostración formalizada es constructiva 

    Theorem stripped_Odd_Order T mul one inv (G : T -> Type) (n : natural) :
    group_axioms T mul one inv -> group T mul one inv G ->
    finite_of_order T G n -> odd n ->
  solvable_group T mul one inv G.
Proof. exact (InternalSkepticOddOrderProof.main T mul one inv G n). Qed.

    y contiene, aproximadamente, 170.000 líneas de código, 15.000 definiciones y 4.200 teoremas.

  • El desarrollo incluye librerías para grupos finitos, álgebra lineal y teoría de la representación.
  • Más información en A Machine-checked proof of the odd order theorem.

5.7. Conjetura de Kepler (2014)

  • La conjetura de Kepler afirma que si apilamos esferas iguales, la densidad máxima se alcanza con una apilamiento piramidal de caras centradas. Esta densidad es aproximadamente del 74%.
  • En 1611, Johannes Kepler conjeturó la optimalidad.
  • En 1993, Hsiang publicó una prueba incompleta.
  • En 1998, Thomas Hales anunció una prueba de la conjetura de Kepler.
  • La prueba tenía de 250 páginas de notas y 3 gigabytes de programas informáticos, datos y resultados.
  • El proceso de revisión en los Annals fue insatisfactorio.
  • En 2003, Hales inicia el proyecto Flyspeck para verificar los resultados formalmente.
  • En 2014, se publicó un anuncio con la finalización del proyecto.
  • El proyecto se encuentra en GitHub.

    • La prueba se encuentra en the_kepler_conjecture.hl 

      let kepler_conjecture_with_assumptions_and_archive = prove_by_refinement(
  `import_tame_classification /\
    linear_programming_results /\
    the_nonlinear_inequalities
    ==> the_kepler_conjecture
    `,
  (* {{{ proof *)
  [
  REPEAT WEAKER_STRIP_TAC;
  INTRO_TAC kepler_conjecture_with_assumptions [`tame_archive_lists`];
  DISCH_THEN MATCH_MP_TAC;
  ASM_REWRITE_TAC[good_linear_programming_results;GSYM linear_programming_results];
  ASM_REWRITE_TAC[GSYM import_tame_classification_tame];
  MP_TAC Good_list_archive.good_list_archive;
  BY(REWRITE_TAC[Good_list_archive.good_list_archive])
  ]);;
  • La verificación de varios cientos de desigualdades no lineales requirió aproximadamente 5.000 horas de procesador en la nube de Microsoft Azure.
  • Más información en A formal proof of the Kepler conjecture.

5.8. Otros teoremas famosos formalizados

6. Formalización de teoremas recientes

6.1. LTE (Liquid Tensor Experiment) (2021)

  • Noticias en la prensa:
  • Peter Scholze, especialista en teoría de números y medalla Field 2018, creó junto con Dustin Clausen un proyecto bautizado como matemáticas condensadas en el que prometen aportar nuevas perspectivas y conexiones entre la geometría, el análisis funcional y los números p-ádicos.
  • El 5 de diciembre de 2020, Peter Scholze desafió a cualquiera a verificar formalmente uno de sus teoremas fundamentales de las matemáticas condensadas (concretamente, de Lectures on analytic geometry) de cuya prueba no estaban seguros.
  • El nombre del desafío era Liquid Tensor Experiment (LTE) y era un homenaje a Liquid Tension Experiment, una banda de rock progresivo a la que Scholze le tiene cariño.
  • El LTE es un teorema complejo sobre objetos matemáticos complejos.
    • Muchas de las anteriores formalizaciones son teoremas complejos sobre objetos simples.

  • El teorema a demostrar en el LTE es

    Sean \(0 < p' < p ≤ 1\) números reales, \(S\) un conjunto profinito y \(\mathcal{M}_{p′}(S)\) el espacio de las p'-medidas sobre \(S\) y \(V\) un p-espacio de Banach. Entonces, \[\text{Ext}^i(\mathcal{M}_{p'}(S),V) = 0\] para todo \(i ≥ 1\).

  • Su formulación en Lean es 

    variables (p' p : ℝ ≥ 0) [fact (0 < p')] [fact (p' < p)] [fact (p ≤ 1)]

theorem liquid_tensor_experiment
  (S : Profinite) (V : pBanach p) :
  ∀ i > 0, Ext i (ℳ_{p'} S) V ≅ 0 :=
-- la demostración ...

    que se encuentra en challenge.lean del repositorio lean-liquid.

  • Johan Commelin lideró la respuesta de la comunidad Lean.

  • El 5 de junio de 2021, se anunció la formalización dela parte de la prueba en la que Scholze tenía más dudas.

    "Hace exactamente medio año escribí en el blog Liquid Tensor Experiment desafiando la formalización de un difícil teorema fundamental de mimis apuntes de Geometría Analítica en colaboración con Dustin Clausen. Si bien este desafío no se ha completado todavía, estoy emocionado de anunciar que el Experimento ha verificado la toda la parte del argumento de la que no estaba seguro. Me parece que los asistentes de prueba interactivos están ahora al nivel que en un periodo de tiempo muy razonable puedan verificar formalmente investigaciones originales difíciles".

  • El LTE es un modelo de colaboración digital.
    • La formalización se mantuvo en un repositorio compartido en línea.
    • Los participantes siguieron un plan informal con enlaces al repositorio.
    • Los participantes estaban en contacto permanente en Zulip.
    • Lean se aseguró de que las piezas encajaran.
  • La razón por la que tomó tanto tiempo la prueba de LTE fue que la comunidad Lean tuvo que construir una teoría funcional de categorías abelianas, cohomología, functores derivados, etc., como requisitos previos.
  • El factor de Bruijn de una formalización es la relación entre el número de líneas de código informático y el número de líneas de matemáticas humanas.
    • Un objetivo en el área de la formalización informática es reducir el factor de Bruijn a 1.
    • En el caso del LTE se utilizaron alrededor de 30.000 líneas de código para formalizar la prueba de cinco páginas del Teorema 9.4, y alrededor de 60.000 líneas de código se utilizaron para formalizar las cinco páginas del teorema final.
    • Si los conceptos básicos requeridos (categorías abelianas, etc.) ya hubieran estado en la biblioteca de matemáticas de Lean, la formalización habría llevado mucho menos tiempo y muchas menos líneas.
  • Lo que probablemente causó el interés del LTE fue que una de las motivaciones de Scholze para alentar una formalización era que no estaba convencido de que la demostración del teorema 9.4 fuese correcta.
  • Más información

6.2. Fracciones unitarias (2021)

6.3. La conjetura polinómica de Freiman-Ruzsa (2023)

  • La conjetura polinómica de Freiman-Ruzsa (PFR) afirma que

    Si \(A\) es un subconjunto no vacío de \(\mathbb{F}^n_2\) tal que \(|A+A|≤K|A|\), entonces \(A\) puede ser cubierto por a lo sumo \(2K^{12}\) cosets de un subespacio \(H\) de \(\mathbb{F}^n_2\) de cardinalidad a lo sumo \(|A|\).

  • El 9 de noviembre de 2023, W. T. Gowers, Ben Green, Freddie Manners y Terence Tao publicaron su demostración: On a conjecture of Marton.
  • El 13 de noviembre de 2023, Terry Tao propuso su formalización en Lean4: On a conjecture of Marton.
  • El 5 de diciembre de 2023, Terry Tao comunicó que se había completado el PFR (anuncio en Zulip).

  • La demostración se encuentra en PFR/Main.lean 

    theorem PFR_conjecture (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * Nat.card A) :
     ∃ (H : AddSubgroup G) (c : Set G),
      Nat.card c < 2 * K ^ 12 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
  • El proyecto se desarrolló en GitHub y Zulip.
  • La página del proyecto PFR se encuentra en este enlace.
  • Más información en Formalizing the proof of PFR in Lean4 using Blueprint: a short tour

Autor: José A. Alonso

Created: 2024-01-14 dom 09:51

Validate