Estas son las 38 lecturas que compartí en Mastodon durante la semana pasada.

El hilo principal de esta semana es el impacto de la IA en las matemáticas. Terence Tao («Math 2.0»), Jeremy Avigad, Christian Szegedy y Quanta Magazine se preguntan hacia dónde va la disciplina, y Thomas Hales analiza la fiabilidad de Lean y de las demostraciones generadas por IA. Un tema relacionado en la sección de Lean 4 es la autoformalización: Scott Armstrong sostiene que ahora es muy fácil y publica una colección de skills para Codex y Claude Code, y hay una formalización asistida por IA de la conjetura de Poincaré. También merece la pena echar un vistazo a la edición en línea de Software Foundations en Lean.

El resto abarca Isabelle/HOL (geometría en el AFP, metaprogramación en Isabelle/ML y enseñanza de la lógica), un resultado de certificación en Rocq para poliedros y un libro de texto clásico de Haskell. La última sección recoge contenido en español: una guía docente sobre Lean 4, los retos de Lean 4 y reseñas de algunas de las entradas de AI4Math anteriores.

Lean 4

• A Lean 4 framework for the radii polynomial method. ~ Fengyang Wang. #LeanProver #ITP #Math
• Advancing mathematics research with AI-driven formal proof search. ~ George Tsoukalas et al. #LeanProver #ITP #AI4Math
• AIProver: agentic auto-formalization of mathematical research via certificate-driven evolving harness. ~ Prithwish Jana et al. #LeanProver #ITP #AI4Math
• An AI-assisted formalization of the Poincaré conjecture. ~ Zhiyuan Zhang, Axel Delaval, Leheng Chen, Jinxuan Chen, Jie Xu, Yuxuan Liao, Jiedong Jiang, Chunlei Liu, Bin Dong. #LeanProver #ITP #AI4Math
• Autoformalization is now very easy. ~ Scott Armstrong. #LeanProver #ITP #AI4Math #Autoformalization
• Erdős 374: classical square products of factorials (in Lean 4). ~ Alexander. #LeanProver #ITP #Math
• LeanAutoformalizationSkills: A collection of skills for using Codex or Claude Code to formalize mathematics in Lean 4. ~ Scott Armstrong. #LeanProver #ITP #AI4Math #Autoformalization
• Software Foundations in Lean. ~ Benjamin Pierce et al. #LeanProver #ITP
• Sound and complete solving for multi-width parametric bitvectors via principled reductions. ~ Siddharth Bhat et al. #LeanProver
• Toward a Lean formalization of analog computing with microwaves. ~ Matteo Nerini, Xuekang Liu, Bruno Clerckx. #LeanProver #ITP
• We live in the dependently typed future now. ~ Stephen Diehl. #LeanProver #ITP #AI4Math
• What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI. ~ Thomas Hales. #LeanProver #ITP #AI4Math
• ZFLean: a Lean 4 library for doing core mathematics inside Mathlib's model of ZFC set theory. ~ Vincent Trélat, Matteo Pouillat. #LeanProver #ITP #Math
• ZFLean: a framework for set-level mathematics in Lean. ~ Vincent Trélat, Matteo Pouillat. #LeanProver #ITP #Math

Isabelle/HOL

• A first introduction to Isabelle/ML metaprogramming: automatic estimation of polynomial degrees. ~ Jonas Bayer, Anna Danilkin, Marco David, Annie Yao. #IsabelleHOL #ITP
• Mathematical proof assistants for teaching logic: the LogiKEy methodology. ~ Christoph Benzmüller, David Fuenmayor, Luca Pasetto. #IsabelleHOL #ITP #Logic
• Steiner's line theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• The Steiner deltoid as the tangent envelope of Wallace-Simson lines in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math

Rocq

• Formally certifying the vertex set of a polyhedron faster than informal enumeration. ~ Xavier Allamigeon, Yazid Id-Sahra, Pierre-Yves Strub. #RocqProver #ITP #Math

Inteligencia artificial para las matemáticas (AI4Math)

• Agentic approach to computer algebra systems. ~ Bartosz Naskręcki et al. #AI4Math #CAS
• Could AI help mathematics escape the meritocracy trap?. ~ Anonymous mathematician in the United States. #AI4Math
• Is AI the end of math as we know it?. ~ Jordana Cepelewicz. #AI4Math
• Is mathematics over, or just graduating?. ~ Christian Szegedy. #AI4Math
• Math 2.0. ~ Terence Tao. #AI4Math
• Navigating the risks of AI in academia. ~ Sahana Balasubramanya. #AI4Math
• On OpenAI’s release of mathematical results. ~ Advisory Group on Mathematics and Artificial Intelligence. #AI4Math
• Solving open research problems together (Mathematicians and Muse Spark collaborate on six research papers). ~ Meata AI. #AI4Math
• The future of mathematics. ~ Jeremy Avigad. #AI4Math
• What should we tell our students?. ~ Álvaro Lozano-Robledo. #AI4Math

Haskell

• Online edition of "Haskell: the craft of functional programming". ~ Simon Thompson. #Haskell #FunctionalProgramming

Contenido en español

Enseñanza de Lean 4

• Lean 4 para matemáticos: guía docente. #LeanProver #ITP #Math

Retos de Lean 4 (RetoLean4)

• Enunciado del reto 22 de Lean 4: Si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente. #RetoLean4 #LeanProver #ITP #Math
• Soluciones del reto 21 de Lean 4: Las subsucesiones tienen el mismo límite que la sucesión. #RetoLean4 #LeanProver #ITP #Math

Inteligencia artificial para las matemáticas (AI4Math)

• Debate sobre Matemáticas e IA: IA en EDPs. ~ Javier Gómez Serrano. #AI4Math
• Reseña de «Is AI the end of math as we know it?». #AI4Math
• Reseña de «Is mathematics over, or just graduating?». #AI4Math
• Reseña de «Navigating the risks of AI in academia». #AI4Math
• Reseña de «The future of mathematics». #AI4Math

Lista anterior

• Weekly reads: Sep 28 – Oct 4, 2026. #AI4Math #Agda #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver