Menu Close

Autor: José A. Alonso

Reseña: Computational logic: its origins and applications

José A. Alonso--

Lawrence C. Paulson publicó en 1998 el artículo Computational logic: its origins and applications cuyo resumen es

Computational logic is the use of computers to establish facts in a logical formalism. Originating in nineteenth century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the ‘logic for computable functions (LCF) approach’ pioneered by Robin Milner, where proofs can be constructed interactively or with the help of users’ code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.

y su contenido es

  1. Introduction.
  2. A brief history of formal logic.
  3. Mechanized logic: the LCF tradition.
  4. A new theorem-proving architecture: Isabelle.
  5. Formalizing mathematics.
  6. Obstacles to formalizing mathematics.
  7. The way forward.
Seguir leyendo →

Reseña: Windmills of the minds: an algorithm for Fermat’s two squares theorem

José A. Alonso--

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de números titulado Windmills of the minds: an algorithm for Fermat’s two squares theorem.

Sus autor es Hing Lun Chan (de la Australian National University en Canberra, Australia).

Su resumen es

The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence “proof from the Book“. Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a finite set, especially the parity of the number of fixed points in the involutions. Starting as an existence proof that is non-constructive, there is an ingenious way to turn it into a constructive one. This gives an algorithm to compute the two squares by iterating the two involutions alternatively from a known fixed point.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

El código de las correspondientes teorías se encuentra aquí.

Seguir leyendo →

Reseña: Formalizing ordinal partition relations using Isabelle/HOL

José A. Alonso--

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre combinatoria titulado Formalizing ordinal partition relations using Isabelle/HOL.

Sus autores son

Su resumen es

This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all m ∈ ℕ, ω^ω → (ω^ω,m). This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.

El trabajo se ha publicado en Experimental Mathematics.

El código de las correspondientes teorías se encuentra aquí.

Seguir leyendo →

Reseña: A machine-checked direct proof of the Steiner-Lehmus theorem

José A. Alonso--

Se ha publicado un artículo de razonamiento formalizado en Nuprl sobre geometría titulado A machine-checked direct proof of the Steiner-Lehmus theorem.

Su autora es Ariel Kellison (de Cornell University).

Su resumen es

A direct proof of the Steiner-Lehmus theorem has eluded geometers for over 170 years. The challenge has been that a proof is only considered direct if it does not rely on reductio ad absurdum. Thus, any proof that claims to be direct must show, going back to the axioms, that all of the auxiliary theorems used are also proved directly. In this paper, we give a proof of the Steiner-Lehmus theorem that is guaranteed to be direct. The evidence for this claim is derived from our methodology: we have formalized a constructive axiom set for Euclidean plane geometry in a proof assistant that implements a constructive logic and have built the proof of the Steiner-Lehmus theorem on this constructive foundation.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

El código de las correspondientes teorías se encuentra aquí.

Seguir leyendo →

Reseña: Completeness theorems for first-order logic analysed in constructive type theory

José A. Alonso--

Se ha publicado un artículo de razonamiento formalizado en Coq sobre lógica titulado Completeness theorems for first-order logic analysed in constructive type theory.

Sus autores son

Su resumen es

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak König’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

El trabajo se ha presentado en el Logical Foundations of Computer Science (LFCS 2020) y publicado en el Journal of Logic and Computation.

El código de las correspondientes teorías se encuentra aquí.

Seguir leyendo →

Reseña: Formalising Lie algebras in Lean

José A. Alonso--

Se ha publicado un artículo de razonamiento formalizado en Lean sobre álgebras de Lie titulado Formalising Lie algebras.

Su autor es Oliver Nash (Imperial College in London, U.K.).

Su resumen es

Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean’s Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed; the intention is that the overall themes will be accessible even to readers unfamiliar with Lie theory.

Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero.

In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.

El código de las correspondientes teorías se encuentra aquí.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

Seguir leyendo →

Reseña: Why formalize mathematics?

José A. Alonso--

Se ha publicado un artículo sobre razonamiento formalizado titulado Why formalize mathematics?

Su autor es Patrick Massot (del Laboratoire de mathématiques d’Orsay en la Université Paris-Saclay, Orsay, Francia).

