The readings shared in Bluesky on 13 June 2025 are

• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• Formal verification of relational algebra transformations in Fiat2 using Coq. ~ Christian Teshome. #ITP #CoqProver #Rocq
• Growing a modular framework for modal systems - HOLMS: a HOL Light library. ~ Antonella Bilotta. #ITP #HOL_Light #Logic #Math
• Trinity: an autoformalization system for verified superintelligence. #Autoformalization #AIforMath #ITP #LeanProver
• The abc conjecture almost always — autoformalized. ~ Jesse Michael Han et als. #Autoformalization #AIforMath #ITP #LeanProver
• MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems? ~ Zhitao He et als. #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath
• Mathesis: Towards formal theorem proving from natural languages. ~ Yu Xuejun et als. #AI #LLMs #Math #ITP #LeanProver #AIforMath
• StepProof: Step-by-step verification of natural language mathematical proofs. ~ Xiaolin Hu, Qinghua Zhou, Bogdan Grechuk, Ivan Y. Tyukin. #LLMs #ITP #IsabelleHOL #Math #AIforMath
• Reseña de «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?». #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath
• Reseña de «Mathesis: Towards formal theorem proving from natural languages». #AI #LLMs #Math #ITP #LeanProver #AIforMath

En el artículo «Mathesis: Towards formal theorem proving from natural languages», se aborda la limitación clave de los demostradores de teoremas: su dependencia de enunciados ya formalizados. El trabajo se centra en el paso crítico de la 'autoformalización' —la traducción a un lenguaje formal como Lean 4— y presenta Mathesis, un sistema integral diseñado para automatizar todo el proceso.

El sistema introduce un Mathesis-Autoformalizer entrenado mediante aprendizaje por refuerzo para optimizar la traducción a código Lean. Su rendimiento se evalúa con LeanScorer, y se pone a prueba en Gaokao-Formal, un nuevo y exigente banco de pruebas. Finalmente, Mathesis-Prover genera la demostración completa en Lean, asegurando que la prueba final sea verificable.

Los resultados demuestran que Mathesis alcanza un rendimiento de vanguardia en varios bancos de prueba. El análisis revela una conclusión crucial: las mejoras en la autoformalización impactan el éxito final mucho más que las mejoras en el demostrador. Esto se explica porque si el problema se traduce incorrectamente a código Lean, el demostrador recibe una tarea mal planteada y no puede generar una prueba válida, sin importar su potencia. El trabajo confirma así que una traducción inicial de alta calidad es el factor más determinante para el éxito del proceso.

En el artículo «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?», los autores investigan la aplicabilidad de los modelos de lenguaje grandes multimodales (MLLMs) al problema de la demostración automática de teoremas que involucran componentes tanto textuales como visuales. Motivados por las limitaciones de los enfoques puramente textuales en dominios como la geometría, donde los diagramas constituyen información esencial, desarrollan un marco de evaluación sistemático para esta clase de problemas.

La contribución principal consiste en la construcción de MATP-BENCH, un conjunto de datos que contiene más de 1000 problemas matemáticos multimodales formalizados en tres asistentes de demostración: Lean 4, Coq e Isabelle/HOL. El corpus abarca problemas de complejidad variable, desde el nivel de secundaria hasta competiciones matemáticas avanzadas, proporcionando así un banco de pruebas comprehensivo para evaluar capacidades de razonamiento multimodal.

Los experimentos incluyen seis modelos representativos: tres con capacidades especializadas de razonamiento (OpenAI-o1, Claude-3.7-Sonnet-Thinking, Gemini-2.0-Flash-Thinking) y tres sin estas capacidades (GPT-4.1, Qwen2.5-VL-Instruct-70B, Llama3.2-Vision-Instruct-11B). Los resultados revelan que, si bien los modelos demuestran competencia en la comprensión de problemas y formalización de enunciados, exhiben deficiencias significativas en la construcción de cadenas de inferencia válidas.

