Estas son las 42 lecturas que he compartido en Mastodon durante la semana pasada.

El hilo principal de esta semana es, de nuevo, el futuro de las matemáticas en la era de la IA. La mayoría de las lecturas de AI4Math proceden de la serie Proofs and Prompts: la pregunta sobre quiénes serán los nuevos matemáticos de las Matemáticas 2.0 y las respuestas que ha suscitado (Álvaro Lozano-Robledo), una crítica de la economía matemática (Álvaro Gutiérrez), András Juhász sobre bien público, reconocimiento y educación, Marcus Zibrowius sobre el rechazo a la IA, la carta de David A. Madore a un estudiante preocupado, Dave Anderson sobre el bosque oscuro, Helmut Hofer sobre quién liderará la IA matemática y «Mathematics of the future», de Pavel Etingof et al. El blog de Terence Tao acoge otras dos perspectivas, de Tristan Buckmaster y Francesco Maggi, y el propio Tao propone un desafío experimental de IA y matemáticas sobre los ceros de Siegel. Konstantin Kakaes comenta en Quanta Magazine la demostración mediante IA de la hipótesis cuasi-Riemann, y el benchmark REUF2F evalúa agentes de programación sobre problemas de investigación de grado formalizados.

La sección de Lean 4 combina nuevas formalizaciones con reflexiones sobre el propio sistema: la formalización de la teoría de modelos de Yunus Maranki, el teorema de interpolación real para el proyecto Carleson, la falsedad de la condición (TU) de Isaac y el exponente de irracionalidad del período de la lemniscata. También merecen una mirada «Maestro», sobre el desarrollo agéntico de demostraciones formales, «Reflections on trusting Lean», de Lorenzo Bresolin y Marcello Mamino, y los valores de Mathlib. Una lectura sobre Prolog y programación lógica, «Simply logical», completa la parte técnica.

Las secciones finales recogen mis propios contenidos: los retos de Lean 4 (en español y en inglés) y mis reseñas de cuatro de las entradas de AI4Math.

Lean 4

• Formalization of model theory in Lean. ~ Yunus Maranki. #LeanProver #ITP #Logic #Math
• Formalization of the real interpolation theorem for the Carleson project. ~ Jim Portegies, Michael Rothgang. #LeanProver #ITP #Math
• Isaac's condition (TU) is false. ~ Ralf Stephan. #LeanProver #ITP #Math
• Maestro: Agentic formal proof development by coordination. ~ Haoyu Li et al. #LeanProver #ITP #AI4Math
• Mathlib's values. #LeanProver #ITP
• Reflections on trusting Lean. ~ Lorenzo Bresolin, Marcello Mamino. #LeanProver #ITP #Logic #Math
• The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization. ~ Gregory V. Chudnovsky. #LeanProver #ITP #AI4Math

Programación lógica

• Simply logical - The first three decades. ~ Peter Flach, Kacper Sokol, Jan Wielemaker. #Prolog #LogicProgramming

Inteligencia artificial para las matemáticas (AI4Math)

• A critique of the mathematical economy. ~ Álvaro Gutiérrez. #AI4Math
• A response to “Who will become the new mathematicians of Math 2.0?”. ~ Álvaro Lozano-Robledo. #AI4Math #AI #Math
• AI and mathematics: public good, credit, and education. ~ András Juhász. #AI4Math #AI #Math
• AI proved the quasi-Riemann hypothesis. What happens now?. ~ Konstantin Kakaes. #AI4Math
• An experimental AI-math challenge: using tenth discriminant bounds to explore arguments ruling out Siegel zeroes. ~ Terence Tao. #AI4Math
• Disgusted by AI?. ~ Marcus Zibrowius. #AI4Math
• Letter to a worried student. ~ David A. Madore. #AI4Math
• Mathematics in the dark forest. ~ Dave Anderson. #AI4Math
• Mathematics is a subject for the young. ~ Tristan Buckmaster. #AI4Math
• Mathematics of the future. ~ Pavel Etingof et al. #AI4Math
• Recommendations on the use of AI for PhD students and supervisors. #AI4Math
• REUF2F: Benchmarking coding agents on formalized undergraduate research problems. ~ Zeyu Zheng et al. #AI4Math
• The power of beauty and elegance. ~ Márton Balázs. #AI4Math
• Thinking hard above AI. ~ Benjamin Merlin Bumpus. #AI4Math
• Who will become the new mathematicians of Math 2.0?. #AI4Math
• Who will lead mathematical AI?. ~ Helmut H. W. Hofer. #AI4Math
• Will it be a golden age or a dark age for mathematics (and science)?. ~ Francesco Maggi. #AI4Math

Retos de Lean 4 (RetoLean4)

• Reto 24 de Lean 4: La sucesión 1, -1, 1, -1,... no es convergente (usando el Reto 22). #RetoLean4 #LeanProver #ITP #Math
• Soluciones del reto 23 de Lean 4: La sucesión constante aₙ = L converge a L. #RetoLean4 #LeanProver #ITP #Math

Reseñas

• Reseña de «Disgusted by AI?». #AI4Math
• Reseña de «Mathematics is a subject for the young». #AI4Math #AI #Math
• Reseña de «Mathematics of the future». #AI4Math
• Reseña de «Towards a world mathematical commons». #AI4Math #LeanProver #ITP #AI #Math

Contenido en inglés

Lean 4 challenges (Lean4Challenge)

• Challenge 3: If aₙ converges to L, then 2aₙ converges to 2L. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 4: There are infinitely many prime numbers. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 5: 5²ⁿ - 2³ⁿ is divisible by 17. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 6: If aₙ and cₙ converge to L and aₙ ≤ bₙ ≤ cₙ for all n, then bₙ converges to L. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 7: The composition of injective functions is injective. #LeanProver #ITP #Math #Lean4Challenge
• Solutions to Challenge 23: The constant sequence aₙ = L converges to L. #Lean4Challenge #LeanProver #ITP #Math
• Challenge 24: The sequence 1, -1, 1, -1,... is not convergent (using Challenge 22). #Lean4Challenge #LeanProver #ITP #Math

Reviews

• Review of «Disgusted by AI?». #AI4Math
• Review of «Mathematics is a subject for the young». #AI4Math #AI #Math
• Review of «Mathematics of the future». #AI4Math
• Review of «Towards a world mathematical commons». #AI4Math #LeanProver #ITP #AI #Math

Lista anterior

• Lecturas de la semana: 12 oct – 18 oct 2026. #AI #AI4Math #ITP #Lean4Challenge #LeanProver #Math #RetoLean4