Su resumen es

We’ve been doing mathematics for more than two thousand years with remarkable success. Hence it is natural to be puzzled by people investing a lot of time and energy into a very new and weird way of doing mathematics: the formalized way where human beings explain mathematical definitions and proofs to computers. Beyond puzzlement, some people are wary. They think the traditional way may disappear, or maybe even mathematicians may disappear, being replaced by AI agents. These events are extremely unlikely and they are not the goals of the mathematical formalization community. We want to add to our tool set, without losing anything we already have. In this text I’ll explain what we want to add, distinguishing what already partially exists and what is currently science fiction. Examples will use Lean, a proof assistant software developed mostly by Leonardo de Moura at Microsoft Research, but everything I’ll write applies to other proof assistants such as Coq or Isabelle.

El trabajo es una ampliación de la charla con el mismo título impartida el 27 de octubre de 2021 en el seminario New Technologies in Mathematics Seminar Series en Harvard. El vídeo de la charla se encuentra en este enlace.

Finalmente, a continuación se muestra un resumen más detallado de su contenido.

1. Verificar demostraciones

  • La ventaja más evidente de las matemáticas formalizadas es la certeza de que una prueba es correcta cuando ha sido comprobada por un ordenador.
  • La verificación por el ordenador garantiza la integridad y la consistencia a todas las escalas.
    • La consistencia a pequeña escala significa que no hay ningún caso límite olvidado (como el conjunto vacío o el único número primo par).
    • La exhaustividad consiste en asegurarse de que no hay afirmaciones implícitas erróneas.
    • La consistencia a mediana escala significa que no dejan de ser correctos los lemas cuando modificamos definiciones.
    • La consistencia a gran escala significa que no permitimos que se produzcan malentendidos al utilizar un teorema de un documento que tenía una suposición o notación ligeramente diferente.
  • La tecnología actual no permite esperar que pronto tengamos pruebas formales de cualquier artículo publicado porque:
    • La formalización lleva demasiado tiempo por ahora.
    • No tenemos suficiente matemática formalizada sobre la que basarnos.
  • Alternativas posibles:
    • Podemos concentrarnos en partes de teoremas grandes, como en el Liquid tensor experiment.
    • Verificación de pruebas demasiados grandes para el cerebro humano, como en el teorema de los cuatros colores o en la conjetura de Kepler.

2. Explicar y aprender

  • Al escribir textos matemáticos hay que elegir los conocimientos previos asumidos y seleccionar un nivel de detalle.
  • La aplicación más prometedora de las matemáticas formalizadas es el sueño de producir documentos matemáticos que permitan a los lectores elegir dinámicamente el nivel de detalle y el conocimiento usado.
  • Una vez que se entiende una afirmación, se puede pasar a su demostración.
    • La capacidad informática más importante es la visualización del “estado táctico”, que es una lista de todos los objetos y supuestos que son relevantes en ese momento y el objetivo actual de la prueba.
    • Esta información cambia en cada paso de la prueba.
  • La idea es tener un documento progresivo en el que los lectores puedan elegir dinámicamente dónde pedir los detalles cuando los necesiten.
  • Actualmente no tenemos una forma muy agradable de presentar esta información, pero esperamos tenerla en un par de años como máximo.

3. Enseñar

  • Hay que enseñar a concebir y escribir pruebas.
  • Muy a menudo, esto se enseña sólo indirectamente: se pretende que los alumnos aprendan por imitación.
  • Enseñar utilizando un asistente de pruebas tiene el coste obvio de poner una barrera tecnológica a la entrada (aprender sintaxis y navegar por el software). Pero también tiene grandes ventajas.
    • Una ventaja es el estado táctico que se muestra de forma interactiva durante la escritura de pruebas.
    • La obligación establecer formalmente el enunciado y separarlo de la demostración.
  • Ejemplo de demostración en Lean literario: 
    example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ)
  (hu : sequence_tendsto u x₀) (hf : continuous_function_at f x₀) :
