Por qué no usar simplemente Lean

 (lawrencecpaulson.github.io)
1 puntos por GN⁺ 1 일 전 | 1 comentarios | Compartir por WhatsApp
  • La historia de la formalización matemática no empezó con Lean, y durante casi 60 años varios linajes de sistemas ya habían acumulado técnicas clave y logros importantes
  • Herramientas como AUTOMATH en 1968, la familia LCF, HOL, Rocq, ACL2 y Mizar lograron formalizaciones amplias, desde análisis real hasta el teorema de los números primos, el teorema de los cuatro colores y la conjetura de Kepler
  • Lean construyó rápidamente definiciones de la matemática moderna apoyándose en una gran biblioteca y una comunidad activa, pero propositions as types y los tipos dependientes no son el único camino para los asistentes de prueba
  • Isabelle destaca por su automatización fuerte, alta legibilidad y la ventaja de evitar tipos dependientes, continuando la tradición LCF de construir verificación de pruebas mediante la barrera de abstracción del kernel incluso sin proof objects
  • A medida que la IA también ordena pruebas estructuradas y las traduce entre sistemas, podría seguir disminuyendo la presión de ver una sola herramienta como estándar absoluto

Sistemas iniciales y otros linajes

  • AUTOMATH

    • AUTOMATH ya incluía en 1968 la mayoría de los elementos necesarios para la formalización matemática
    • En 1977, Jutting formalizó con AUTOMATH Foundations of Analysis de Landau, yendo desde la lógica pura hasta la construcción de los números complejos
    • Usó clases de equivalencia y el conjunto de los números racionales, y también demostró formalmente la completitud de Dedekind de la recta real
    • Este logro no volvió a aparecer durante 20 años, y solo a mediados de los noventa se retomó la formalización de los reales en HOL Light de John Harrison y en Isabelle/HOL de Jacques Fleuriot
    • La notación era muy incómoda y no había automatización alguna, por lo que las pruebas eran largas y difíciles de leer
    • Aun así, considera que era mejor que Rocq para tratar clases de equivalencia; a diferencia del setoid hell que sufren los usuarios de Rocq, Jutting llevó a cabo esa formalización con calma

  • Boyer y Moore

La evolución después de LCF

  • Edinburgh LCF se concentró en teoría de lenguajes de programación, pero la idea de usar un lenguaje funcional como metalenguaje del asistente de prueba se difundió ampliamente
  • Varios grupos en Cambridge, INRIA, Cornell y otros lugares usaron ML para crear herramientas como HOL temprano, Coq (hoy Rocq) y Nuprl
  • El grupo HOL se enfocó en verificación de hardware, pero la verificación de hardware de punto flotante terminó requiriendo análisis real
  • John Harrison demostró en la familia HOL resultados matemáticos de peso como el teorema de los números primos mediante la fórmula integral de Cauchy
  • Bajo el objetivo de verificar la mayor cantidad posible de los 100 theorems, HOL Light estuvo con frecuencia entre los primeros lugares
  • Para 2014, los sistemas de este linaje ya habían formalizado varios teoremas avanzados
  • En general, estas pruebas eran largas y complejas, y el trabajo de formalización también fue de gran escala, desempeñando un papel clave para reducir dudas que aún rodeaban a esos teoremas

El ascenso de la comunidad de Lean

  • Los matemáticos veían que los logros previos de formalización aún no llegaban a construcciones sofisticadas de la matemática moderna dominante, como Grothendieck schemes o perfectoid spaces
  • Tom Hales eligió avanzar acumulando esas definiciones como biblioteca y, más que centrarse en las pruebas, puso el foco en la acumulación de definiciones, eligiendo Lean
  • Presentó esta dirección en el programa Big Proof, donde también se discutieron ideas similares
  • Kevin Buzzard escuchó esto y decidió probar Lean en educación, tras lo cual su difusión se aceleró
  • Como punto de inflexión importante en la comunidad Lean, se señala el alejamiento de la obsesión con la prueba constructiva que dominó durante mucho tiempo en Rocq
  • El intuicionismo apareció tras la paradoja de Russell y tuvo implicaciones específicas incluso para el concepto de número real
  • La teoría de tipos de Martin-Löf es claramente un formalismo intuicionista, pero se escribe que Rocq no puede entenderse de manera tan simple
  • Aun así, en trabajos relacionados con Rocq la prueba constructiva reaparecía repetidamente incluso donde era irrelevante o carente de sentido, y se considera que esa tendencia obstaculizó el uso matemático de Rocq y terminó cediendo terreno a Lean