El análisis establece que la principal limitación no radica en las capacidades de percepción visual sino en la insuficiencia del razonamiento simbólico formal. Los autores concluyen que los MLLMs actuales no constituyen demostradores automáticos efectivos para problemas multimodales, identificando la brecha entre comprensión multimodal y razonamiento lógico como el desafío fundamental a resolver.

MATP-BENCH se posiciona como el primer banco de prueba estándar para este dominio, proporcionando una base metodológica para la evaluación de futuros desarrollos en demostración automática multimodal.

The readings shared in Bluesky on 12 June 2025 are

• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• Lean meta-theory: The proofs behind the proofs. ~ Mario Carneiro. #ITP #LeanProver
• Litex: Scale formal reasoning in AI age. ~ Jiachen Shen. #Logic #ATP #LitexLang
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #ITP #LeanProver #LLMs
• Can large language models verify system software? A case study using FSCQ as a benchmark. ~ Jianxing Qin et als. #LLMs #ITP #CoqProver #Rocq
• Reinventing records and variants. ~ Murat Kasimov. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 11 June 2025 are

• LeanTutor: A formally-verified AI tutor for mathematical proofs. ~ Manooshree Patel et als. #ITP #LeanProver #Math #AIforMath #Teaching
• Common Lean pitfalls. ~ Niels Voss. #ITP #LeanProver
• Rewriting SymCrypt in Rust to modernize Microsoft’s cryptographic library. ~ Brenda Potts. #ITP #LeanProver #RustLang
• Z3Guide: A scalable, student-centered, and extensible educational environment for logic modeling. ~ Ruanqianqian Huang, Ayana Monroe, Peli de Halleux, Sorin Lerner, Nikolaj Bjørner. #Logic #SMT #Z3 #Teaching
• Martin Davis: An overview of his work in logic, computer science, and philosophy. ~ Liesbeth De Mol, Yuri V. Matiyasevich, Eugenio G. Omodeo, Alberto Policriti, Wilfried Sieg, Elaine J. Weyuker. #Logic #Math #CompSci
• El futuro del razonamiento matemático: Integrando IA y Lean. #IA #ITP #LeanProver #Math #AIforMath
• Reseña de 'LeanTutor: A formally-verified AI tutor for mathematical proofs'. #ITP #LeanProver #Math #AIforMath #Teaching

El artículo "LeanTutor: A formally-verified AI tutor for mathematical proofs" aborda un problema común en la educación matemática: los estudiantes tienen dificultades para aprender demostraciones. Actualmente existen dos tipos de herramientas, pero ninguna funciona bien para enseñar. Los chatbots como ChatGPT son fáciles de usar pero dan respuestas directas o incorrectas, sin ayudar realmente al aprendizaje. Los asistentes de demostración como Lean verifican las matemáticas perfectamente, pero son demasiado complicados para principiantes. Se necesita una herramienta que combine lo mejor de ambos: la facilidad del lenguaje natural y la precisión de la verificación formal.

Los autores crearon LeanTutor, un sistema que funciona como tutor inteligente combinando lenguaje natural con verificación formal. El sistema tiene tres partes que trabajan juntas. Primero, el 'autoformalizador' toma lo que escribe el estudiante en lenguaje normal y lo convierte a código Lean para verificar si es correcto. Si hay un error, el 'generador del siguiente paso' calcula cuál sería la respuesta correcta. Finalmente, el 'generador de retroalimentación' convierte esta información técnica en consejos útiles para el estudiante, dándole pistas sin revelar directamente la solución.

Los investigadores probaron LeanTutor usando un nuevo conjunto de datos llamado PeanoBench y los resultados fueron positivos. El sistema logró convertir correctamente la mayoría de los pasos que escribían los estudiantes y detectó muchos errores. Cuando compararon la retroalimentación de LeanTutor con otros sistemas, encontraron que era más precisa y útil para los estudiantes. Los autores concluyen que este enfoque de combinar IA conversacional con verificación formal es una buena dirección para crear mejores herramientas educativas.