sequence_tendsto (f ∘ u) (f x₀) :=
begin
  Let's prove that ∀ ε > 0, ∃ N, ∀ n ≥ N, |f (u n) - f x₀| ≤ ε,
  Fix ε > 0,
  By hf applied to ε using ε_pos we obtain δ such that
    (δ_pos : δ > 0) (Hf : ∀ (x : ℝ), |x - x₀| ≤ δ → |f x - f x₀| ≤ ε),
  By hu applied to δ using δ_pos we obtain N such that
    Hu : ∀ n ≥ N, |u n - x₀| ≤ δ,
  Let's prove that N works : ∀ n ≥ N, |f (u n) - f x₀| ≤ ε,
  Fix n ≥ N,
  By Hf applied to u n it suffices to prove |u n - x₀| ≤ δ,
  This is Hu applied to n using n_ge
end
  • Otra ventaja del uso de los asistentes de pruebas es que los alumnos pueden percibir mucho mejor la alternancia entre las fases en las que la estructura del objetivo dicta el siguiente movimiento y las fases en las que se requiere cierta iniciativa.

4. Crear nuevas matemáticas

  • El ordenador puede
    • Volver a comprobar continuamente todo en cada cambio de definición o enunciado de lema, marcando (casi) instantáneamente lo que hay que modificar.
    • Ayudar a la limpieza, por ejemplo, marcando los supuestos no utilizados.
    • Aclarar qué lemas dependen de otros lemas y definiciones.
    • Demostrar automáticamente pruebas pasos rutinarios o al menos sugerir un paso siguiente.
  • Formalizar mientras se crea es actualmente una enorme ralentización, incluso para los usuarios experimentados. La esperanza es que la tecnología mejore para que la formalización consuma mucho menos tiempo. Aquí puede ayudar alguna forma de inteligencia artificial.
  • Otro sueño que necesita de la IA es un buen motor de búsqueda de enunciados matemáticos.
  • La principal ayuda a la creación puede ser más indirecta. Las matemáticas formalizadas requieren un pensamiento claro.
  • Las matemáticas formalizadas fomentan, o incluso a veces exigen, abstracciones poderosas.

5. Colaborar y divertirse

  • Las matemáticas formalizadas aportan mucha diversión. Parte de esta diversión proviene del aspecto de “videojuego” de los asistentes de pruebas. Pero la verdadera diversión proviene de la colaboración.
Seguir leyendo →

Reseña: What is the point of computers? A question for pure mathematicians

José A. Alonso--

Se ha publicado un artículo sobe razonamiento formalizado titulado What is the point of computers? A question for pure mathematicians.

Su autor es Kevin Buzzard (Imperial College in London, U.K.).

Su resumen es

We discuss the idea that computers might soon help pure mathematicians to prove theorems in areas where they have not previously been useful.

El trabajo se presentará en julio de 2022 como una conferencia invitada en el ICM 2022.

Finalmente, se muestra un resumen más detallado de su contenido.

1. Introducción

  • Los ordenadores se han utilizado para ayudar a algunos matemáticos puros a hacer su trabajo desde que existen los ordenadores.
  • Birch y Swinnerton-Dyer utilizaron un ordenador para calcular muchos ejemplos de soluciones de ecuaciones cúbicas en dos variables módulo números primos.
  • Este artículo es un intento de explicar a todos los investigadores en matemáticas puras que los ordenadores pueden utilizarse ahora para ayudarnos no sólo a calcular, sino a razonar.
  • Se trata de la posibilidad de que los ordenadores pronto nos ayuden a demostrar teoremas.
  • No se debe esperar en los próximos 10 años que un ordenador, por sí solo, consiga una demostración de cualquier problema abierto de interés para los matemáticos puros.
  • Lo que se debe esperar en los próximos 10 años:
    • Que los ordenadores ayuden a los matemáticos puros a demostrar teoremas.
    • Bases de datos de matemáticas digitalizadas y con capacidad de búsqueda semántica.
    • Que los ordenadores completen las pruebas de los lemas, señalen contraejemplos a nuestras conjeturas y sugieran resultados que nos podrían ser útiles.
  • La formalización es la matemática reinterpretada como un juego de ordenador.
  • Los primeros asistentes de pruebas por ordenador aparecieron en los años sesenta.
  • Más recientemente han ocurrido dos cosas:
    • Los resultados a nivel de investigación en todas las áreas tradicionales de las matemáticas puras son ahora accesibles a estos sistemas.
    • Muchos asistentes de pruebas modernos admiten “tácticas”, lo que permite a los matemáticos comunicarse con estas máquinas de un modo de alto nivel, similar al modo en que se comunican entre sí.

