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.

En su conferencia de ayer "AlphaProof: When RL meets formal maths", Thomas Hubert de Google DeepMind presentó AlphaProof, un sistema de inteligencia artificial que aplica los principios del aprendizaje por refuerzo (RL, del inglés "Reinforcement learning") al dominio de las matemáticas formales. El concepto fundamental radica en que los asistentes de demostración como Lean proporcionan el entorno perfecto para el RL: un espacio de experimentación masiva con retroalimentación inequívoca (una prueba matemática es correcta o incorrecta, sin ambigüedades). Siguiendo el paradigma exitoso de sistemas como AlphaGo Zero, AlphaProof está diseñado para generar conocimiento matemático de forma autónoma, trascendiendo la mera imitación de demostraciones humanas preexistentes.

La arquitectura de AlphaProof se estructura en un proceso de múltiples fases que combina diferentes técnicas de aprendizaje automático. Inicialmente, emplea modelos de lenguaje para autoformalizar problemas matemáticos expresados en lenguaje natural hacia el código formal de Lean, generando así un extenso conjunto de datos de entrenamiento. Su modelo demostrador experimenta dos etapas: primero, un entrenamiento supervisado utilizando la biblioteca mathlib, seguido de un refinamiento intensivo mediante RL que resuelve millones de problemas matemáticos. Para desafíos particularmente complejos —como los de la Olimpiada Internacional de Matemáticas (IMO)—, el sistema implementa una estrategia de adaptación en tiempo real, generando y resolviendo múltiples variantes de un problema para desarrollar gradualmente la intuición necesaria.

Los resultados validan el potencial transformador de AlphaProof como herramienta matemática colaborativa. El sistema alcanzó una puntuación equivalente a una medalla de plata en la IMO y, durante una demostración en vivo durante la conferencia, asistió exitosamente a un matemático a completar los pasos de una prueba compleja relacionada con la función zeta de Riemann. Hubert enfatiza que el objetivo trasciende las competiciones académicas: la meta fundamental es contribuir significativamente a la investigación matemática contemporánea, convirtiendo AlphaProof en una útil para la comunidad matemática que facilite el descubrimiento y verificación de nuevas verdades matemáticas.

The readings shared in Bluesky on 9 June 2025 are

• Formalizing invisible mathematics: case studies from higher category theory. ~ Emily Riehl. #ITP #LeanProver #Math #CategoryTheory
• Sequencelib: A platform for formalizing in Lean 4 sequences from "The On-Line Encyclopedia of Integer Sequences" (OEIS). ~ Walter Moreira, Joe Stubbs. #ITP #LeanProver #Math
• At secret math meeting, researchers struggle to outsmart AI. ~ Lyndie Chiou. #AIforMath #AI #LLMs #Math
• Comparing code: Spatial reasoning with zigzag patterns! ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Exploring topological spaces with Prolog: A practical approach using "Mathematics with Prolog". ~ Kenichi Sasagawa. #Prolog #LogicProgramming #Math
• Teaching and learning mathematics with Prolog. ~ Tom Bensky (2021). #Prolog #LogicProgramming #Math
• Evaluando la IA con problemas matemáticos inéditos de nivel experto. #AIforMath #AI #LLMs #Math
• Curso "Lógica informática (2012-13)". #Lógica #ProgramaciónLógica #Prolog
• Curso "Lógica matemática y fundamentos (2012-13)". #Lógica #Haskell #ProgramaciónFuncional #Isabelle/HOL

El artículo Inside the secret meeting where mathematicians struggled to outsmart AI documenta una reunión extraordinaria celebrada en Berkeley a mediados de mayo de 2025, donde treinta de los matemáticos más prestigiosos del mundo se enfrentaron en un duelo intelectual contra o4-mini, el avanzado modelo de razonamiento de OpenAI, en un desafío organizado por Epoch AI bajo el nombre FrontierMath. La misión parecía clara: crear problemas de investigación de nivel de doctorado que los humanos pudieran resolver pero que resultaran infranqueables para la inteligencia artificial. Sin embargo, los participantes experimentaron una sorpresa mayúscula al descubrir que el sistema resolvía algunos de los problemas más complejos que le presentaron, exhibiendo una capacidad de razonamiento que trascendió todas sus expectativas.

La extraordinaria destreza del sistema quedó vívidamente ilustrada en la experiencia del matemático Ken Ono, quien presenció cómo o4-mini resolvía un problema abierto de nivel de doctorado en apenas diez minutos: primero exploró sistemáticamente la literatura especializada, después resolvió una versión simplificada como ejercicio de "aprendizaje", y finalmente presentó una solución rigurosa al desafío principal. Este enfoque metodológico, que Ono caracterizó como propio del razonamiento científico auténtico, no fue un caso aislado, ya que el grupo logró formular únicamente diez problemas que resistieron los embates de la IA, subrayando la eficacia abrumadora del sistema.

El encuentro concluyó con una profunda reflexión sobre las transformaciones que se avecinan en el campo matemático. Entre las preocupaciones emergentes destacó el fenómeno de la "prueba por intimidación": la tendencia a aceptar los resultados de la IA sin el escrutinio riguroso tradicional. La conclusión consensuada apunta hacia una metamorfosis radical en el rol del matemático profesional, que evolucionará desde el tradicional "solucionador de problemas" hacia una nueva función como "formulador de preguntas estratégicas" que colabora y orienta el potencial de la inteligencia artificial. Como advirtió Ono, subestimar estas herramientas constituye un grave error, dado que ya están superando el rendimiento de los estudiantes de posgrado más talentosos del mundo.

The readings shared in Bluesky on 8 June 2025 are

• The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity. ~ Parshin Shojaee et als. #LLMs #Reasoning
• Más allá de la "ilusión de pensar". #LLMs #Reasoning #Math #ITP #LeanProver
• AutoGPS: Un sistema neuro-simbólico para la geometría. #AI #Math
• Curso "Informática (2012-13)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima

El artículo AutoGPS: Automated Geometry Problem Solving via Multimodal Formalization and Deductive Reasoning presenta AutoGPS, un sistema paradigmático para la geometría. Este trabajo aborda la dicotomía fundamental entre los modelos neuronales, que destacan en la interpretación multimodal pero carecen de fiabilidad lógica, y los métodos simbólicos, que garantizan el rigor pero son ineficaces para formalizar problemas a partir de entradas complejas. AutoGPS resuelve este dilema mediante un marco neuro-simbólico: un formalizador de problemas multimodales (MPF) traduce la entrada visual y textual a un lenguaje lógico, sobre el cual opera un razonador simbólico deductivo (DSR) para derivar la solución.

La innovación crucial reside en la interacción bidireccional entre ambos componentes. El DSR no se limita a resolver el problema formalizado, sino que actúa como un verificador, validando la interpretación del MPF y pudiendo solicitarle correcciones. Este bucle de retroalimentación garantiza la consistencia lógica de todo el proceso, fusionando la capacidad heurística del modelo neuronal con el rigor inflexible del razonamiento deductivo.

Como resultado, AutoGPS establece un nuevo estado del arte en los benchmarks de referencia, produciendo derivaciones que no solo son correctas, sino también concisas y legibles para un humano. De este modo, redefine el estándar de fiabilidad e interpretabilidad en la resolución automática de problemas matemáticos. La página del proyecto ofrece ejemplos ilustrativos de su funcionamiento.

Un reciente artículo de investigadores de Apple, titulado "The illusion of thinking: A survey of the state of the art in Large Language Models", postula que las impresionantes capacidades de los Grandes Modelos de Lenguaje (LLMs) no derivan de una comprensión o razonamiento genuino, sino de una sofisticada imitación de patrones estadísticos extraídos de vastos corpus de datos. Esta "ilusión de pensar" se vuelve particularmente manifiesta en dominios que exigen una lógica estricta y verificable, como las matemáticas formales. En este campo, la propensión de los LLMs a la "alucinación" y su inherente falta de un modelo causal del mundo limitan fundamentalmente su fiabilidad, incapacitándolos para producir razonamientos complejos de manera autónoma y garantizada.

Para abordar esta limitación estructural, la investigación contemporánea ha centrado sus esfuerzos en el desarrollo de arquitecturas híbridas neuro-simbólicas. Dichos sistemas implementan una división funcional del trabajo computacional: el componente neuronal (el LLM) opera como interfaz de alto nivel, encargado de procesar entradas en lenguaje natural y generar estrategias heurísticas preliminares. Estas propuestas son luego transferidas a un módulo simbólico —ya sea un sistema de cálculo algebraico exacto o un demostrador de teoremas— que actúa como verificador formal. Este último componente, regido por reglas lógicas inflexibles, examina cada inferencia producida por el LLM, proporcionando retroalimentación inmediata y garantizando la corrección deductiva del proceso.