La diferencia entre propositions as types y LCF

  • Propositions as types es la dualidad que conecta los símbolos lógicos ∀, ∃, →, ∧, ∨ con los constructores de tipos Π, Σ, →, ×, +
  • Este marco es hermoso y teóricamente productivo, pero no es el único camino
  • Si se limita un proof assistant a software que verifica pruebas bajo el principio de propositions as types, gran parte de la investigación del último medio siglo queda fuera de la definición
  • Entonces solo quedarían Rocq, Lean y Agda
  • Incluso AUTOMATH no es un caso de propositions as types; aunque tiene elementos parecidos a Π y →, establece la lógica como axiomas al estilo de un texto general de lógica
  • de Bruijn ya veía hace 50 años la necesidad de separar tipos y proposiciones
  • Un ejemplo representativo es la división: debe tomar tres argumentos, y el valor de (x/y) pasa a depender de una prueba de (y \ne 0), por lo que se necesita proof irrelevance
  • También subraya que la idea de que el enfoque LCF es igual a propositions as types no se ajusta a los hechos
  • Rocq y Lean tienen Prop como sort de las proposiciones, donde todos los objetos de prueba de una misma proposición se evalúan como el mismo valor y así se obtiene proof irrelevance
  • Pero eso no hace desaparecer los enormes objetos de prueba; en los sistemas reales siguen estando allí
  • El descubrimiento central de Robin Milner fue que en LCF no hacen falta objetos de prueba como tales
  • Si el kernel de pruebas se coloca dentro de un tipo de dato abstracto de ML y las reglas de inferencia se vuelven constructores, la verificación puede hacerse de manera dinámica
  • Se considera que la abstraction barrier de ML impide hacer trampa
  • Que términos gigantescos ocupen decenas de MB sin siquiera señalar nada resulta especialmente irracional en la era de RAMmageddon
  • También critica que incluso se continúe investigando cómo embellecer de forma más elegante esos términos innecesarios

Razones para elegir Isabelle

  • Si tus colegas usan Lean, la experiencia del equipo también está en Lean y las bibliotecas de base que necesitas están en Lean, entonces lo natural es usar Lean
  • Pero si puedes elegir libremente, hay razones claras para considerar Isabelle

  • Automatización

    • Señala como ventaja la automatización más potente, y sostiene que incluso comparada con los “hammer” cotidianos, nada está a la altura de sledgehammer
    • Añade que el lado del álgebra computacional también debe tratarse por separado

  • Legibilidad

  • Evitar tipos dependientes

    • Como no tiene tipos dependientes, evita niveles de universos y otras rarezas que complican la vida a principiantes
    • Señala que incluso en mathlib de Lean y en SSReflect y Mathematical Components de Rocq no se recomienda usar tipos dependientes
    • La dificultad central de los tipos dependientes es que, si se implementan correctamente, la verificación de tipos misma se vuelve indecidible
    • Esto se debe a que decidir la igualdad es indecidible, y se escribe que al principio este punto se aceptaba como algo natural
    • Desde alrededor de 1990, el consenso pasó a hacer decidible la verificación de tipos rebajando la igualdad a definitional/intensional equality
    • Como resultado, (T(N+1)) y (T(1+N)) se vuelven tipos distintos
    • Estas restricciones afectan a las pruebas reales, y además la propia comprobación de la igualdad definicional sigue teniendo un costo computacional considerable

Matemática moderna posible incluso sin tipos dependientes