2. Breve historia de los teoremas verificados formalmente

2.1. El siglo XX

  • Pruebas de
    • La raíz cuadrada de 2 es irracional.
    • Hay infinitos números primos.
    • Si x e y son números reales, entonces (x + y)(x + 2y)(x + 3y) = x³ + 6x²y + 11xy² + 6y³ se puede demostrar con la táctica ring.

2.2. El teorema de los cuatro colores

  • Una de sus formulaciones es la afirmación de que los vértices de todo grafo plano (sin bucles) pueden colorearse con cuatro colores de forma que ningún vértice adyacente comparta un color.
  • En 1976, Appel y Haken lo probaron utilizando un ordenador de manera esencial.
    • En este caso el ordenador se utilizaba para calcular y no para demostrar.
    • La prueba se basa, esencialmente, en un cálculo informático y, por tanto, depende de la corrección del código informático.
  • En 2005, Georges Gonthier verificó formalmente el resultado de Appel-Haken .
    • El trabajo consta de 60.000 líneas de código escritas en el asistente de pruebas Coq.
    • Comprende pruebas en topología y teoría de grafos, al tiempo que verifica formalmente el cálculo informático necesario para terminar la prueba.
    • Gran parte del trabajo consistió en escribir material de base en lugar de formalizar la prueba en sí.

2.3. El teorema de los números primos

  • En 2007, un equipo formado por Jeremy Avigad, Kevin Donnelly, David Gray y Paul Raff verificó formalmente el teorema de los números primos, en el sistema Isabelle/HOL.
    • El trabajo se basaba en las teorías de la aritmética y el análisis real básico.
    • En 2007, las matemáticas más serias de nivel de licenciatura y de máster ya eran, en teoría, accesibles a estos sistemas, al menos en algunas áreas de las matemáticas puras.
  • En 2009, John Harrison formalizó la prueba analítica compleja del teorema de los números primos en HOL Light.
  • En 2016, Mario Carneiro formalizó la prueba en Metamath.
  • Una de las razones por las que el resultado se estaba formalizando de forma independiente en varios demostradores de teoremas era que resultaba extremadamente difícil traducir una demostración escrita en uno de los sistemas a una demostración en otro sistema.
  • En 2020, Mario Carneiro tradujo la prueba a Lean.

2.4. Teorema del orden impar

  • El teorema del orden impar afirma que cualquier grupo finito de orden impar es resoluble.
  • En 2013, un equipo de 15 personas dirigido por Gonthier verificó formalmente una prueba de este teorema en Coq.
  • La prueba es muy larga; un argumento completo (modulo los fundamentos en teoría de grupos y representaciones) se presenta en los dos volúmenes.
  • El teorema está mucho más allá de las matemáticas de nivel de maestría (este trabajo fue una de las razones por las que Thompson fue galardonado con la Medalla Fields en 1970).
  • La prueba de Coq implicó la formalización de los dos libros mencionados anteriormente, además de la teoría de grupos, la teoría de la representación, la teoría de Galois y la teoría de los números.
  • La formalización del material de base ocupó gran parte de los seis años que los autores dedicaron a la prueba.
  • Lo que este trabajo de formalización nos muestra es que los demostradores de teoremas son ahora capaces de operar a este tipo de escala.
  • Por término medio, una línea de matemáticas en los libros de texto correspondía a cinco líneas de código informático, por lo que sabemos que en 2013 el llamado “factor De Bruijn” para este tipo de matemáticas es de alrededor de 5.
  • Los grandes proyectos de formalización como éste son una forma muy eficaz de motivar el desarrollo de bibliotecas de matemáticas fundamentales.
  • Una de las consecuencias de este proyecto de formalización fue que Coq desarrolló una biblioteca muy sólida de álgebra de nivel universitario que, por supuesto, puede utilizarse (y se utiliza) para otros proyectos.