La eficacia de este paradigma ha sido demostrada empíricamente por sistemas de última generación diseñados para resolver problemas de la Olimpiada Internacional de Matemáticas (IMO). Tal como se documenta en el estudio AI achieves silver-medal standard solving International Mathematical Olympiad problems, estas plataformas combinan un LLM encargado de la generación inicial de hipótesis con herramientas especializadas como AlphaProof, un sistema optimizado para demostrar enunciados matemáticos en el lenguaje formal de Lean. Cabe destacar que Lean, lejos de ser una mera herramienta auxiliar, constituye un componente estructural en estos sistemas: su integración permite traducir la capacidad heurística de los LLMs a un marco verificable formalmente. Esta sinergia entre la creatividad inductiva de los modelos neuronales y el rigor de los sistemas simbólicos representa el estado del arte en la construcción de inteligencias artificiales capaces de razonamiento matemático formalmente validable.

The readings shared in Bluesky on 7 June 2025 are

• The bizarre story of a maths proof that is only true in Japan. ~ Jacob Aron. #Math
• La disputa sobre la conjetura abc y el papel de la verificación formal. #Matemáticas #ITP #LeanProver

Leibniz soñaba con un sistema de razonamiento formal, su "Calculemus", que permitiría resolver disputas simplemente diciendo "calculemos". Hoy, esta idea cobra especial relevancia en el centro de una de las controversias más extrañas de las matemáticas modernas, la detallada en el artículo de New Scientist "The bizarre story of a maths-proof that is only true in Japan". El artículo describe cómo la prueba de la conjetura abc del matemático Shinichi Mochizuki, basada en su compleja teoría de Teichmüller Interuniversal (IUT), ha dividido a la comunidad. A pesar de haber sido publicada formalmente en Japón, la mayoría de los matemáticos internacionales la rechazan, siguiendo la crítica de expertos como Peter Scholze que señalan un supuesto "error fatal", creando una división geográfica sin precedentes sobre la validez de un resultado matemático.

La razón de este intenso escrutinio reside en el inmenso poder de la propia conjetura abc. Esta establece una conexión profunda entre la suma y la multiplicación de números enteros, postulando que para tres números coprimos a + b = c, el valor de c es casi siempre más pequeño que el "radical" del producto a*b*c (el producto de sus factores primos únicos). Si se demostrara, la conjetura actuaría como una "piedra Rosetta" para la teoría de números, resolviendo de un plumazo una multitud de otros problemas famosos, como el último teorema de Fermat, lo que justifica la frustración y el interés global por resolver esta disputa de una vez por todas.

Para resolver el impasse y cumplir el sueño de Leibniz, la solución definitiva sería utilizar un asistente de pruebas formal como Lean, un software que puede verificar la lógica de una demostración con certeza absoluta, eliminando la ambigüedad humana. Sin embargo, formalizar la novedosa y compleja IUT de Mochizuki es una tarea monumental, considerada casi imposible hoy en día. A pesar de ello, la comunidad de Lean está dando pasos cruciales. Proyectos como Exceptional set in the abc conjecture de Jared Duker Lichtman y Bhavik Mehta no verifican la prueba directamente, pero sí formalizan el enunciado del problema y desarrollan las herramientas y la experiencia necesarias. Estos esfuerzos sientan las bases para que, quizás algún día, esta extraordinaria disputa matemática pueda finalmente ser resuelta mediante el cálculo.

The readings shared in Bluesky on 6 June 2025 are

• Big steps in higher-order mathematical operational semantics. ~ Sergey Goncharov, Pouya Partow, Stelios Tsampas. #Haskell #FunctionalProgramming
• Libro "Matemáticas en Lean4" (versión del 6-junio-25). #ITP #Lean4 #Math

El artículo What's next for AI and math, publicado ayer, examina la transformación que la inteligencia artificial está generando en el ámbito matemático. La iniciativa expMath (Exponentiating Mathematics) de DARPA busca revolucionar el progreso matemático mediante una IA coautora capaz de abordar problemas de alta complejidad. Aunque los modelos de lenguaje grandes (LLMs) han demostrado un rendimiento excepcional en problemas de nivel escolar y universitario —superando frecuentemente a los humanos en exámenes como la AIME (American Invitational Mathematics Examination)— estos sistemas operan principalmente siguiendo patrones previamente establecidos. No obstante, cuando se enfrentan a desafíos de investigación abiertos y sin precedentes, como los planteados en el nuevo test FrontierMath, las limitaciones actuales de la IA se manifiestan claramente, revelando una brecha considerable entre las capacidades actuales y la resolución de problemas del calibre de la Hipótesis de Riemann.

Pese a estas limitaciones, la IA está realizando contribuciones significativas al asistir a los matemáticos en la exploración de nuevos enfoques y la identificación de rutas prometedoras. Herramientas como AlphaEvolve y PatternBoost han sido específicamente diseñadas para generar hipótesis, evaluar soluciones potenciales y descartar aproximaciones infructuosas, optimizando así el tiempo de investigación. Paralelamente, se están desarrollando metodologías para simplificar las complejas secuencias de pasos requeridas para resolver problemas de extrema dificultad, como se evidenció en el reciente avance relacionado con la conjetura de Andrews-Curtis.

Sin embargo, la intuición profunda y la creatividad conceptual que caracterizan a los grandes descubrimientos matemáticos permanecen como dominios esencialmente humanos. En este contexto, la IA funciona como una herramienta potente que complementa y amplifica la investigación matemática, pero la chispa de genialidad —esa capacidad de "pensar fuera de los marcos establecidos"— continúa siendo patrimonio exclusivo de la mente humana.

The readings shared in Bluesky on 5 June 2025 are

• Exceptional set in the abc conjecture (in Lean). ~ Jared Duker Lichtman, Bhavik Mehta. #ITP #LeanProver #Math
• IDE for validating specifications. ~ Evan Miyazono, Daniel Windham, Alexandre Rademaker. #ITP #LeanProver
• Faithful logic embeddings in HOL — Deep and shallow (Isabelle/HOL dataset). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• A verified reduction algorithm from MLSSmf to MLSS. ~ Yiran Duan, Lukas Stevens. #ITP #IsabelleHOL #Math
• David Poole on knowledge graphs and relational learning. #AI #LogicProgramming
• IA y matemáticas (presente y futuro). #IA #Matemáticas

The readings shared in Bluesky on 4 June 2025 are

• Mathematics in Lean (Release v4.19.0). ~ Jeremy Avigad, Patrick Massot. #ITP #LeanProver #Math
• Functional programming in Lean. ~ David Thrane Christiansen. #ITP #LeanProver #FunctionalProgramming
• The concept of definition: in mathematics, and in computational logic. ~ Lawrence Paulson. #Logic #Math #ITP

Una noticia publicada por Cadena SER presenta una predicción sobre el futuro de la enseñanza de las matemáticas, planteando que su práctica tradicional podría transformarse radicalmente debido al avance de la inteligencia artificial (IA). La tecnología tendría la capacidad de realizar gran parte de las tareas matemáticas que actualmente resuelven los estudiantes.

Esta perspectiva se enmarca dentro de un debate más amplio sobre la evolución del sistema educativo, tal como se analiza en el Informe GoStudent sobre el Futuro de la Educación 2025. El documento subraya la necesidad urgente de modernizar los métodos pedagógicos, ya que los enfoques tradicionales no se alinean adecuadamente con las exigencias del entorno tecnológico y socioeconómico actual.

El informe recomienda integrar competencias emergentes en el currículo educativo, como inteligencia artificial, ciberseguridad y pensamiento crítico. Aunque se reconoce el potencial transformador de la IA en educación, su implementación avanza de forma lenta y desigual, particularmente en la capacitación docente.

Respecto a la enseñanza de las matemáticas, este escenario sugiere una reorientación metodológica fundamental: abandonar el enfoque centrado en el cálculo mecánico para privilegiar la comprensión conceptual profunda, complementada con el uso estratégico de herramientas tecnológicas e inteligencia artificial como apoyo al razonamiento matemático.

The readings shared in Bluesky on 3 June 2025 are

• Project Numina and AI for Theorem Proving. ~ Yann Fleureau. #AI #Math #ITP #LeanProver
• Restriction spaces: a fixed-point theory (in Isabelle/HOL). ~ Benoît Ballenghienm, Benjamin Puyobro, Burkhart Wolff. #ITP #IsabelleHOL
• Automated symmetric constructions in discrete geometry. ~ Bernardo Subercaseaux, Ethan Mackey, Long Qian, Marijn J. H. Heule. #ATP #SAT_Solvers #Math
• Coalgebraic proof translations for non-wellfounded proofs. ~ Borja Sierra Miranda, Thomas Studer, Lukas Zenger. #Logic #Math
• 25 Useful tips for Emacs (for beginners and advanced users). ~ Raoul Comninos. #Emacs
• Debate sobre IA y enseñanza de las matemáticas. #IA #Matemáticas

The readings shared in Bluesky on 2 June 2025 are

