- Lean es un lenguaje de programación diseñado para formalizar matemáticas, y permite que los matemáticos manejen los teoremas matemáticos como si fueran código.
- Los usuarios escriben teoremas, pruebas y axiomas, entre otros, en formato de código, y el proceso de prueba se lleva a cabo mediante un conjunto de comandos llamado tactic.
- Aunque se puede cerrar provisionalmente una prueba con
sorry aunque aún no esté terminada, esto es una prueba falsa similar al any de TypeScript.
- Si se agregan axiomas de forma incorrecta (por ejemplo,
2 = 3), surge el riesgo de contradicción lógica y de la posibilidad de probar cualquier enunciado.
- Lean solo obtiene conclusiones sobre los axiomas elegidos y el sistema de pruebas lógicamente válido, por lo que preservar la validez matemática es de gran importancia.
Lean: un lenguaje para trabajar la matemática como código
- Lean es un lenguaje de programación especializado en escribir matemáticas formalizadas.
- Los matemáticos usan Lean para expresar la matemática como código y estructurar sus teoremas y demostraciones para poder colaborar y compartirlos.
- Plantea un futuro en el que una gran parte del conocimiento matemático de la humanidad podría volverse código para verificación y composición mecánica.
Primeros pasos en una prueba en Lean
- Es posible declarar un teorema simple en Lean como
theorem two_eq_two : 2 = 2 := by sorry.
- Cuando la prueba no está completa, se usa
sorry, pero es solo un recurso temporal y no una prueba real.
sorry pasa la verificación de pruebas de Lean, pero lógicamente no se puede considerar confiable.
- Para una prueba completa se usan táctica como
rfl (reflexividad) para demostrar una igualdad trivial como 2 = 2.
- Lo que ya se ha demostrado puede reutilizarse en otros teoremas con
exact, destacando la modularidad.
Axiomas y contradicción: cuando la matemática está embrujada
- Si se agrega un axioma como
axiom math_is_haunted : 2 = 3, Lean lo tratará como verdadero.
- Ese axioma puede luego aplicarse en procesos de prueba y permite demostrar conclusiones matemáticamente imposibles (por ejemplo,
2 + 2 = 6).
- Es posible usar la táctica
rewrite para sustituir 2 por 3 y terminar el procedimiento de demostración con rfl.
- Si un axioma inadecuado provoca contradicción, en Lean se llega a un estado donde todas las proposiciones son demostrables (colapso lógico).
- En realidad, a principios del siglo XX, paradojas como la de Russell provocaron una revisión profunda de los fundamentos matemáticos debido a contradicciones en sistemas axiomáticos.
- Lean muestra claramente que la elección de los axiomas es decisiva para mantener la validez de un sistema lógico.
Lean como verificador de pruebas (proof checker)
- Si los axiomas se eligen bien y Lean es lógicamente correcto, ofrece conclusiones con fiabilidad teórica.
- Verifica desde igualdades simples hasta teoremas muy complejos (por ejemplo, el Último Teorema de Fermat) siguiendo los mismos principios.
- Un gran teorema se completa como un árbol en el que la estructura total se va armando a partir de la acumulación repetida de pruebas de subestructuras y teoremas.
- Como ejemplo, existe un proyecto a gran escala para formalizar el Último Teorema de Fermat en Lean, y se espera que finalmente se complete un sistema de prueba formal sin pruebas provisionales (
sorry).
El placer de aprender Lean
- Hacer pruebas con Lean es una combinación creativa de programación y matemáticas.
- Al principio se trata de aprender a probar proposiciones simples, y luego, gradualmente, el proceso de construir matemáticas cada vez más complejas y profundas con rigurosidad se vuelve una gran fuente de disfrute.
- Los tutoriales oficiales y recursos comunitarios (por ejemplo, Natural Numbers Game, Mathematics in Lean, entre otros) son adecuados para empezar.
- Al usar Lean, al formalizar la lógica por uno mismo, se puede redescubrir la belleza de ideas y argumentos ingeniosos.
- Finalmente se concluye que, con o sin una razón aparente, para cierto tipo de personas Lean brinda una diversión especial.
Aún no hay comentarios.