2.5. La conjetura de Kepler

  • La conjetura de Kepler afirma que el empaquetamiento cúbico centrado en la cara es la forma más densa de empaquetar esferas congruentes en el espacio.
  • En 1998, Hales y Ferguson demostraron la conjetura.
    • Parte de la prueba de Hales-Ferguson consistió en la comprobación de más de 23.000 desigualdades no lineales en un ordenador.
    • También se realizaron otros cálculos informáticos.
  • En 2003 Hales anunció un proyecto para verificar formalmente la prueba.
    • El proyecto de formalización tardó unos 12 años en completarse, y comprendió más de medio millón de líneas de código.
    • Uno de los principales beneficios del trabajo es que la biblioteca estándar de HOL Light creció hasta incluir teoremas como el teorema del punto fijo de Brouwer, el teorema de Krein-Milman y el teorema de Stone- Weierstrass.
  • En 2017, Hales dio una charla en la que cuenta la historia de la prueba de Kepler y explica su visión para el futuro de las matemáticas formalizadas.

2.6. Espacios perfectoides

  • Este proyecto implicaba el desarrollo de teorías básicas de localización de anillos y de gavillas en espacios topológicos.
  • El proyecto aclaró que debería ser posible formalizar objetos matemáticos mucho más complejos.
  • A finales de 2017 a Patrick Massot y a Kevin Buzzard se les ocurrió de forma independiente la idea de formalizar los espacios perfectoides. En 2018 Johan Commelin se unió al proyecto.
  • El proyecto se podría resumir como una formalización informática de la única línea matemática “sea X un espacio perfectoide”
  • La principal ganancia fue la ampliación de la biblioteca matemática de Lean, mathlib, con los resultados de la Topología General de Bourbaki así como muchos resultados del álgebra topológica y los inicios de una teoría de campos de valoración discretos.
  • La siguiente pregunta natural es si los sistemas de demostración por ordenador pueden demostrar teoremas complejos sobre objetos complejos.

2.7. Matemáticas condensadas

  • Clausen y Scholze han estado desarrollando una teoría de las matemáticas condensadas, con el objetivo de conseguir que las técnicas del álgebra homológica se apliquen a varios problemas de la teoría de la geometría analítica.
  • Scholze desafió a la comunidad de la formalización para demostrar su Teorema 9.1 en una entrada de su blog.
  • Johan Commelin se convirtió en el líder de facto del proceso de formalización, y Patrick Massot le apoyó y un equipo de teóricos de números algebraicos y geómetras aritméticos comenzó a trabajar en el proyecto.
  • En seis meses, el equipo había crecido hasta contar con más de diez personas y había formalizado una demostración completa del teorema 9.4.
  • En el momento de escribir estas líneas no se ha deemostrado el teorema 9.1, pero es sólo cuestión de tiempo.
  • Esto representa una prueba sustancial de que ahora cualquier matemática pura puede formalizarse con demostradores de teoremas.
  • En muchos proyectos de formalización se suele dedicar una cantidad de tiempo considerable a la formalización del material de base.
  • A medida que las bibliotecas de los demostradores mejoren y empiecen a contener el tipo de material que los matemáticos en activo dan por sentado, habrá menos de estos “costes iniciales”.

2.8. Otros resultados

  • Sebastien Gouëzel formalizó las definiciones básicas de los ∞colectores Ck y C en Lean.
  • Mahboubi y Sibut-Pinote demostraron la irracionalidad de ζ(3) en Coq y Eberl lo demostró en Isabelle/HOL.
  • Han y van Doorn demostraron la independencia de la hipótesis del continuo en Lean.
  • Immler verificó formalmente los cálculos de Tucker utilizados para verificar la existencia del atractor extraño.
  • Mehta y Dillies verificaron formalmente el teorema de Roth sobre las progresiones aritméticas en Lean.
  • Argyraki, Edmonds y Paulson verificaron el teorema de Szemeredi en Isabelle/HOL.
  • La resolución de Ellenberg-Gijswijt de la conjetura del conjunto tope fue verificada en Lean por Dahmen, Hölzl y Lewis.