Este trabajo presenta una idea muy buena para mejorar la educación matemática. La principal fortaleza es que logra combinar de manera inteligente la facilidad de uso del lenguaje natural con la precisión matemática de Lean. Sin embargo, también tiene algunas limitaciones importantes. El sistema necesita tener de antemano la solución correcta del problema, y asume que los pasos del estudiante se pueden traducir directamente a código Lean, lo que podría no funcionar en situaciones más complejas. A pesar de estas limitaciones, LeanTutor es un buen primer paso que muestra cómo la IA puede ayudar a enseñar matemáticas de forma más efectiva y segura.

En su conferencia "Will computers prove theorems?", Kevin Buzzard plantea que los ordenadores ya demuestran teoremas, pero la pregunta crucial es cómo pueden transformar la investigación matemática. Aunque reconoce la utilidad de las herramientas actuales como las redes neuronales para identificar patrones, su aplicación permanece limitada. Los modelos de lenguaje como ChatGPT, por su parte, pueden ofrecer ideas valiosas, pero fracasan rotundamente en el razonamiento lógico: tienden a "alucinar" o inventar detalles para parecer convincentes, lo que los convierte en herramientas poco confiables para las matemáticas rigurosas.

La solución que propone Buzzard para superar estas limitaciones radica en la sinergia entre la inteligencia artificial y los asistentes de demostración formal como Lean. Su propuesta consiste en entrenar modelos de IA para que generen pruebas directamente en código de Lean, en lugar de utilizar lenguaje natural. De este modo, el asistente de demostración funciona como un verificador infalible: cualquier argumento lógicamente incorrecto será rechazado automáticamente por el sistema. Esta metodología obligaría a la IA a evolucionar desde la mera imitación de patrones hacia la construcción de razonamientos lógicamente verificables.

No obstante, el principal obstáculo para materializar esta visión es la escasez de matemáticas modernas y avanzadas formalizadas en Lean, elementos esenciales para el entrenamiento de estos modelos. Buzzard concluye con un llamamiento directo a la comunidad matemática: considera que es responsabilidad de los investigadores emprender la tarea fundamental de formalizar el conocimiento de sus respectivos campos, tal como él mismo está haciendo con el último teorema de Fermat. Argumenta que este esfuerzo resulta crucial para desarrollar las herramientas que revolucionarán la disciplina, a pesar de que el sistema académico actual no reconozca ni recompense adecuadamente este tipo de contribuciones.

The readings shared in Bluesky on 10 June 2025 are

• Inductive definitions. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• The equational theories project: advancing collaborative mathematical research at scale. ~ Terence Tao et als. #ITP #LeanProver #Math #AIforMath
• New AI stuns mathematicians with its problem-solving skill. ~ David H Bailey. #AI #LLMs #Math #AIforMath #ITP #LeanProver
• Premise selection for a Lean hammer. ~ Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, Sean Welleck. #ITP #LeanProver #AI
• Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification. ~ Chengwu Liu et als. #LLMs #Math #ITP #LeanProver
• AlphaProof: When RL meets formal maths. ~ Thomas Hubert. #AI #Math #AIforMath #ITP #LeanProver #AlphaProof
• AI for Math: The future of collaborative discovery. ~ Mateja Jamnik. #AIforMath
• Are LLMs reliable translators of logical reasoning across lexically diversified contexts? ~ Qingchuan Li et als. #LLMs #Math #ATP #Prover9
• Dr. Neckbeard, or how I learned to stop worrying and love Emacs. ~ Watts Martin. #Emacs
• Revistas, editoriales y congresos depredadores. #Investigación
• AlphaProof: Aprendizaje por refuerzo aplicado a la demostración matemática. #AI #Math #AIforMath #ITP #LeanProver #AlphaProof
• El futuro de las matemáticas: Descubrimiento colaborativo entre humanos y máquinas. #AIforMath #AI #Math
• El proyecto ETP (Un caso de estudio en investigación matemática colaborativa y formalizada). #AIforMath #ITP #LeanProver #Math