La dirección futura y la IA

  • Lean está acertando en muchos aspectos y, al admitir incluso bloques de prueba anidados, tiene potencial para convertirse en un lenguaje de pruebas suficientemente legible
  • Ahora la comunidad de Lean debe usar realmente esas funciones, y se escribe que los usuarios de Isabelle ya lo hacen en gran medida
  • Más importante que un objeto de prueba verificable por computadora es la transparencia del texto de prueba que las personas realmente pueden leer
  • El auge de la IA hace esta diferencia todavía más clara
  • Las pruebas generadas por IA suelen ser desordenadas, pero son fáciles de ordenar con sledgehammer y, si la estructura está bien planteada, siguen siendo legibles aunque los detalles sean excesivos
  • Eso facilita captar el flujo del avance y reducirlo luego a una forma más simple
  • Recientemente incluso aparecieron investigaciones en las que un modelo de lenguaje llama directamente a sledgehammer
  • La IA también puede encargarse fácilmente de traducir pruebas estructuradas y legibles de un proof assistant a otro
  • Si eso ocurre, disminuye la carga misma de decidir qué sistema elegir

Complemento sobre la omisión de Mizar

  • La historia de la formalización matemática no puede estar completa sin Mizar y su enorme biblioteca matemática
  • El lenguaje Isar de Isabelle también recibió una fuerte influencia de Mizar
  • Corrige por separado el haber omitido Mizar y escribe que lo tratará en la próxima entrada

Lecturas relacionadas