3. mathlib

  • mathlib:
    • Es la biblioteca de matemáticas de Lean.
    • Es una de las mayores colecciones de matemáticas formalizadas que existen.
    • Actualmente está experimentando un rápido crecimiento.
  • En 2013, Leonardo de Moura inició el desarrollo del Lean Theorem Prover.
  • En 2017, se decidió separar la mayor parte de la parte “matemática” del prover de la parte “central”, y trasladar las matemáticas a una biblioteca propia. De esta forma nació mathlib.
  • En el 2017, mathlib contenía definiciones de grupos, anillos y topología espacios, filtros, una construcción de los números racionales (los naturales y los enteros se quedaron en el núcleo de Lean), y poco más.
  • Johannes Hölzl y Mario Carneiro se convirtieron en los mantenedores de mathlib.
  • La biblioteca es un proyecto gratuito y de código abierto.
  • mathlib tiene ahora más de 200 colaboradores.
  • Uno de los principios de la biblioteca es hacer las cosas “en la generalidad correcta”.
  • La biblioteca no está concebida con fines pedagógicos o de legibilidad; la idea es seguir creando una base sólida para el tipo de matemáticas que se dan en un departamento de matemáticas puras contemporáneo.
  • Es interesante observar que Lean parece estar aprendiendo matemáticas más o menos a la misma velocidad que un estudiante universitario.
  • Para tener una idea actualizada del estado actual de mathlib, lo mejor es echar un vistazo a la descripción completa de mathlib de la comunidad Lean aquí, o a su resumen de las matemáticas de nivel universitario que contiene aquí.

4. Una breve guía de la teoría de tipos

  • Muchos demostradores de teoremas modernos utilizan alguna versión de la teoría de tipos como base.
    • Isabelle/HOL y los otros sistemas HOL utilizan la teoría de tipos simple.
    • Lean y Coq utilizan la teoría de tipos dependiente.
    • Los diversos sistemas HoTT utilizan la teoría de tipos de homotopía.
  • Hoy en día la mayoría de las matemáticas que se realizan en los demostradores de teoremas se hacen en un sistema de teoría de tipos,

4.1. ¿Qué es un tipo?

  • En definiciones como la de grupo, la palabra “conjunto” no significa más que “colección de elementos”.
  • En la teoría de tipos, el papel de “colección de elementos” lo desempeña el tipo.
  • Un tipo es una colección de términos.
  • La definición de un grupo en la teoría de tipos: un grupo es un tipo dotado de multiplicación tal que se cumplen algunos axiomas.
  • La única diferencia es la notación: el `a ∈ X` de la teoría de conjuntos se sustituye por el `a : X` de la teoría de tipos.
  • En la teoría de tipos, todo es un término, y todo término tiene un tipo, pero no todo término es un tipo.
  • Una diferencia entre los tipos y los conjuntos es que los tipos no se mezclan: los tipos distintos son disjuntos.

4.2. Tipos inductivos

  • En Lean se pueden definir tipos “inductivamente”. Por ejemplo, la definición de los naturales es así: 
    nat inductive
| cero : nat
| suc (n : nat) : nat

    Con la definición se obtienen:

    • constructores_
      • nat.cero ; nat
      • nat.suc : nat -> nat
    • el eliminador del tipo que permite construir funciones cuyo dominio son las naturales y cuyo codominio es otra cosa. En otras palabras, es el principio de recursión.
  • En Lean, la propia igualdad se define como un tipo inductivo 
    inductive eq {X : Type} : X → X → Prop
| refl (a : X) : eq a a

4.3. Las proposiciones son tipos

  • Una proposición es un tipo y sus pruebas son sus términos.
  • La hipótesis h de que P implica Q se convierte en una función h : P → Q.

4.4. Las pruebas son funciones

  • Nueva forma de pensar en la naturaleza de una prueba: se trata de una función que toma como entrada las hipótesis del resultado que se afirma, y devuelve como salida una prueba del resultado.

4.5. Un ejemplo

  • Enunciado: 
    example (n : ℕ) : (∑ i in range n, i^3 : ℚ) = ((n-1)*n/2)^2 :=
sorry
  • Demostración (se encuentra aquí) 
    -- use Lean's tactics