• Regex decision procedures in extended RE#. ~ Ian Erik Varatalu et als. #ITP #LeanProver
• Learn physics with functional programming. ~ Esteban Marin. #Haskell #FunctionalProgramming #Physics

The readings shared in Bluesky on 1 June 2025 are

• A Lean companion to "Analysis I". ~ Terence Tao. #ITP #LeanProver #Math
• AutoGPS: Automated geometry problem solving via multimodal formalization and deductive reasoning. ~ Bowen Ping et als. #MathAI
• An infinitely large napkin. ~ Evan Chen. #Math

The readings shared in Bluesky on 31 May 2025 are

• Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. ~ Viviana del Barco et als. #ITP #LeanProver #Math
• Lean4Lean: Mechanizing the metatheory of Lean. ~ Mario Carneiro. #ITP #LeanProver
• HoTTLean: Formalizing the meta-theory of HoTT in Lean. ~ Joseph Hua et als. #ITP #LeanProver #HoTT
• Towards modular composition of inductive types using Lean meta-programming. ~ Ramy Shahin. #ITP #LeanProver
• Löb’s theorem and provability predicates in Rocq. ~ Janis Bailitis1, Dominik Kirst, Yannick Forster. #ITP #Rocq #Logic #Math
• A Coq formalization of Lagois connections for secure information flow. ~ Casper Stahl et als. #ITP #Coq #Rocq
• Verifying Z3 RUP proofs with the interactive theorem provers Coq/Rocq and Agda. ~ Harry Bryant et als. #ITP #Coq #Rocq #Agda
• Efficient program extraction in elementary number theory using the proof assistant Minlog. ~ Franziskus Wiesnet. #ITP #Minlog #Haskell #FunctionalProgramming #Math

The readings shared in Bluesky on 30 May 2025 are

• Certified algorithms for numerical semigroups in Rocq. ~ Massimo Bartoletti, Stefano Bonzio, Marco Ferrara. #ITP #Rocq #Math
• Agent-based logics in dependent type theory. ~ Colm Baston. #ITP #Agda
• RocqStar: Leveraging similarity-driven retrieval and agentic systems for Rocq generation. ~ Nikita Khramov, Andrei Kozyrev, Gleb Solovev, Anton Podkopaev. #ITP #Rocq #GenerativeAI
• VERINA: Benchmarking verifiable code generation. ~ Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, Dawn Song. #AIforCode #ITP #LeanProver

The readings shared in Bluesky on 29 May 2025 are

• Geometric reasoning in Lean: from algebraic structures to presheaves. ~ Kenji Maillard, Yiming Xu. #ITP #LeanProver #Math
• Construire des preuves mathématiques. ~ Thierry Coquand, William Rowe-Pirra. #ITP #Coq
• Formalizing colimits in Cat. ~ Mario Carneiro, Emily Riehl. #ITP #LeanProver
• A collection of formalized statements of conjectures in Lean, using Mathlib. #ITP #LeanProver #Math
• A formal analysis of algorithms for matroids and greedoids. ~ Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa. #ITP #IsabelleHOL
• Kimina: Interactive mathematical proof assistant. #AI #ITP #LeanProver #Math
• Context-free grammars and languages (in Isabelle/HOL). ~ Tobias Nipkow et als. #ITP #IsabelleHOL
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, Axel Ljungström. #ITP #Agda
• Mechanized safety of Jolteon consensus in Agda. ~ Orestis Melkonian, Mauro Jaskelioff, and James Chapman. #ITP #Agda
• Implementing Löb’s theorem in Emacs Lisp. ~ John Wiegley. #Emacs #Lisp #Logic #Math

The readings shared in Bluesky on 28 May 2025 are

• Formalizing Fermat: an update. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Algebraic geometry in Mathlib. ~ Andrew Yang. #ITP #LeanProver #Math
• REAL-Prover: Retrieval augmented Lean prover for mathematical reasoning. ~ Ziju Shen et als. #AI #TheoremProving #LeanProver #Math
• Faithful logic embeddings in HOL (Deep and shallow). ~ Christoph Benzmüller. #ITP #TheoremProving #IsabelleHOL #Logic #Math

The readings shared in Bluesky on 27 May 2025 are

• Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. ~ Viviana del Barco, Gustavo Infanti, Exequiel Rivas, Paul Schwahn. #ITP #LeanProver #Math
• Simprocs for the working mathematician. ~ Yaël Dillies Paul Lezeau. #ITP #LeanProver
• Proof assistants and type theory. ~ Judah Towery. #ITP #LeanProver #Math
• A foundationally verified intermediate verification language. ~ Joshua M. Cohen. #ITP #CoqProver #Wyh3
• The way of code (The timeless art of Vibe Coding). ~ Rick Rubin. #Programming #Tao

The readings shared in Bluesky on 25 May 2025 are

• Shallow expressions (in Isabelle/HOL). ~ Simon Foster. #ITP #IsabelleHOL
• Orgro: A mobile Org Mode file editor and viewer. #OrgMode

The readings shared in Bluesky on 24 May 2025 are

• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Munta: A verified model checker for timed automata (in Isabelle/HOL). ~ Simon Wimmer. #ITP #IsabelleHOL
• Learning Physics with functional programming and Haskell. ~ Esteban Marín. #Haskell #FunctionalProgramming #Physics
• Is AI making coders obsolete? (Are there problems with having AI tools take over coding from humans?). ~ Jennifer Goforth Gregory. #AIforCode

The readings shared in Bluesky on 23 May 2025 are

• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Solving guarded domain equations in presheaves over ordinals and mechanizing it. ~ Sergei Stepanenko, Amin Timany. #ITP #RocqProver #CategoryTheory
• Ineq-Comp: Benchmarking human-intuitive compositional reasoning in automated theorem proving on inequalities. ~ Haoyu Zhao et als. #LLMs #ITP #LeanProver #Math
• CLEVER: A curated benchmark for formally verified code generation. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver #AIforCode
• Formalisation of fairness notions in assignment problem. ~ Duc Minh Do. #ITP #IsabelleHOL

The readings shared in Bluesky on 22 May 2025 are

• A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. #ITP #ACL2 #Math
• Lean-auto: An interface between Lean 4 and automated theorem provers. ~ Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad. #ITP #LeanProver
• Lean-SMT: An SMT tactic for discharging proof goals in Lean. ~ Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark Barrett. #ITP #LeanProver
• The roots of Lisp. ~ Paul Graham (2002). #Lisp #Programming
• Las raíces de Lisp. ~ Paul Graham (2002). #Lisp #Programming
• LISP, el "lenguaje de DIOS". ~ LinuxChad. #Lisp #Programming

The readings shared in Bluesky on 21 May 2025 are

• Will computers prove theorems? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formalizing the future: Lean’s impact on mathematics, programming, and AI. ~ Leo De Moura. #ITP #LeanProver #Math #CompSci #AI
• A formalization of the correctness of the Floodsub protocol. ~ Ankit Kumar, Panagiotis Manolios. #ITP #ACL2
• OpenEvolve: Open-source implementation of AlphaEvolve. ~ Asankhaya Sharma. #AI #LLMs #AlphaEvolve #Math
• AlphaEvolveVerify: Verification of Google DeepMind's AlphaEvolve 48-multiplication matrix algorithm. ~ Deming Xu. #Python #Programming #Math
• Toward safe, flexible, and efficient software in Common Lisp. ~ Robert Smith. #CommonLisp
• Theorems and conjectures with Python. ~ Alessio Drivet. #Math #Python #Programming
• Analysis of selection noise in genetic algorithms. Nataliya M. Gulayeva, Joaquín Borrego-Díaz, Fernando Sancho-Caparrini. #GeneticAlgoritm
• org-expex: Expex glosses in Org-mode (Emacs org-mode extension to auto-create linguistic glosses). ~ David Diem. #Emacs #OrgMode

The readings shared in Bluesky on 20 May 2025 are

• Formalising the Bruhat-Tits tree. ~ Judith Ludwig, Christian Merten. #ITP #LeanProver
• Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #HoTT
• A Python frozenset interpretation of Dependent Type Theory. ~ Philip Zucker. #TypeTheory #Python #Logic
• Comparing code: LeetCode problems in Rust vs. Haskell. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Symbolic sets for proving bounds on Rado numbers. ~ Tanbir Ahmed, Lamina Zaman, Curtis Bright #SAT #Python #Math
• Formatting academic papers in Emacs Orgmode. ~ Kenneth Flak. #Emacs #OrgMode

The readings shared in Bluesky on 19 May 2025 are