1 comentarios

 
GN⁺ 1 일 전
Opiniones de Hacker News

  • La mayoría de los lectores de HN se parecen más a programadores que a matemáticos, así que parece más práctico ver Lean desde la perspectiva de la programación que desde la de las demostraciones matemáticas
    Como libro para abordar Lean desde la óptica de la programación funcional, https://leanprover.github.io/functional_programming_in_lean/ está bastante bien
    Yo también estoy aprendiendo Lean, así que puede que tenga una visión color de rosa de principiante, pero mi objetivo va más por escribir y demostrar código de programadores comunes, como algoritmos reales de compresión/descompresión, tal como en el ejemplo reciente de lean-zip
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • Mientras leía ese libro, probé por mi cuenta un simplificador básico de álgebra computacional en Lean
      https://github.com/dharmatech/symbolism.lean
      Es un port de código en C#, y la expresividad de Lean es sorprendentemente grande
    • Para ese tipo de uso, me pregunto si Dafny no sería una opción similar
      Recuerdo haber visto que se habló un poco de eso hace tiempo, aunque últimamente no he seguido de cerca esta área
    • Recuerdo casos de los años 90 en los que se experimentó con demostraciones de corrección de software, y según recuerdo, al final había más errores en las anotaciones de la prueba que en el software real
      Y además veo otros dos obstáculos. Primero, ya de por sí es difícil saber qué debe hacer el software, y lo que el usuario quiere hacer no necesariamente coincide con aquello por lo que el cliente paga
      Segundo, la calidad del trabajo de muchos desarrolladores es tan baja que cuesta creer que vayan a manejar mejor un lenguaje de la verdad que un lenguaje como Java
      Aunque lo segundo podría desaparecer si se reemplaza por sistemas de IA que pongan la atención necesaria, y en ese caso la situación podría cambiar
    • Me hace pensar en qué pasa con la programación no funcional
      Igual que las matemáticas que ya dejó de lado la programación funcional, creo que para la mayoría de los programadores tiene muy poca relevancia

  • Parece que el autor entendió bastante mal Lean, y sorprende más porque da la impresión de conocer bien esta área
    Da la impresión de que cree que Lean conserva tal cual los objetos de prueba y que, al final, verifica un único objeto de prueba gigantesco con todas las definiciones desplegadas, pero eso está lejos de la realidad
    Lean implementa prácticamente la misma optimización que el autor elogia como ventaja de LCF. Por poner una analogía, es como ir borrando el pizarrón mientras se avanza en la demostración
    Si en Lean4 se escribe con theorem y no con def, ese objeto de prueba deja de usarse, y no es una simple optimización sino una propiedad central del lenguaje. theorem es opaque
    Aunque quedara el término de la prueba, sería solo para que el usuario pueda verlo en modo interactivo, y al kernel ni siquiera le importa cuál era ese objeto de prueba

    • Esto se acerca más a una diferencia conceptual que de implementación
      En LCF, una prueba y un término son cosas distintas, y en mi opinión así debería ser. Esa confusión al estilo Curry-Howard es innecesaria, pero mucha gente cree que es la única manera de hacer matemáticas con computadoras
      Si uno quiere, en LCF también puede guardar y reutilizar pruebas, y en Lean también puede eliminarlas por optimización si así lo desea
    • En teoría de tipos dependientes, un objeto de prueba es simplemente el término que llena cierto tipo, así que me pregunto si eso significa que la implementación de Lean puede construir pruebas sin crear ese tipo de término
    • Suena correcto
      El enfoque de tipos abstractos quizá ahorre algo de memoria, pero sería solo una diferencia por factor constante, no una mejora asintótica
      Quejarse de que Lean desperdicia decenas de MB tal vez importaba en los años 80 y 90, pero hoy ya no parece una ventaja tan decisiva

  • Se oye mucho que Lean es bueno para programación funcional, pero viniendo de Agda se siente como un downgrade bastante tosco
    También se dice que sus tactic son buenas, pero por mi experiencia las tactic de Coq eran más potentes y más cómodas de usar
    Puede que todo esto sea sesgo de primera impresión, pero hasta ahora parece que la fortaleza de Lean no está en hacer una sola cosa mejor que nadie, sino en que en general cumple y tiene una comunidad grande
    Entiendo por qué resulta atractivo, pero también da un poco de pena sentir que en el proceso se perdió algo de belleza y de potencia

    • Al final también es una historia de efectos de red
      Pero estos efectos, aunque en el momento parezcan permanentes, en realidad duran menos de lo que uno cree. Si de verdad eso fuera lo único importante, Perl seguiría siendo un gigante hasta hoy
      En Lean pesa mucho haber conseguido primero una gran biblioteca. Algo parecido a lo que fue CPAN para Perl
      Pero si uno mira las leyes de escalamiento, para la mayoría de los usuarios el valor de una gran biblioteca probablemente crece más o menos como el logaritmo de su tamaño
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      Al principio esa brecha parece imposible de cerrar, pero no hace falta igualar el tamaño para que llegue un punto en que la usabilidad importe más
      Además, el port de bibliotecas matemáticas es una tarea que les calza muy bien a los LLM. La fuente ya está verificada, el destino también se puede verificar, y el camino de razonamiento en general se puede trasladar
      Visto al revés, gracias a los LLM la barrera para trabajar en plataformas minoritarias también baja más de lo esperado. Si puedo portar esa biblioteca a mi plataforma, probablemente también pueda portar mis pruebas hacia ella
    • Más bien eso parece significar que la comunidad por fin maduró y empezó a hacer trabajo real
      La clave no es tener la herramienta perfecta, sino lograr sacar el trabajo adelante con una herramienta suficientemente buena
    • Agda será mejor como verificador de pruebas, pero no me parece una opción práctica para desarrollar software
      Lean de verdad podría crecer hasta convertirse en un sucesor de Haskell, con potencial como lenguaje funcional para desarrollo de software
    • He usado un poco Agda y algo más Lean, y para escribir programas funcionales generales en vez de demostraciones matemáticas, Lean me resultó muchísimo más fácil
      Creo que la diferencia estaba sobre todo en el soporte de herramientas. La documentación de Agda es floja, instalarlo y ponerlo a funcionar es engorroso, y prácticamente te empuja a usar Emacs
      En cambio, Lean tiene en su propia documentación hasta cómo escribir una utilidad cat, y en general da una experiencia de tooling mucho más moderna
    • Me da curiosidad qué es exactamente lo bueno de Agda en programación funcional
      Normalmente los elogios van mucho por el lado del dependent pattern matching, y ahí sí siento que Lean es bastante débil
      Pero si aun así Agda te parece más amigable incluso para FP en general, me gustaría saber en qué sentido

  • Isabelle/HOL como lenguaje está bien, pero su tooling tiene fallas profundas incluso dejando de lado su enfoque centrado en escritorio
    El lenguaje no es tan distinto de Lean ni necesariamente mejor, y sí coincido con algunas críticas a los tipos dependientes
    Al final, ambos lenguajes hicieron trade-offs distintos, y esas decisiones parecen haberlos vuelto herramientas bastante eficaces en sus respectivos terrenos. El campo de las pruebas es tan amplio que cada paradigma tiene fortalezas y debilidades, y Lean simplemente se especializa en otra parte de ese espacio
    Sledgehammer está bien, pero parece cuestión de tiempo para que Lean tenga algo similar
    En la etapa de exploración puede ser útil, pero consume muchos recursos, y aunque acorta las pruebas, en código público prefiero que se vean directamente todos los pasos de la prueba en lugar de algo medio mágico como by sledgehammer
    En cambio, desarrollar Isabelle en sí es mucho más doloroso que Lean, y especialmente lo es el proceso de comunicarse con sus desarrolladores
    Esa actitud en la lista de correo de que no hay bugs, solo comportamientos no previstos me pareció infantil y poco profesional
    Y burlarse del uso de RAM de sistemas parecidos a Lean también da bastante risa cuando se ve el despilfarro de memoria del lado de Isabelle

    • El problema aquí es que convertir un certificado UNSAT en una forma que se pueda verificar rápido no es en absoluto algo trivial
      En la práctica, tiene una dificultad muy parecida a usar pruebas formales en sí
    • La última vez que revisé, recuerdo que Isabelle/HOL usaba como interfaz un modo personalizado de Emacs
      Aunque podría estar confundiéndolo con otro HOL
    • No sé qué sea Sledgehammer, pero por la descripción suena casi igual que grind de Mathlib
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Lo interesante de Lean es que Lean es un lenguaje, pero de lo que la gente suele hablar en realidad es de una biblioteca llamada Mathlib
    Los creadores de Mathlib parecen bastante pragmáticos, y por eso meten lógica clásica dentro de los tipos de Lean y usan la lógica intuicionista solo de forma parcial

    • El ejemplo dado al explicar el tercero excluido está mal
      “Algo no puede ser verdadero y falso al mismo tiempo” no es el tercero excluido sino la ley de no contradicción
      El tercero excluido significa que p es verdadero o not p es verdadero
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • La gente de ciencias de la computación ya está armando su propia CSLib
      https://www.cslib.io https://www.github.com/leanprover/cslib
      La lógica intuicionista tiene sentido esencialmente porque busca convertir argumentos matemáticos en construcciones computables, así que será interesante ver cómo manejan este tema
      De hecho, en cuanto escribes algoritmos en Lean ya entras, de una u otra forma, en restricciones constructivas, y para ese propósito ese nivel de lógica quizá sea suficiente
    • Me acordé del chiste de las cinco etapas de aceptar la matemática constructivista
      negación, ira, negociación, depresión, aceptación
      También valen la pena la charla y el texto relacionados de Andrej Bauer
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • Aquí lo correcto no sería intuitive logic sino intuitionistic logic
    • Aun con tantas restricciones y bloqueos, me da curiosidad cuándo y por qué alguien termina prefiriendo la lógica intuicionista

  • Creo que hacen falta más textos como este
    Incluso frente al pensamiento grupal de empujar como si fuera obvio eso de simplemente usa X, siempre hay razones al menos plausibles para examinar alternativas
    Aunque al final termines descartándolas y eligiendo lo dominante, sigue siendo mejor decidir conociendo el terreno

    • No estoy completamente de acuerdo
      Incluso hoy seguimos creando demasiados frameworks y alternativas, probablemente porque es divertido
      Muchas veces, en lugar de mejorar las herramientas existentes o simplemente avanzar con el trabajo real, se termina multiplicando sin fin lenguajes, bibliotecas y herramientas de build
      Creo que estaríamos mejor si hubiera solo la mitad de los lenguajes, bibliotecas y herramientas de build que existen hoy
    • Al final depende del contexto
      Cuanto más te alejas de lo dominante, menos documentación hay, más bugs aparecen en rincones menos explorados y menos gente tienes para ayudarte
      Cuando ya se acumulan más de veinte opciones, en promedio lo correcto es elegir la opción estándar y seguir adelante. La atención es limitada, y si haces un informe de investigación por cada dependencia, al final no resuelves el problema principal
      Hay dos excepciones: cuando la herramienta estándar de verdad no encaja con mi caso de uso, o cuando la herramienta estándar se cruza mucho con el problema central que intento resolver

  • Esta discusión me recuerda a los textos que señalan las limitaciones de Python para computación científica
    Cuando una comunidad alrededor de una herramienta razonablemente buena supera cierta masa crítica, eso termina pesando más que casi cualquier otro factor
    Se genera impulso, se acumulan tutoriales, explicaciones y mejor documentación, y en la práctica se llega a una especie de velocidad de escape
    Lean parece estar justo en esa posición ahora, incluso con el fuerte respaldo de alguien como Terrance Tao
    Por eso, decir que “el lenguaje X es mejor” no es totalmente falso, pero hace fácil perder de vista la pregunta importante
    La clave es si realmente es mejor que esa herramienta que todo el mundo conoce, puede usar de inmediato y a la que se le dedica más tiempo de mejora
    Al final, parece otro caso de worse is better, o de que si algo es bueno y popular, con eso basta

    • Me parece un buen punto que los LLM probablemente volverán bastante efectiva la traducción entre sistemas formales distintos
      Sobre todo porque en este campo el resultado traducido se puede verificar automáticamente en buena medida, así que la elección en sí quizá no sea un problema tan grande
    • Pero en la era de la IA la importancia de la masa crítica es mucho menor
      La IA puede escribir código por su cuenta aunque no exista una biblioteca comunitaria gigantesca, y puede leer directamente la documentación y las especificaciones aunque no haya un millón de tutoriales dando vueltas por internet
      Tampoco hace falta evitar lenguajes sin mercado laboral. La IA no está construyendo carrera, solo hace el trabajo que tiene enfrente
      Así que lenguajes pequeños y DSL que antes no habrían tenido oportunidad ahora tienen más espacio para ser adoptados
      Creo que la vieja monocultura de lenguajes en programación también podría terminarse por culpa de la IA

  • Decir que “casi todo lo formalizado hoy en cualquier sistema también podría haberse formalizado en AUTOMATH” se parece a decir que hoy todo lo que se programa en lenguajes modernos también podría haberse hecho en ensamblador hace 50 años
    Técnicamente es cierto, pero económicamente es otra historia por completo

    • Los lenguajes ensambladores suelen ser Turing completos, pero no tengo claro cuál sería exactamente la comparación equivalente del lado de los motores de prueba

  • Hace unos 15 años traté de probar Coq/Rocq y algunas otras herramientas, y más que los conceptos, lo difícil era entender el software mismo
    Lo raro de los asistentes de pruebas / demostradores interactivos de teoremas es que, por su naturaleza interactiva, el lenguaje y el IDE terminan acoplados, y en la práctica están fuertemente entrelazados
    Por eso cuesta hablar del lenguaje por separado; también hay que mirar en qué entorno se usa
    Yo tampoco soy un fanático de VS Code, pero está claro que un IDE extensible pulido por muchísima gente, usado por millones y respaldado con mucho dinero, va muy por delante del entorno de las alternativas
    Rutas de entrada tan buenas como Natural Numbers Game también parecen posibles gracias a la capacidad de hackeo y al ecosistema de VS Code
    Aun así, algo que me preocupa al aprender Lean es que la extensibilidad sintáctica sea un arma de doble filo
    Una vez que aprendes el lenguaje, quieres leer código escrito en él, pero si cada proyecto empieza a crear un montón de DSL propios, eso puede salirse de control
    Al final, esto depende de cuánta moderación tenga la comunidad y el ecosistema, así que lo veo con algo de entusiasmo pero también con cierta preocupación

  • Lean no es el asistente de pruebas más querido por los matemáticos, ni la mejor herramienta para la verificación formal de software
    Pero hace ambas cosas razonablemente bien y, a cambio, consiguió el impulso que es lo más difícil de obtener
    Además, en la era de la IA la cantidad de código escrito por humanos y disponible públicamente influye directamente en qué tan bien los agentes pueden generar código nuevo, así que ese impulso se vuelve todavía más fuerte