import tactic

open_locale big_operators

open finset

example (n : ℕ) : (∑ i in range n, i^3 : ℚ) = ((n-1)*n/2)^2 :=
begin
  induction n with d hd,
  { simp, ring },
  { rewrite sum_range_succ,
    rewrite hd,
    simp, ring }
end

4.6. Fundamentos

  • Los matemáticos suelen tener muy poco interés en los tecnicismos de los fundamentos lógicos de su materia.
  • Las controversias de principios del siglo XX sobre si los métodos no constructivos están permitidos en las demostraciones matemáticas han desaparecido hace tiempo.

5. El futuro

5.1. Un nuevo tipo de documento matemático

  • La formalización ofrece la posibilidad de un nuevo tipo de documento matemático, en el que el lector puede decidir qué cantidad de detalles son visibles.
  • También se podría imaginar que los libros de texto del grado se escribieran de esta manera, en la que las afirmaciones que un estudiante no pueda entender (quizás por ser ambiguas) puedan ser inspeccionadas con más detalle hasta que se resuelvan las dificultades.

5.2. Búsqueda semántica en una base de datos matemática

  • Algo que no va a ocurrir pronto es que todos los matemáticos empiecen a escribir todos sus trabajos en un asistente de pruebas formal.
  • se puede esperar un futuro en el que algunos trabajos se formalicen parcialmente, o incluso completamente, en un demostrador de teoremas.
  • Hales aboga por una versión formalizada de Math Reviews/Zentralblatt. Es decir, un sitio web cuya función sea simplemente exponer formalmente los resultados que se anuncian en las principales revistas de matemáticas.
  • El problema con el plan de Hales es que para poder formalizar los enunciados de los teoremas habría que definir todos los objetos básicos que se utilizan.
  • La comunidad de Lean se ha esforzado por introducir en mathlib algunas de las principales definiciones de la matemática de investigación moderna.
  • Un proyecto relacionado es la formalización de etiquetas en el Proyecto Stacks: una gigantesca base de datos en línea de geometría algebraica, de libre acceso en línea.
  • Formalizar todas las pruebas del Proyecto Stacks no es una idea factible. Sin embargo, formalizar sólo las definiciones y el estado de los teoremas es una tarea absolutamente accesible.

5.3. Comprobación de pruebas

  • Lo que es factible es formalizar partes de la pruebas de grandes teoremas.
  • Los demostradores de teoremas pueden utilizarse para comprobar pruebas que los humanos podrían considerar tediosas.

5.4. La enseñanza

  • Deberíamos enseñar a los estudiantes universitarios a utilizar los asistentes de pruebas.
  • Los demostradores deben ser más fáciles de usar, quizás con interfaces gráficas y documentación más apropiada para los matemáticos.

5.5. Otras ideas

  • Es hora de mirar más allá de cómo solemos enseñar y aprender matemáticas, y tratar de entender cómo nosotros, como comunidad de matemáticos, podemos utilizar la inevitable digitalización del material matemático como una herramienta para mejorar nuestras vidas, y las de nuestros estudiantes.
Seguir leyendo →

Materiales para el estudio de la programación funcional con Haskell

José A. Alonso--

He publicado en GitHub la página Informática con materiales para el estudio de la programación funcional con Haskell cuyo contenido se ha ido creando a lo largo de los 11 años que he impartido la asignatura de Informática en primero del Grado en Matemáticas.

Voy a comentar su contenido siguiendo los apartados de la página y en la última sección comentaré su desarrollo histórico.

1. Temas y códigos

El primer apartado la página es Temas y códigos que contiene los apuntes y códigos de los temas. Los temas están en las siguientes versiones:

Respecto a los códigos de los temas:

  • En el repositorio de Códigos de los temas están los códigos de los temas como un proyecto. Está escrito como un proyecto de forma que basta ejecutar stack test para instalar Haskell, las librerías necesarias y verificar todos los ejemplos.
  • En I1M: Code for the Haskell course taught at the University of Seville, de Hackage, está el código y la documentación de las librerías desarrolladas en el curso.
  • En la página codigosDeTemas están los enlaces a los códigos de los temas usados en los apuntes de los temas.