• A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. #ITP #LeanProver #Math
• Towards a mechanization of fraud proof games in Lean. ~ Martín Ceresa, César Sánchez. #ITP #LeanProver
• Farey sequences and Ford circles (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Formal verification of a fail-safe cross-chain bridge. ~ Filip Marić, Bernhard Scholz, Pavle Subotić. #ITP #IsabelleHOL
• Verifying smart contract transformations using bisimulations. ~ Kegan McIlwaine, James Caldwell. #ITP #IsabelleHOL
• Formally specifying contract optimizations with bisimulations in Coq. ~ Derek Sorensen. #ITP #Coq #Rocq
• Math for programming (Learn the math, write better code). ~ Ronald T. Kneusel. #Math #Python #Programming
• Lisp. But why? ~ Raj. #CommonLisp #Programming

The readings shared in Bluesky on 18 May 2025 are

• Formalizing a proof in Lean using Claude and o4. ~ Terence Tao. #ITP #LeanProver #Math
• Formalizing a proof in Lean using Github Copilot only. ~ Terence Tao. #ITP #LeanProver #Math
• Formal proof of Dilworth’s theorem (in Isabelle/HOL). ~ Vivek Soorya Maadoori et als. #ITP #IsabelleHOL #Math
• Benchmarking energy calculations using formal proofs. ~ Ejike D. Ugwuanyi, Colin T. Jones, John Velkey, Tyler R. Josephson. #ITP #LeanProver
• Freer arrows and why you need them. ~ Grant Vandomelen, Yao Li. #Haskell #FunctionalProgramming
• Computer science and mathematics: A powerful synergy. ~ Khaled M.M. Alrantisi, Mohammad Imtiyaz Gulbarga. #Math #CompSci
• Tipos abstractos y polimorfismo en programación funcional. ~ Emanuel Goette. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 17 May 2025 are

• Formalizing the future: Lean’s impact on mathematics, programming, and AI. ~ Leo De Moura. #ITP #LeanProver #Math #CompSci #AI
• Will computers prove theorems? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Recursive definitions in Lean. ~ Joachim Breitner. #ITP #LeanProver #FunctionalProgramming
• Digitalizing Wick's theorem. ~ Joseph Tooby-Smith. #ITP #LeanProver
• The Haskell Unfolder Episode 44: State-based testing with quickcheck-lockstep. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 16 May 2025 are

• AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms. ~ AlphaEvolve team. #AI #LLMs #AlphaEvolve #Math
• AlphaEvolve: A coding agent for scientific and algorithmic discovery. ~ AlphaEvolve team. #AI #LLMs #AlphaEvolve #Math
• The collapse of GPT (Will future artificial intelligence systems perform increasingly poorly due to AI-generated material in their training data?). ~ Neil Savage. #AI #GPT
• La última IA de Google promete ser capaz de mejorarse a sí misma. De momento, ya está superando a los matemáticos humanos. ~ Marcos Merino. #AI #LLMs #AlphaEvolve #Math

The readings shared in Bluesky on 15 May 2025 are

• Heftia: The final word in Haskell effect system libraries (Part 1.1). ~ Riyo. #Haskell #FunctionalProgramming
• Quasiquoting for fun, profit, expressions and patterns. ~ MLabs. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 14 May 2025 are

• Formal P-category theory and normalization by evaluation in Rocq. ~ David G. Berry, Marcelo P. Fiore. #ITP #Rocq #CategoryTheory
• Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. #ITP #Rocq #OCaml
• Theorem prover Arend. ~ Fedor Part, Valery Isaev, and Sergey Sinchuk. #ITP #Arend
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 13 May 2025 are

• Course: Functional programming and theorem proving in Lean 4. ~ Leni Aniva, Abdalrhman Mohamed. #ITP #LeanProver #FunctionalProgramming
• Formalizing a proof in Lean using Github copilot and canonical. ~ Terence Tao. #ITP #LeanProver #Math
• APOLLO: Automated LLM and Lean collaboration for advanced formal reasoning. ~ Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh. #LLMs #ITP #LeanProver
• La gran ilusión de la IA: no piensa, no siente, pero habla como si lo hiciera. ~ Ramón López de Mántaras. #IA

The readings shared in Bluesky on 10 May 2025 are

• A tool to verify estimates, II: a flexible proof assistant. ~Terence Tao. #ITP #Python #Math
• How to (actually) prove it - New frontiers of mathematics & computing in Lean. ~ Kiran. #ITP #LeanProver #Math
• LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. #ITP #LeanProver #Mathlib
• How do undergraduates do mathematics? (A guide to studying mathematics at Oxford University). #Math

The readings shared in Bluesky on 9 May 2025 are

• Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord and Julien Narboux. #ATP #ITP #IsabelleHOL #LeanProver #Coq #Rocq #Education
• Maths with Coq in L1, a pedagogical experiment. ~ Marie Kerjean, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Logic #Math #Teaching
• Teaching divisibility and binomials with Coq. ~ Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Math #Teaching
• A graphical interface for category theory proofs in Coq. ~ Luc Chabassier. #ITP #Coq #Rocq #CategoryTheory
• OnlineProver: Experience with a visualisation tool for teaching formal proofs. ~ Ján Perháč et als. #ITP #Logic #Teaching
• Minimal sequent calculus for teaching first-order logic: Lessons learned. ~ Jørgen Villadsen. #ITP #IsabelleHOL #Logic #Teaching
• ProofBuddy (How it started, how it's going). ~ Nadine Karsten, Kim Jana Eiken, Uwe Nestmann. #ITP #IsabelleHOL #Logic #Teaching
• Lean4 machine assisted proof framework for chip firing game & graphical Riemann-Roch. ~ Dhyey Dharmendrakumar Mavani. #ITP #LeanProver
• Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. #ITP #Coq #Rocq
• Analyzing API design via algebraic laws. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Beginnings of a Haskell game engine. ~ Mitchell Vitez. #Haskell #FunctionalProgramming
• Scrap your iteration combinators. ~ Tom Ellis. #Haskell #FunctionalProgramming
• From Haskell to a new structured combinator processor. ~ Yukang Xie et als. #Haskell #FunctionalProgramming
• Lógicas de orden superior y verificación formal. ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
• Lógicas de orden superior y verificación formal (Slides). ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq

The readings shared in Bluesky on 8 May 2025 are

• SAT-solving the poset cover problem. ~ Chih-Cheng Rex Yuan, Bow-Yaw Wang. #ATP #SAT_solvers #Z3
• FormalMATH: Benchmarking formal mathematical reasoning of large language models. ~ Zhouliang Yu et als. #LLMs #Autoformalization #Math #ITP #LeanProver
• Beyond theorem proving: Formulation, framework and benchmark for formal problem-solving. ~ Qi Liu et als. #LLMs #ITP #LeanProver
• The Haskell Unfolder Episode 43: Monomorphism restriction and defaulting. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• What is programming?… and what is programming in the age of artificial intelligence? ~ Sebastian Nicolajsen, Claus Brabrand. #Programming

The readings shared in Bluesky on 6 May 2025 are

• Sophie Germain’s theorem (in Isabelle/HOL). ~ Benoît Ballenghien. #ITP #IsabelleHOL #Math
• Recamán’s sequence. ~ John D. Cook. #Math #Python
• 25 useful tips for Emacs (for beginners and advanced users). Raoul Comninos. #Emacs

The readings shared in Bluesky on 5 May 2025 are

• Compiling Haskell into Lean: A common abstract syntax for Haskell and interactive theorem provers. ~ Talitha Holcombe. #Haskell #FunctionalProgramming #ITP #LeanProver
• Avaliando a habilidade do ChatGPT de realizar provas de dedução natural em lógica proposicional e lógica de predicados. ~ Francisco Leonardo Batista Martins et als. #LLLms #ChatGPT #Logic
• Typed Lisp, a primer. ~ Musa Al-hassy (2019). #CommonLisp #Haskell

The readings shared in Bluesky on 4 May 2025 are

• Formalizing resource ownership semantics of spinlocks with the Coq proof assistant. ~ Sebastian Luis S. Ortiz et als. #ITP #Coq #Rocq
• Formalizing reversible computations for synchronous dataflow languages with infinite lists. ~ Sosuke Moriguchi et als. #ITP #Coq #Rocq
• Formal verification of blockchain nonforking in DAG-based BFT consensus with dynamic stake. ~ Alessandro Coglio, Eric McCarthy. #ITP #ACL2
• The minimal megaparsec tutorial. ~ Clément Hurlin. #Haskell #FunctionalProgramming
• Mathematician solves algebra's oldest problem using intriguing new number sequences. ~ University of New South Wales. #Math
• A hyper-Catalan series solution to polynomial equations, and the Geode. ~ N.J. Wildberger, Dean Rubine. #Math
• Entrevista a Jeffrey Ullman (ACM Turing Award). ~ Camilo Chacón Sartori. #Computación

The readings shared in Bluesky on 2 May 2025 are

• A proof of concept tool to verify estimates. ~ Terence Tao. #Math #AI #LLMs #ChatGPT #Python
• Advancing mathematics by guiding human intuition with AI. ~ Alex Davies et als. (2021). #Math #AI
• Semantics of probabilistic programs using s-finite kernels in dependent type theory. ~ Reynald Affeldt, Cyril Cohen, Ayumu Saito. #ITP #Rocq
• DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL #LLMs
• Frontier of formal theorem proving with large language models: Insights from the DeepSeek-Prover. ~ Huajian Xin. #ITP #LeanProver #LLMs #DeepSeek
• Automated theorem provers as the hub of the AI math ecosystem. ~ Stephan Schulz. #Math #AI #ITP

The readings shared in Bluesky on 1 May 2025 are

• DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. ~ Z.Z. Ren et als. #LLMs #ITP #LeanProver
• Mathematical beauty, truth and proof in the age of AI. ~ Jordana Cepelewicz. #Math #AI #ITP
• Logical modelling in CS education: Bridging the natural language gap. ~ Tristan Kneisel, Fabian Vehlken, Thomas Zeume. #Logic #Education
• Iltis: An interactive, web-based system for teaching formal foundations of computer science. #Logic #Education
• Introduction to Iltis: An interactive, web-based system for teaching logic. ~ Gaetano Geck et als. (2018). #Logic #Teaching
• Iltis: Learning Logic in the Web. ~ Gaetano Geck et als. (2022). #Logic #Teaching
• Clear: A formal verification framework for smart contracts in Lean. ~ Julian Sutherland. #ITP #LeanProver

The readings shared in Bluesky on 30 April 2025 are

• Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. #ITP #Coq #Rocq
• Verified hand-written Lean solutions to HumanEval. ~ Markus Himmel. #ITP #LeanProver

The readings shared in Bluesky on 29 April 2025 are

• Improving mathematical proving skills through interactive theorem proving. ~ Sana Stojanović Đurđević, Andrija Urošević, Filip Marić (2024). #ITP #IsabelleHOL #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math

The readings shared in Bluesky on 28 April 2025 are

• Tutte's theorem as an educational formalization project. ~ Pim Otte. #ITP #LeanProver #Math
• Haskelling my Python (Reimplementing Haskell lazy infinite lists using Python generators). ~ Unnamed Website. #Python #Haskell #FunctionalProgramming #Math
• Power series, power serious. ~ M. Douglas McIlroy (1998). #Haskell #FunctionalProgramming #Math
• Tree rewriting calculi for strictly positive logics. ~ Sofía Santiago-Fernández, David Fernández-Duque, Joost J. Joosten. #Logic

The readings shared in Bluesky on 27 April 2025 are

• Bitcoinolog: Reason about Bitcoin addresses with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Working with Common Lisp pathnames. ~ Nicolas Martyanoff. #CommonLisp
• AI for program verification. ~ Cristian Cadar, Abhik Roychoudhury. #AI #FormalVerification
• Introducing category theory (Version 26 Apr 2025). ~ Peter Smith. #CategoryTheory
• The levels of Emacs proficiency. ~ Vivek Haldar (2011). #Emacs

The readings shared in Bluesky on 25 April 2025 are

• Lean 4 formalization of the logic textbook "Logic Notes" by Lou van den Dries. ~ Will Bradley. #ITP #LeanProver #Logic #Math
• Neural theorem proving: Generating and structuring proofs for formal verification. ~ Balaji Rao, William Eiers, Carlo Lipizzi. #LLMs #ITP #IsabelleHOL
• Mathematical Logic (Math 570) Lecture Notes. ~ Lou van den Drie. #Logic #Math
• Implementing Unsure Calculator in 100 lines of Haskell. ~ Rodrigo Mesquita. #Haskell #FunctionalProgramming
• Integrating effectful and persistent. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Porting song recommendations to Haskell. ~ Mark Seemann. #Haskell #FunctionalProgramming
• Magical Haskell: A friendly approach to modern functional programming, type theory, and artificial intelligence. ~ Anton Antich. #Haskell #FunctionalProgramming #AI
• #Exercitium: Duplicación de cada elemento. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 24 April 2025 are

• On the averaging problem of ideal families related to Frankl's conjecture with formal proof by Lean 4. ~ Masahiro Hachimori, Kenji Kashiwabara. #ITP #LeanProver #Math
• #Exercitium: Sistema factorádico de numeración. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 23 April 2025 are

• Bullshit universities: the future of automated education. ~ Robert Sparrow, Gene Flenady. #GenerativeAI #Education
• #Exercitium: Suma de cadenas. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∪ f⁻¹[v]​] ⊆ f[s] ∪ v". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 22 April 2025 are

• The inverse method is a good fit for Datalog theorem proving. ~ Philip Zucker. #Datalog #Logic
• In between myth and reality: AI for math (a case study in category theory). ~ Răzvan Diaconescu. #LLMs #Math
• #Exercitium: Cuadrado más cercano. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ∩ t = f(s ∩ f⁻¹(t)". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 21 April 2025 are

• A formalisation of Aristotle’s assertoric syllogistic in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Karol Wapniarski. #ITP #IsabelleHOL #Logic
• Non-circular trigonometric proofs of the pythagorean theorem in Lean4: A comparison. ~ Paul Pajo. #ITP #LeanProver #Math
• Enhancing AI trustworthiness through automated reasoning: A novel method for explaining deep learning and LLM reasoning. ~ Julia Connolly, Oliver Stanton, Sarah Veronica, Liam Whitmore. #LLMs #Reasoning #ITP
• SLip: Lisp system in your browser. ~ Mihai Bazon. #CommonLisp
• #Exercitium: Divisores de un número con final dado. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] \ f[t] ⊆ f[s \ t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 20 April 2025 are

• Readings shared April 19, 2025. #Algorithms #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #MachineLearning #Math #Python #SMT #Z3
• Gridbach: Un proyecto para comprobar de forma distribuida la famosa conjetura de Goldbach. ~ @Alvy #Matemáticas
• Gridbach: The grid-computing system that calculates verification of the mathematical problem "Goldbach conjecture". #Math
• #Exercitium: Órbita prima. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 19 April 2025 are

• Knuckledragger: A low barrier proof assistant. ~ Philip Zucker. #ITP #SMT #Z3 #Python
• Neural theorem proving tutorial. ~ Sean Welleck. #MachineLearning #ITP #LeanProver
• Listing prime numbers periodically. ~ Han-Lin Li, Shu-Cherng Fang, Way Kuo, Nianrui Lin. #Math #Algorithms
• #Exercitium: Ordenada cíclicamente. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∩ t] ⊆ f[s] ∩ f[t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 18 April 2025 are

• #Exercitium: Eliminación de las ocurrencias aisladas. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 17 April 2025 are

• Formalization of Fraïssé limits in Lean. ~ Gabin Kolly. #ITP #LeanProver #Math
• A readable and computable formalization of the Streamlet consensus protocol. ~ Mauro Jaskelioff, Orestis Melkonian, James Chapman. #ITP #Agda
• The Haskell Unfolder Episode 42: Logic programming with typedKanren. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Emparejamiento de árboles. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 15 April 2025 are

• Simplified and verified: A second look at a proof-producing union-find algorithm. ~ Lukas Stevens, Rebecca Ghidini. #ITP #IsabelleHOL
• First-order rewriting (in Isabelle/HOL). ~ René Thiemann et als. #ITP #IsabelleHOL
• Proof terms for term rewriting (in Isabelle/HOL). ~ Christina Kirk. #ITP #IsabelleHOL
• The Kolmogorov-Chentsov theorem (in Isabelle/HOL). ~ Christian Pardillo-Laursen, Simon Foster. #ITP #IsabelleHOL #Math
• Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. ~ Numina & Kimi Team. #LLMs #LeanProver
• Mathematical reasoning & proofs. ~ Alistair Savage. #Math
• Decomposing factorial of 300K as the product of 300K factors larger than 100K. ~ Gustavo. #Programming #RacketLang #FunctionalProgramming #Math
• Emacs Lisp elements (A big picture view of the Emacs Lisp programming language). ~ Protesilaos Stavrou. #Emacs #Lisp
• The Barium experiment. ~ Tom Szilagyi. #CommonLisp
• #Exercitium: Separación por posición. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Monotonía de la imagen de conjuntos". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 13 April 2025 are

• Completeness of decreasing diagrams for the least uncountable cardinality (in Isabelle/HOL). ~ Ievgen Ivanov. #ITP #IsabelleHOL #Math #SetTheory
• Efficient formal verification of quantum error correcting programs. ~ Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying. #ITP #Coq
• Mathematical reading list (University of Cambridge). #Math
• LLMs can't stop making up software dependencies and sabotaging everything. ~ Thomas Claburn. #AI #LLMs #Programming
• #Exercitium: Descomposiciones triangulares. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]". #LeanProver #IsabelleHOL #Math
• Curso "Razonamiento automático (2011-12)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 12 April 2025 are

• Evaluating AI's impact on Haskell open source development. ~ Matthew Pickering, Sam Derbyshire. #LLMs #Haskell #FunctionalProgramming
• #Exercitium: Índices de valores verdaderos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 11 April 2025 are

• Code generation via meta-programming in dependently typed proof assistants. ~ Mathis Bouverot-Dupuis, Yannick Forster. #ITP #Agda #Rocq #LeanProver
• A comparative review of ZFC, NBG, and MK axiom systems: Theoretical foundations and formalization in Coq. ~ Si Chen, Wensheng Yu. #ITP #Coq #Rocq #Math #SetTheory
• A (very niche) footgun in GHC.Generics. ~ welltypedwitch. #Haskell #FunctionalProgramming
• Refactoring strings in GHC. ~ Brandon Chinn. #Hakell #FunctionalProgramming
• #Exercitium: Código de las alergias. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[f⁻¹[u]​] ⊆ u". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 10 April 2025 are

• Canonical for automated theorem proving in Lean. ~ Chase Norman, Jeremy Avigad. #ITP #LeanProver #Math
• Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity (in Isabelle/HOL). ~ Filip Marić, Jelena Markovic. #ITP #IsabelleHOL
• Leanabell-prover: Posttraining scaling in formal reasoning. ~ Jingyuan Zhang et als. #LLMs #ITP #LeanProver
• Lemmanaid: Neuro-symbolic lemma conjecturing. ~ Yousef Alhessi et als. #LLMs #ITP #IsabelleHOL
• Reasoning about AI’s reasoning. ~ Höjer Key. #AI #LLMs #ITP #ATP
• Search index in 150 lines of Haskell. ~ kqr. #Haskell #FunctionalProgramming
• Distilling PEP 8 for teaching introductory programming. ~ Diana Kirk, Andrew Luxton-Reilly, Ewan Tempero. #Programming
• Why I program in Lisp. ~ Joe Marshall. #CommonLisp #FunctionalProgramming
• From blind solvers to logical thinkers: Benchmarking LLMs' logical integrity on faulty mathematical problems. ~ A M Muntasir Rahman et als. #LLMs #Math #Reasoning
• #Exercitium: Pim, Pam, Pum y divisibilidad. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 8 April 2025 are

• DMTL4: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. #ITP #LeanProver #Math
• Course Cs2120f24: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. #ITP #LeanProver #Math
• Training making math proofs using Lean 4. ~ Krillof. #ITP #LeanProver #Math
• PEIRCE: Unifying material and formal reasoning via LLM-driven neuro-symbolic refinement. ~ Xin Quan, Marco Valentino, Danilo S. Carvalho, Dhairya Dalal, André Freitas. #AI #LLMs #ITP #IsabelleHOL #Prolog #LogicProgramming
• #Exercitium: Reiteración de una función. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f⁻¹(f(s)) ⊆ s"". #LeanProver #IsabelleHOL #Math

• Verified program extraction in number theory: The fundamental theorem of arithmetic and relatives. ~ Franziskus Wiesnet. #ITP #Minlog #Haskell #FunctionalProgramming #Math
• Central limit theorem in Lean. ~ Rémy Degenne. #ITP #LeanProver #Math
• Prime number theorem and more in Lean. ~ Alex Kontorovich. #ITP #LeanProver #Math
• Formalizing value distribution theory in Lean. ~ Stefan Kebekus. #ITP #LeanProver #Math
• Learn Lean 4 with PLFA (Programming Language Foundations in Agda) proofs. ~ rami3l. #ITP #LeanProver
• Chandra-Furst-Lipton (A digitisation of the number on the forehead model in Lean). ~ Yaël Dillies. #ITP #LeanProver #Math
• Toric varieties in Lean (Formalisation of toric varieties in Lean 4). ~ Yaël Dillies, Paul Lezeau, Patrick Luo, Michał Mrugała, Justus Springer, Andrew Yang. #ITP #LeanProver #Math
• Arithmetic progressions - almost periodicity (A digitisation of the Kelley-Meka bound on Roth numbers in Lean). ~ Thomas Bloom, Yaël Dillies. #ITP #LeanProver #Math
• Lecture notes for an introductory course in group theory. ~ Ben Selfridge. #ITP #LeanProver #Math
• Stronger SMT solvers for proof assistants (Proofs, quantifier simplification, strategy schedules). ~ Hans-Jörg Schurr. #ATP #SMT #ITP #IsabelleHOL
• An introduction to typeclass metaprogramming. ~ Alexis King. #Haskell #FunctionalProgramming
• meta_predicate declarations. ~ Markus Triska. #Prolog #LogicProgramming
• #Exercitium: Elementos de una matriz con algún vecino menor. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ⊆ u ↔ s ⊆ f⁻¹(u)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica matemática y fundamentos (2011-12)". #Lógica #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 6 April 2025 are

• Prolog vs LLMs: A complementary approach to AI (according to DeepSeek). #Prolog #LogicProgramming #LLMs #AI
• #Exercitium: Enumeración de árboles binarios. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ⊆ f⁻¹(f(s))". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2011-12)". #Lógica #ProgramaciónLógica #Prolog
• Temas de "Lógica informática" (curso 2011-12). #Lógica #ProgramaciónLógica #Prolog
• Ejercicios de "Lógica informática" (curso 2010-11). #Lógica

The readings shared in Bluesky on 5 April 2025 are

• Building AI for mathematical reasoning. ~ Chris Garcia. #Prolog #LogicProgramming #Logic #Math
• #Exercitium: Números triangulares con n cifras distintas. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "f(s ∪ t) = f(s) ∪ f(t)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 4 April 2025 are

• Learning Lean in the age of Artificial Intelligence. ~ Adolfo Neto. #ITP #LeanProver
• Guessing game: Haskell style. ~ kqr. #Haskell #FunctionalProgramming
• Function application needs to grow a spine already. ~ Thunderseethe. #Haskell #FunctionalProgramming
• Why you should maintain a personal LLM coding benchmark. ~ Edward Z. Yang. #LLMs #Programming
• #Exercitium: Trenzado de listas. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Informática (2011-12)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2011-12). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2011–12). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2011–12). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 3 April 2025 are

• Morley's theorem (in Isabelle/HOL). ~ Benjamin Puyobro. #ITP #IsabelleHOL #Math
• Category theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. #CategoryTheory #Math #Haskell #FunctionalProgramming
• LeanSolver: Solving theorems through large language models and search. ~ Avi Luciano Halevy #LLMs #ITP #LeanProver
• AlphaProof: when reinforcement learning meets formal mathematics. ~ Thomas Hubert. #AlphaProof #AI #Math
• #Exercitium: Biparticiones de una lista. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 2 April 2025 are

• Basic probability in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Mathlib #Math
• GOL in GOL in HOL: Verified circuits in Conway's game of life. ~ Magnus O. Myreen, Mario Carneiro. #ITP #HOL4
• Unfolding trees breadth-first in Haskell. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• Faking ADTs and GADTs in languages that shouldn't have them. ~ Justin Lê. #Haskell #FunctionalProgramming
• Proof or bluff? Evaluating LLMs on 2025 USA math olympiad. ~ Ivo Petrov et als. #LLMs #Math
• TAUT2 (Here you will find various types of randomly-generated, self-correcting logic excercises). #Logic
• Logica (Tools for thought). #Logic
• Curso de programación lógica. ~ Ana Pradera. #Lógica #ProgramaciónLógica #Prolog
• Enseñanza del sistema de deducción natural en lógica proposicional aplicando programación lógica. ~ Joaquín Arias, Iván Ramírez. #Lógica #ProgramaciónLógica #Prolog
• Apuntes de lógica: desde Aristóteles hasta Prolog. ~ Joaquín Arias. #Lógica #ProgramaciónLógica #Prolog
• #Exercitium: Mayor producto de las ramas de un árbol. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i))". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso: Demostración asistida por ordenador (2010-11). #ITP #IsabelleHOL #Lógica

The readings shared in Bluesky on 1 April 2025 are

• A small Prolog on the Z3 AST. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
• STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. #AI #LLMs #ITP #LeanProver
• The disconnect between AI benchmarks and math research (Evaluating AI systems on their ability to be a mathematical copilot). ~ Ralph Furman. #AI #LLMs #Math
• The cultural divide between mathematics and AI (A reflection on cultural differences observed at the 2025 Joint Mathematics Meeting). ~ Ralph Furman. #AI #LLMs #Math
• #Exercitium: Número de pares de elementos adyacentes iguales en una matriz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Razonamiento automático (2010-11)". #ITP #IsabelleHOL #Logic #Math
• Deducción natural en lógica proposicional con Isabelle/HOL. #Lógica #IsabelleHOL
• Deducción natural en lógica de primer orden con Isabelle/HOL. #Lógica #IsabelleHOL
• Introducción a la demostración asistida por ordenador con Isabelle/HOL (versión de 7 de agosto de 2010). #ITP #IsabelleHOL

The readings shared in Bluesky on 31 March 2025 are

• Formally verifying a transformation from MLTL formulas to regular expressions. ~ Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. #ITP #IsabelleHOL
• #Exercitium: Elemento más repetido de manera consecutiva. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "Los primos mayores que 2 son impares". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2010-11)". #Logic #Math #CompSci
• Temas de "Lógica informática" (2010-11). #Logic #Math #CompSci
• Ejercicios de "Lógica informática" (2010-11). #Logic #Math #CompSci
• Ejercicios de deducción natural proposicional. #Logic #Math
• Ejercicios de deducción natural en lógica de primer orden. #Logic #Math

The readings shared in Bluesky on 30 March 2025 are

• Towards mechanized verification of Verilog equivalence checking. ~ Michalis Pardalos, Laura Pozzi, John Wickerson. #ITP #Coq
• Introducing clean, a formal verification DSL for zk circuits in Lean4. ~ Giorgio Dell'Immagine. #ITP #LeanProver
• #Exercitium: Regiones determinadas por n rectas del plano. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "La unión del conjunto de los números naturales pares e impares es el conjunto de los naturales". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Informática (2010-11)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2010-11). #Haskell #ProgramaciónFuncional
• Ejercicios de "Informática de 1º de Matemáticas" (2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Exámenes de "Programación funcional con Haskell" Vol. 2 (Curso 2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Introducción al cálculo simbólico con Maxima. #CálculoSimbólico #Maxima #Matemáticas

The readings shared in Bluesky on 29 March 2025 are

• Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. #ITP #LeanProver
• #Exercitium: Ampliación de matrices por columnas. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 28 March 2025 are

• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• Verified collaboration: How Lean is transforming mathematics, programming, and AI. ~ Leonardo de Moura. #ITP #LeanProver #Math #Programming #AI
• The philosophical problem of induction, and the problem of Fetzer. ~ Lawrence Paulson. #Philosophy #Math #CompSci
• #Exercitium: Emparejamiento binario. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ t = s ∪ t". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2009-10)". #Lógica #Matemática #Computación
• Temas de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Ejercicios de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Soluciones de exámenes de Lógica informática (2000-07). #Logic #Math #CompSci
• Curso "Programación declarativa (2009-10)". #Haskell #FunctionalProgramming #Prolog #LogicProgramming
• Temas de "Programación funcional con Haskell" (2009-10). #Haskell #FunctionalProgramming
• Introducción a la programación lógica con Prolog. #Prolog #LogicProgramming
• Ejercicios de programación funcional con Haskell (versión del 20 de septiembre de 2007). #Haskell #FunctionalProgramming
• Ejercicios de programación lógica con Prolog (Versión de 20 de septiembre de 2007). #Prolog #LogicProgramming

The readings shared in Bluesky on 27 March 2025 are

• Formalization of optimality conditions for smooth constrained optimization problems. ~ Chenyi Li et als. #ITP #LeanProver
• Formalization of algorithms for optimization with block structures. ~ Chenyi Li, Zichen Wang et als. #ITP #LeanProver
• Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. #ITP #Coq #Rocq #Logic
• Automated reasoning in blockchain: Foundations, applications, and frontiers. ~ Hojer Key. #ITP #Blockchain
• Functional programming in Haskell. ~ Graham Hutton. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 41: Generic monoids. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Decomposing a factorial into large factors. ~ Terence Tao. #Math
• Mathematics of the “I Ching”. ~ Peter Rowlett. #Math #TeXLaTeX
• Apuntes de programación lógica (Hasta Prolog y más allá). ~ Joaquín Arias. #LogicProgramming #Prolog #CLP
• #Exercitium: Ordenación de estructuras. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (s ∩ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 26 March 2025 are

• Formal proof of Dilworth's theorem (in Isabelle/HOL). ~ Vivek Soorya Maadoori et als. #ITP #IsabelleHOL #Math
• Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong, Tianming Liu. #AI #Math
• LogicLearner: A tool for the guided practice of propositional logic proofs. ~ Amogh Inamdar et als. #Logic
• #Exercitium: Numeración de las ternas de números naturales. #Haskell #ProgramaciónFuncional #Matemáticas
• Curso "Informática (2009-10)". #Haskell #ProgramaciónFuncional #Maxima

The readings shared in Bluesky on 25 March 2025 are

• Teaching "Foundations of Mathematics" with the Lean theorem prover. ~ Mattia Luciano Bottoni, Alberto Cattaneo, Elif Sacikara. #ITP #LeanProver #Math
• Ten Commandments of the Church of Emacs. #Emacs
• #Exercitium: Alfabeto comenzando en un carácter. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ (s ∪ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 24 March 2025 are

• Formal verification of machine learning models in Lean. ~ Matéo H. Petel. #ITP #LeanProver #MachineLearning
• Why Lisp syntax works. ~ Fernando Borretti. #Lisp #Programming
• MathGPT: Your personal math solver (Get instant homework help from your on-demand AI math solver). #AI #LLMs #Math
• MathGPT: una herramienta para resolver problemas matemáticos y ayudar con los deberes. ~ @Alvy. #IA #LLMs #Matemáticas
• Exercitium (Un reto diario de programación). #Exercitium #Haskell #ProgramaciónFuncional
• #Exercitium: Ramas de un árbol. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ t = t ∩ s". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Programación lógica (2008-09)". #ProgramaciónLógica #Prolog #IA
• Curso "Razonamiento automático (2008-09)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 23 March 2025 are

• A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
• Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu (2019). #ITP #Coq #SetTheory
• A formal proof in Coq of Cantor-Bernstein-Schroeder’s theorem without axiom of choice (2019). #ITP #Coq #SetTheory
• A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu (2020). #ITP #Coq #SetTheory
• A formalization of properties of continuous functions on closed intervals. Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalization of the equivalence among completeness theorems of real number in Coq. ~ Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalizing calculus without limit theory in Coq. ~ Yaoshun Fu, Wensheng Yu (2021). #ITP #Coq #Math
• A formalization of topological spaces in Coq. ~ Sheng Yan, Yaoshun Fu, Dakai Guo, and Wensheng Yu (2022). #ITP #Coq #Math #SetTheory
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). #ITP #Coq #Math #SetTheory
• Implementation of Bourbaki's elements of mathematics in Coq: Part one, theory of sets. ~ José Grimm (2009). #ITP #Coq #SetTheory
• Implementation of Bourbaki’s elements of mathematics in Coq: Part two, ordered sets, cardinals, integers. ~ José Grimm (2018). #ITP #Coq #Math
• Concurrent games in Agda. ~ Amy Yin. #ITP #Agda
• #Exercitium: Valores de polinomios representados con vectores. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s \ (t ∪ u) ⊆ (s \ t) \ u". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 22 March 2025 are

• Non-obvious Haskell idiom: Guard-sequence. ~ kqr. #Haskell #FunctionalProgramming
• Learn Haskell by example. ~ Phillip Hagenlocher. #Haskell #FunctionalProgramming
• #Exercitium: Segmentos maximales con elementos consecutivos. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 21 March 2025 are

• Case study: Verified Vampire proofs in the LambdaPi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suad. #ATP #Vampire #Dedukti
• A hundred pull requests for Liquid Haskell. ~ Facundo Domínguez. #Liquid #Haskell #FunctionalProgramming #SMT
• Artificial intelligence learns to reason. ~ Melanie Mitchell. #AI #LLMs #Reasoning
• #Exercitium: Lista cuadrada. #Haskell #ProgramaciónFuncional
• Demostraciones de "(a ∖ b) ∖ c ⊆ a ∖ (b ∪ c)" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2008-09)". #Lógica #Matemática #Computación
• Curso "Programación declarativa (2008-09)". #ProgramaciónFuncional #Haskell #ProgramaciónLógica #Prolog

The readings shared in Bluesky on 19 March 2025 are

• A trickier lower bound proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Can LLMs enable verification in mainstream programming? ~ Aleksandr Shefer et als. #LLMs #Programming #FormalVerification
• Towards AI-assisted academic writing. ~ Daniel J. Liebling et als. #AI #LLMs
• VisuAlgo: Visualising data structures and algorithms through animation. #Programming #CompSci
• VisuAlgo muestra visualmente cómo funcionan los algoritmos, las estructuras de datos y cómo resolver problemas. ~ @Alvy. #Programación #Computación
• #Exercitium: Matrices de Toepliz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones de "Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 19 March 2025 are

• #Exercitium: Máximos locales. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones de "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 18 March 2025 are

• Lessons learned with the Z3 SAT/SMT solver. ~ John D. Cook. #SMT #Z3
• Teaching logic programming: a review. ~ Serhiy O. Semerikov, Iryna S. Mintii, Natalia V. Moiseienko. #LogicProgramming #Prolog #ASP #CLP #Datalog
• Series vs. streams. ~ Joe Marshall. #CommonLisp
• #Exercitium: Suma si todos los valores son justos. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostrar con Isabelle/HOL que las relaciones reflexivas y circulares son simétricas. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2007-08)". #ProgramaciónFuncional #Haskell #ProgramaciónLógica #Prolog
• Curso "Programación lógica (2007-08)". #ProgramaciónLógica #Prolog #IA
• Curso "Razonamiento automático (2007-08)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 17 March 2025 are

• The calculated typer. ~ Zac Garby, Patrick Bahr, Graham Hutton. #Haskell #FunctionalProgramming
• #Exercitium: Primos equidistantes. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema del barbero. #IsabelleHOL #Lógica

The readings shared in Bluesky on 16 March 2025 are

• Permutations with no consecutive elements. ~ John D. Cook. #Math #Python #Programming
• #Exercitium: Anagramas. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 15 March 2025 are

• Revisiting an early critique of formal verification. ~ Lawrence Paulson. #ITP #Math #FormalVerification
• A proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. #ITP #ACL2 #Math
• Principles of rule-based programming. ~ Thom Frühwirth. #CHR #Constraint #LogicProgramming
• Mathematics for inference and machine learning. ~ Marc Deisenroth, Stefanos Zafeiriou. #Math #MachineLearning
• Introducción a la Introducción de Emacs. ~ Notxor. #Emacs
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema de los infectados. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2006-07)". #LogicProgramming #Prolog #AI #NLP #Constraints #Logic
• Curso "Lógica informática (2007-08)". #Lógica #Matemática #Computación

The readings shared in Bluesky on 14 March 2025 are

• La théorie des types, de Russell aux assistans à la demostration. ~ Thierry Coquand. #TypeTheory #ITP #Logic #Math
• Local look-ahead guidance via verifier-in-the-loop for automated theorem proving. ~ Sara Rajaee, Kumar Pratik, Gabriele Cesa, Arash Behboodi. #LLMs #LeanProver
• Algebra, topology, differential calculus, and optimization theory for computer science and machine learning. ~ Jean Gallier, Jocelyn Quaintance. #Math #CompSci #MachineLearning
• Las matemáticas son, sobre todo, hermosas. ~ Marta Macho-Stadler. #Matemáticas
• #Exercitium: Mastermind. #Haskell #FunctionalProgramming
• #Calculemus: La dama o el tigre. #IsabelleHOL #Lógica
• Curso "Razonamiento automático (2005-06)". #ATP #Otter #Mace #ITP #PVS
• Curso "Lógica informática (2006-07)". #Logic #Math #CompSci

The readings shared in Bluesky on 13 March 2025 are

• Course notes for "Formalising Mathematics 2025". ~ Bhavik Mehta et als. #ITP #LeanProver #Math
• LeanAgent: Lifelong learning for formal theorem proving. ~ Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar. #LLMs #ITP #LeanProver #Math
• The Haskell Unfolder Episode 40: Understanding through a model. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Determinación de los elementos minimales. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema lógico del mal. #ITP #IsabelleHOL #Lógica
• Curso "Lógica informática (2005-06)". #Logic #Math #CompSci
• Curso "Programación declarativa (2005-06)". #LogicProgramming #Prolog

The readings shared in Bluesky on 12 March 2025 are

• A formal proof of the irrationality of ζ(3) in Lean 4. ~ Junqi Liu, Jujian Zhang, Lihong Zhi. #ITP #LeanProver #Math
• #Exercitium: La bandera tricolor. #Haskell
• #Calculemus: Teorema de Nicómaco. #IsabelleHOL #Lógica #Matemática
• Curso "Demostración automática de teoremas (2004-05)". #ATP #Otter #Mace #Logic #Math
• Curso "Programación lógica (2004-05)". #LogicProgramming #Prolog #AI #NLP #Constraints #MachineLearning
• Curso "Razonamiento automático (2004-05)". #ATP #Otter #Mace #Jape #Logic #ITP #PVS

The readings shared in Bluesky on 11 March 2025 are

• Extrinsic termination proofs for well-founded recursion in Lean. ~ Joachim Breitner. #ITP #LeanProver
• Knuth Bendix solver on Z3 AST. ~ Philip Zucker. #SMT #Z3
• Books on the history of mathematics, some thoughts. ~ Thony Christie. #Math
• LLMs can find mathematical reasoning mistakes by pedagogical chain-of-thought. ~ Zhuoxuan Jiang et als. #LLMs #Math
• Can proof assistants verify multi-agent systems? ~ Julian Alfredo Mendez, Timotheus Kampik. #MAS #FormalVerification #LeanProver #Scala
• DeepSeek vs. ChatGPT vs. Claude: A comparative study for scientific computing and scientific machine learning tasks. ~ Qile Jiang, Zhiwei Gao, George Em Karniadakis. #LLMs #Math
• Why do researchers care about small language models? ~ Stephen Ornes. #LLMs #SMLs
• Navigating between points with registers. ~ Daniel Liden. #Emacs
• #Exercitium: Ordenación por el máximo. #Haskell
• #Calculemus: Reto f(f(f(b))) = f(b). #IsabelleHOL #Lógica #Matemática
• Curso "Demostración automática de teoremas (2002-03)". #ATP #Otter #Mace #Logic #Math
• Curso "Programación lógica (2003-04)". #LogicProgramming #Prolog #AI
• Curso "Razonamiento automático (2003-04)". #ATP #Otter #Mace #ITP #Jape #PVS
• Curso "Lógica informática (2004-05)". #Logic #Math
• Curso "Programación declarativa (2004-05)". #LogicProgramming #Prolog

The readings shared in Bluesky on 10 March 2025 are

• The burden of proof: Automated tooling for rapid iteration on large mechanised proofs. ~ Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, John Wickerson. #ITP #IsabelleHOL
• MiniF2F in Rocq: Automatic translation between proof assistants (a case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesúss Gallego Arias, Marc Lelarge. #LLMs #Rocq #LeanProver #IsabelleHOL #Math
• Generating millions of Lean theorems with proofs by exploring state transition graphs. ~ David Yin, Jing Gao. #LLMs #LeanProver #Math
• New proofs expand the limits of what cannot be known (By proving a broader version of Hilbert’s famous 10th problem, two groups of mathematicians have expanded the realm of mathematical unknowability). ~ Joseph Howlett. #Math
• Les sept problèmes mathématiques du prix du millénaire. ~ Nicolas Bacaër et als. #Math
• How to get a Common Lisp job in 2055. ~ Sebastian Carlos. #CommonLisp
• #Exercitium: Iguales al siguiente. #Haskell
• #Calculemus: Celebración del día mundial de la lógica. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2003-04)" #LogicProgramming #Prolog

The readings shared in Bluesky on 9 March 2025 are

• Floating point numbers in Lean. ~ Joseph McKinsey. #ITP #LeanProver #Math
• Flean: Floating point numbers in Lean, mostly done! ~ Joseph McKinsey. #ITP #LeanProver #Math
• Curso "Lógica informática" (2003-04). #Logic #Math #CompSci

The readings shared in Bluesky on 8 March 2025 are

• Sum types and subtypes and unions. ~ Justin Le. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 7 March 2025 are

• A formalisation of addition chains. ~ Laurent Théry. #ITP #Coq #Rocq
• QED in context (An observation study of proof assistant users). ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C. Pierce, Andrew Head #ITP #LeanProver #Coq #Rocq
• On the formalization of the simplicial model of HoTT. ~ Kunhong Du. #ITP #Agda #HoTT
• A gentle introduction to categorical logic and type theory. ~ Eric Schmid. #Math #CategoryTheory #TypeTheory
• MathMistake checker: A comprehensive demonstration for step-by-step math problem mistake finding by prompt-guided LLMs. ~ Tianyang Zhang et als. #LLMs #Math
• A survey on Large Language Models for code generation. ~ Nam Huynh, Beiyu Lin. #LLMs #Programming
• Markov chain of thought for efficient mathematical reasoning. ~ Wen Yang, Minpeng Liao, Kai Fan. #LLMs #Math #Reasoning
• Assisting mathematical formalization with a learning-based premise retriever. ~ Yicheng Tao et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 6 March 2025 are

• Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. #ITP #Coq #Rocq
• Lean-STaR: Learning to interleave thinking and proving. ~ Haohan Lin et als. #LLMs #ITP #LeanProver
• MA-LoT: Multi-agent lean-based long chain-of-thought reasoning enhances formal theorem proving. ~ Ruida Wang et als. #LLMs #ITP #LeanProver
• FANS: Formal answer selection for natural language math reasoning using Lean4. ~ Jiarui Yao, Ruida Wang, Tong Zhang. #LLMs #ITP #LeanProver
• From informal to formal (Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs). ~ Jialun Cao et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 5 March 2025 are

• Language partitioning for mission-time linear temporal logic (in Isabelle/HOL). ~ Zili Wang, Katherine Kosaian, Alec Rosentrater. #ITP #IsabelleHOL
• Unos profesores avisan de que la IA supone una amenaza para el pensamiento crítico de los estudiantes: "escribir también es pensar". ~ Marcos Merino. #AI #Education