¿Por qué no usar simplemente Lean?

 (lawrencecpaulson.github.io)
1 puntos por GN⁺ 20 일 전 | 1 comentarios | Compartir por WhatsApp
  • La historia de la formalización matemática no empezó con Lean, y desde hace casi 60 años varios linajes de sistemas ya habían acumulado técnicas clave y resultados importantes
  • Herramientas como AUTOMATH de 1968, la familia LCF, HOL, Rocq, ACL2 y Mizar lograron una amplia gama de formalizaciones, 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 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 un proof assistant
  • Isabelle destaca por su automatización fuerte, alta legibilidad y por evitar los tipos dependientes, manteniendo la tradición LCF de construir la verificación de pruebas con la barrera de abstracción del kernel incluso sin proof objects
  • A medida que la IA también entra en el flujo de traducción de pruebas estructuradas entre distintos sistemas, la presión por ver una sola herramienta como estándar absoluto podría seguir disminuyendo

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, y trató desde lógica pura hasta la construcción de los números complejos
    • Usó clases de equivalencia y conjuntos de números racionales, y también demostró formalmente la completitud de Dedekind de la recta real
    • Este logro no volvió a verse en 20 años, y recién a mediados de los años 90 reapareció 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 ninguna automatización, por lo que las pruebas eran largas y difíciles de leer
    • Aun así, considera que en el manejo de clases de equivalencia era mejor que Rocq, y que, a diferencia del infierno de setoids que sufren los usuarios de Rocq, Jutting realizó la formalización de clases de equivalencia con calma y solidez

  • Boyer y Moore

La corriente posterior a LCF

  • Edinburgh LCF se centró en teoría de lenguajes de programación, pero la idea de usar un lenguaje funcional como metalenguaje de un asistente de pruebas se difundió ampliamente
  • Varios grupos en Cambridge, INRIA, Cornell y otros lugares usaron ML para crear herramientas como las primeras versiones de HOL, Coq (hoy Rocq) y Nuprl
  • El grupo HOL se concentró en la verificación de hardware, pero la verificación de hardware de punto flotante hizo necesaria el 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 solía ubicarse entre los primeros lugares
  • Hasta 2014, los sistemas de este linaje habían formalizado varios teoremas avanzados
  • En general, estos teoremas tenían pruebas largas y complejas, y el trabajo de formalización también fue de gran escala, cumpliendo un papel clave para reducir dudas que seguían presentes en los teoremas

El ascenso de la comunidad Lean

  • Los matemáticos consideraban que los logros previos de formalización no alcanzaban construcciones sofisticadas de la matemática moderna dominante como los Grothendieck schemes o los perfectoid spaces
  • Tom Hales eligió avanzar construyendo esas definiciones como biblioteca, enfocándose más en la acumulación de definiciones que en las pruebas, y optó por 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 la enseñanza, lo que aceleró luego su expansión
  • Como punto de inflexión importante de la comunidad Lean, se destaca que se alejó de la obsesión por la prueba constructiva que dominó durante mucho tiempo en Rocq
  • El intuicionismo surgió tras la paradoja de Russell y también tuvo implicaciones específicas sobre el concepto de número real
  • La teoría de tipos de Martin-Löf es claramente un formalismo intuicionista, pero se señala que Rocq no puede verse de forma tan simple
  • Aun así, en artículos relacionados con Rocq la prueba constructiva aparecía repetidamente incluso en contextos donde era irrelevante o carente de sentido, y se considera que esa tendencia frenó el uso matemático de Rocq y terminó cediendo espacio a Lean