2. Manuales de funciones Haskell

El segundo apartado es Manuales que contiene las manuales, con ejemplos, de las funciones de las librerías que se usan en el curso.

3. Relaciones de ejercicios

El tercer apartado es Ejercicios que contiene:

  • El repositorio Ejercicios de I1M con las relaciones de ejercicios y sus soluciones. Está escrito como un proyecto de forma que basta ejecutar stack
    test     para instalar Haskell, las librerías necesarias y verificar todos los ejemplos.
  • El libro Ejercicios de programación funcional con Haskell con los ejercicios del repositorio anterior. Este libro es una compilación de los que he ido publicando cada año, desde el curso 2009-10, con las relaciones del curso como se explica más detalladamente en la última sección. El libro consta de tres partes: introducción a la programación funcional (PF), matemática mediante PF y algorítmica mediante PF. La segunda parte, aunque se plantean como relaciones de ejercicios, en realidad se deben de ver como temas desarrollados por los alumnos.
  • El libro Piensa en Haskell tiene una colección de ejercicios de programación funcional con Haskell. Publicado en el 2012, es una versión preliminar del anterior.
  • El blog Exercitium con los problemas propuestos diariamente desde el curso 2013-14 hasta el 2019-20.

4. Colección de exámenes

El cuarto apartado es Exámenes que contiene:

5. Sistemas utilizados

El quinto apartado es Sistemas donde se indica la forma de instalar Haskell y las librerías usadas en el curso.

6. Enlaces a los cursos que han usado el material.

El sexto apartado es Cursos con los enlaces a los cursos que han usado el material desde el 2009-10 al 2019-20.

7. Enlaces con documentación.

El séptimo apartado es Documentación con enlaces a vídeos, libros y otros recursos sobre Haskell. Su última sección es una colección de enlaces a sitios con ejercicios de programación, algunos de los cuales (como Kattis) se han usado algunos años.

8. Evolución del contenido

Las páginas de los cursos, en las que se puede ver la evolución del contenido, son Curso 2009-10, Curso 2010-11, Curso 2011-12, Curso 2012-11, Curso 2013-11, Curso 2014-15, Curso 2015-16, Curso 2016-17, Curso 2017-18, Curso 2018-19 y Curso 2019-20.

El desarrollo histórico de los temas es el siguiente:

Respecto de los ejercicios, al final de cada curso he publicado un libro con las soluciones de sus ejercicios. Los libros son: Ejercicios del 2009-10, Ejercicios del 2010-11, Ejercicios del 2011-12, Ejercicios del 2012-13, Ejercicios del 2013-14, Ejercicios del 2014-15, Ejercicios del 2015-16, Ejercicios del 2016-17, Ejercicios del 2017-18, Ejercicios del 2018-19 y Ejercicios del 2019-20.

Además, en el verano del 2012 publiqué el libro Piensa en Haskell que contiene una colección de ejercicios de programación funcional en Haskell que incluye ejercicios de los tres primeros cursos.

De igual forma, a lo largo de cada curso he ido publicado las soluciones de sus exámenes. Los libros son Exámenes del 2009-10, Exámenes del 2010-11, Exámenes del 2011-12, Exámenes del 2012-13, Exámenes del 2013-14, Exámenes del 2014-15, Exámenes del 2015-16, Exámenes del 2016-17, Exámenes del 2017-18, Exámenes del 2018-19 y Exámenes del 2019-20.

El desarrollo histórico de los manuales es el siguiente:

Por último, desde el curso 2010-11 he publicado en el blog Vestigium los diarios de clases (con un breve resumen de su contenido) que se iban publicando al final de cada clase. Los diarios (cuyas entradas están en orden cronológico inverso) son: Diario del 2010-11, Diario del 2011-12, Diario del 2012-13, Diario del 2013-14, Diario del 2014-15, Diario del 2015-16, Diario del 2016-17, Diario del 2017-18, Diario del 2018-19 y Diario del 2019-20.

Seguir leyendo →

Resumen de lecturas compartidas durante agosto de 2021

José A. Alonso--

Esta entrada es una recopilación de lecturas compartidas, durante agosto de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.

Seguir leyendo →