DAO – Página 2 – Vestigium

Reseña: Formalising Lie algebras in Lean

PorJosé A. Alonso 27 diciembre 202127 diciembre 2021

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.

Reseña: Why formalize mathematics?

PorJosé A. Alonso 26 diciembre 202126 diciembre 2021

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 ∀ ε &gt; 0, ∃ N, ∀ n ≥ N, |f (u n) - f x₀| ≤ ε,
  Fix ε &gt; 0,
  By hf applied to ε using ε_pos we obtain δ such that
    (δ_pos : δ &gt; 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

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.

ForMatUS: Pruebas en Lean de propiedades de la composición de funciones (elemento neutro y asociatividad)

PorJosé A. Alonso 3 noviembre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de propiedades de la composición de funciones:

la función identidad es el elemento neutro de la composición y
la composición es asociativa.

En las pruebas se usan los estilos aplicativos y declarativos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic

open function

variables {X Y Z W : Type}

-- ----------------------------------------------------
-- Ej. 1. Demostrar que
--    id ∘ f = f
-- ----------------------------------------------------

-- 1ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  calc (id ∘ f) x = id (f x) : by rw comp_app
       ...        = f x      : by rw id.def,
end

-- 2ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  rw comp_app,
  rw id.def,
end

-- 3ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  rw [comp_app, id.def],
end

-- 4ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  calc (id ∘ f) x = id (f x) : rfl
       ...        = f x      : rfl,
end

-- 5ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
rfl

-- 6ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
-- by library_search
left_id f

-- 7ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
comp.left_id f

-- ----------------------------------------------------
-- Ej. 2. Demostrar que
--    f ∘ id = f
-- ----------------------------------------------------

-- 1ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  calc (f ∘ id) x = f (id x) : by rw comp_app
       ...        = f x      : by rw id.def,
end

-- 2ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  rw comp_app,
  rw id.def,
end

-- 3ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  rw [comp_app, id.def],
end

-- 4ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  calc (f ∘ id) x = f (id x) : rfl
       ...        = f x      : rfl,
end

-- 5ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
rfl

-- 6ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
-- by library_search
right_id f

-- 7ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
comp.right_id f

-- ----------------------------------------------------
-- Ej. 3. Demostrar que
--    (f ∘ g) ∘ h = f ∘ (g ∘ h)
-- ----------------------------------------------------

-- 1ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
begin
  ext,
  calc ((f ∘ g) ∘ h) x
           = (f ∘ g) (h x)   : by rw comp_app
       ... = f (g (h x))     : by rw comp_app
       ... = f ((g ∘ h) x)   : by rw comp_app
       ... = (f ∘ (g ∘ h)) x : by rw comp_app
end

-- 2ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
begin
  ext,
  rw comp_app,
end

-- 3ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
begin
  ext,
  calc ((f ∘ g) ∘ h) x
           = (f ∘ g) (h x)   : rfl
       ... = f (g (h x))     : rfl
       ... = f ((g ∘ h) x)   : rfl
       ... = (f ∘ (g ∘ h)) x : rfl
end

-- 4ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
rfl

-- 5ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
comp.assoc f g h

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

import tactic

open function

variables {X Y Z W : Type}

-- ----------------------------------------------------

-- Ej. 1. Demostrar que

-- id ∘ f = f

-- ----------------------------------------------------

-- 1ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

calc (id ∘ f) x = id (f x) : by rw comp_app

... = f x : by rw id.def,

end

-- 2ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

rw comp_app,

rw id.def,

end

-- 3ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

rw [comp_app, id.def],

end

-- 4ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

calc (id ∘ f) x = id (f x) : rfl

... = f x : rfl,

end

-- 5ª demostración

example

(f : X → Y)

: id ∘ f = f :=

rfl

-- 6ª demostración

example

(f : X → Y)

: id ∘ f = f :=

-- by library_search

left_id f

-- 7ª demostración

example

(f : X → Y)

: id ∘ f = f :=

comp.left_id f

-- ----------------------------------------------------

-- Ej. 2. Demostrar que

-- f ∘ id = f

-- ----------------------------------------------------

-- 1ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

calc (f ∘ id) x = f (id x) : by rw comp_app

... = f x : by rw id.def,

end

-- 2ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

rw comp_app,

rw id.def,

end

-- 3ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

rw [comp_app, id.def],

end

-- 4ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

calc (f ∘ id) x = f (id x) : rfl

... = f x : rfl,

end

-- 5ª demostración

example

(f : X → Y)

: f ∘ id = f :=

rfl

-- 6ª demostración

example

(f : X → Y)

: f ∘ id = f :=

-- by library_search

right_id f

-- 7ª demostración

example

(f : X → Y)

: f ∘ id = f :=

comp.right_id f

-- ----------------------------------------------------

-- Ej. 3. Demostrar que

-- (f ∘ g) ∘ h = f ∘ (g ∘ h)

-- ----------------------------------------------------

-- 1ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

begin

ext,

calc ((f ∘ g) ∘ h) x

= (f ∘ g) (h x) : by rw comp_app

... = f (g (h x)) : by rw comp_app

... = f ((g ∘ h) x) : by rw comp_app

... = (f ∘ (g ∘ h)) x : by rw comp_app

end

-- 2ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

begin

ext,

rw comp_app,

end

-- 3ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

begin

ext,

calc ((f ∘ g) ∘ h) x

= (f ∘ g) (h x) : rfl

... = f (g (h x)) : rfl

... = f ((g ∘ h) x) : rfl

... = (f ∘ (g ∘ h)) x : rfl

end

-- 4ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

rfl

-- 5ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

comp.assoc f g h

ForMatUS: Pruebas en Lean de que la identidad es biyectiva

PorJosé A. Alonso 3 noviembre 202022 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de que la identidad es biyectiva usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic

open function

variables {X : Type}

-- #print injective
-- #print surjective
-- #print bijective

-- ----------------------------------------------------
-- Ej. 1. Demostrar que la identidad es inyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : injective (@id X) :=
begin
  intros x₁ x₂ h,
  exact h,
end

-- 2ª demostración
example : injective (@id X) :=
λ x₁ x₂ h, h

-- 3ª demostración
example : injective (@id X) :=
λ x₁ x₂, id

-- 4ª demostración
example : injective (@id X) :=
assume x₁ x₂,
assume h : id x₁ = id x₂,
show x₁ = x₂, from h

-- 5ª demostración
example : injective (@id X) :=
--by library_search
injective_id

-- 6ª demostración
example : injective (@id X) :=
-- by hint
by tauto

-- 7ª demostración
example : injective (@id X) :=
-- by hint
by finish

-- ----------------------------------------------------
-- Ej. 2. Demostrar que la identidad es suprayectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : surjective (@id X) :=
begin
  intro x,
  use x,
  exact rfl,
end

-- 2ª demostración
example : surjective (@id X) :=
begin
  intro x,
  exact ⟨x, rfl⟩,
end

-- 3ª demostración
example : surjective (@id X) :=
λ x, ⟨x, rfl⟩

-- 4ª demostración
example : surjective (@id X) :=
assume y,
show ∃ x, id x = y, from exists.intro y rfl

-- 5ª demostración
example : surjective (@id X) :=
-- by library_search
surjective_id

-- 6ª demostración
example : surjective (@id X) :=
-- by hint
by tauto

-- ----------------------------------------------------
-- Ej. 3. Demostrar que la identidad es biyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : bijective (@id X) :=
and.intro injective_id surjective_id

-- 2ª demostración
example : bijective (@id X) :=
⟨injective_id, surjective_id⟩

-- 3ª demostración
example : bijective (@id X) :=
-- by library_search
bijective_id

100

101

102

103

104

import tactic

open function

variables {X : Type}

-- #print injective

-- #print surjective

-- #print bijective

-- ----------------------------------------------------

-- Ej. 1. Demostrar que la identidad es inyectiva.

-- ----------------------------------------------------

-- 1ª demostración