propositions as types y la diferencia con LCF

  • Propositions as types es una dualidad que conecta los símbolos lógicos ∀, ∃, →, ∧, ∨ con los constructores de tipos Π, Σ, →, ×, +
  • Este marco es bello y teóricamente productivo, pero no es el único camino
  • Si se limita un proof assistant a software que verifica pruebas según el principio de propositions as types, gran parte de la investigación del último medio siglo queda fuera de la definición
  • En ese caso, solo quedarían Rocq, Lean y Agda
  • Incluso AUTOMATH no es un caso de propositions as types: aunque tiene elementos parecidos a Π y →, la lógica se establece como axiomas, como en un texto normal de lógica
  • De Bruijn ya veía hace 50 años la necesidad de separar tipos y proposiciones
  • Un ejemplo representativo es que la división debe recibir tres argumentos, y el valor de (x/y) dependería 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 lo mismo que propositions as types no corresponde a los hechos
  • Rocq y Lean tienen Prop, el sort de las proposiciones, donde todos los objetos de prueba de una misma proposición se evalúan como el mismo valor, aportando así proof irrelevance
  • Eso no significa que los enormes objetos de prueba desaparezcan; en el sistema real siguen estando ahí
  • El hallazgo central de Robin Milner fue que en LCF no hacen falta objetos de prueba en sí mismos
  • Si el kernel de prueba se coloca dentro de un tipo de datos abstracto de ML y las reglas de inferencia se usan como constructores, las pruebas pueden verificarse dinámicamente
  • Gracias a la abstraction barrier de ML, se considera imposible hacer trampa
  • Que términos gigantes ocupen decenas de MB aunque no indiquen nada resulta especialmente irracional en la era de RAMmageddon
  • También critica que incluso se siga investigando cómo volver más elegantes esos términos innecesarios

Razones para elegir Isabelle

  • Si tus colegas usan Lean, la especialización del equipo también está en Lean y las bibliotecas previas necesarias existen en Lean, lo natural es usar Lean
  • Aun así, si se puede elegir libremente, hay razones claras para considerar Isabelle

  • Automatización

    • Se destaca su automatización más potente, y sostiene que incluso comparado con los “hammer” de uso cotidiano, nada se compara con sledgehammer
    • Añade que el área de álgebra computacional también merece tratarse por separado

  • Legibilidad

  • Evitar tipos dependientes

    • Como no tiene tipos dependientes, evita niveles de universos y varias rarezas que complican la vida de 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 en sí misma se vuelve indecidible
    • Esto se debe a que la decisión de igualdad es indecidible, y se indica que al principio esto se aceptaba como algo natural
    • Desde alrededor de 1990, el consenso se movió hacia rebajar la igualdad a definitional/intensional equality para hacer decidible la verificación de tipos
    • Como resultado, (T(N+1)) y (T(1+N)) se convierten en tipos distintos
    • Estas limitaciones afectan las pruebas reales, y la verificación de definitional equality sigue teniendo una carga computacional considerable

Matemática moderna posible incluso sin tipos dependientes

Dirección futura e IA

  • Lean está acertando en muchas cosas y, al admitir incluso bloques de prueba anidados, potencialmente puede convertirse en un lenguaje de pruebas lo bastante legible
  • Ahora la comunidad Lean tiene que usar de verdad esas funciones, mientras que los usuarios de Isabelle ya suelen hacerlo
  • Más importante que un objeto de prueba verificable por computadora es la transparencia del texto de prueba que una persona realmente puede leer
  • El auge de la IA hace esta diferencia todavía más clara
  • Las pruebas creadas por IA suelen ser desordenadas, pero son fáciles de ordenar con sledgehammer, y si la estructura está bien planteada, incluso con exceso de detalle siguen siendo legibles
  • Eso facilita seguir el flujo del desarrollo y reducirlo luego a una forma más simple
  • Recientemente también apareció una investigación donde un modelo de lenguaje invoca directamente sledgehammer
  • La IA también podrá traducir con facilidad pruebas estructuradas y legibles de un proof assistant a otro
  • Si eso ocurre, se reducirá la carga misma de decidir qué sistema elegir

Corrección por 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 la omisión de Mizar y señala que en el próximo texto hablará de Mizar

Lecturas relacionadas

1 comentarios

 
GN⁺ 20 일 전
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