Hoy, en su conferencia "The equational theories project", Terence Tao defendió que la investigación matemática debe evolucionar hacia un modelo colaborativo a gran escala, semejante al empleado en otras disciplinas científicas. Esta transformación requiere el uso de herramientas modernas como plataformas colaborativas (GitHub), asistentes de prueba formales (Lean) y automatización mediante inteligencia artificial. El proyecto ETP (Equational Theories Project) constituye un ejemplo paradigmático de esta nueva aproximación a la investigación matemática.

El proyecto nació de una pregunta aparentemente simple planteada en el foro MathOverflow, pero pronto adquirió una dimensión extraordinaria: mapear completamente el "gráfico de implicaciones" entre 4,692 leyes algebraicas únicas dentro de estructuras elementales denominadas magmas. Esta ambiciosa meta implicaba resolver más de 22 millones de problemas individuales, donde cada par de leyes requería encontrar una prueba de implicación o desarrollar un contraejemplo que la refutara. La magnitud descomunal de este desafío lo convertía en una tarea imposible de abordar mediante los métodos tradicionales de investigación individual o de pequeños equipos.

La estrategia implementada por el ETP consistió en un flujo de trabajo híbrido y descentralizado de notable innovación. La componente humana aprovechó la creatividad de una extensa comunidad de colaboradores para desarrollar pruebas y contraejemplos ingeniosos, mientras que la componente computacional empleó masivamente probadores automáticos de teoremas (ATPs) y otras herramientas para resolver millones de casos más directos. El elemento fundamental que garantizó la integridad del proyecto fue la formalización exhaustiva de cada resultado en el asistente de pruebas Lean, asegurando una corrección absoluta y creando una base de conocimiento completamente verificada y confiable.

En el plazo extraordinariamente breve de tres meses, el proyecto logró resolver prácticamente la totalidad de los 22 millones de problemas planteados. Además, el proceso de abordar los casos más complejos estimuló el desarrollo de técnicas matemáticas innovadoras, culminando con la formulación de un nuevo y fascinante problema abierto. El ETP demostró que este modelo colaborativo trasciende la mera verificación de conocimiento existente para convertirse en un motor poderoso de descubrimiento matemático, estableciendo así un precedente exitoso para una investigación matemática más abierta, transparente y asistida computacionalmente.

Ayer, en su conferencia "AI for Math: The future of collaborative discovery", Mateja Jamnik presentó una visión de la inteligencia artificial no como una simple herramienta para resolver problemas, sino como un socio colaborativo en el descubrimiento matemático. Su trabajo explora cómo las máquinas pueden proponer ideas y acelerar la investigación. A través de un estudio empírico con matemáticos, demostró que la interacción humano-IA es compleja; una respuesta de la IA no necesita ser perfectamente correcta para ser útil, ya que incluso ideas parcialmente erróneas pueden inspirar nuevas vías de pensamiento, mientras que respuestas correctas pero verbosas pueden resultar inútiles.

El núcleo técnico de su propuesta, materializado en trabajos como su artículo "Draft, sketch, and prove: Guiding formal theorem provers with informal proofs", es un ciclo auto-mejorable que integra el vasto conocimiento matemático informal. A través de la arquitectura ‘Borrador, Esquema y Prueba’ descrita en dicho artículo, la IA traduce pruebas humanas a un formato formal y riguroso. Este ciclo culmina en un sistema ‘conjeturador-demostrador’ que genera progresivamente nuevas conjeturas, las evalúa según su capacidad para ayudar a resolver problemas más difíciles y utiliza las mejores para mejorar continuamente, acercándose así a la resolución de teoremas que antes eran inaccesibles.

El objetivo final es integrar plenamente al ser humano en este ciclo de descubrimiento. Jamnik imagina un futuro donde los matemáticos interactúen con este sistema para proponer y evaluar conjeturas, guiando la dirección de la investigación. Su conclusión es que la IA no reemplazará a los matemáticos, sino que los potenciará, creando una sinergia entre la intuición humana y la capacidad de la máquina. El futuro de las matemáticas, según su visión, es una era de descubrimiento colaborativo entre humanos y máquinas.