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

El hilo principal de esta semana vuelve a ser las matemáticas en la era de la IA. Cuatro lecturas proceden de la serie Proofs and Prompts: Filippo A. E. Nuccio sobre la formalización como manifestación concreta de la comprensión matemática, Nihar Gargava sobre por qué es un gran momento para ser matemático aficionado, Isabelle Gallagher sobre las matemáticas lentas y Beckett Bradford sobre lo que hace la IA por los estudiantes de olimpiadas. El blog de Terence Tao aloja otras dos aportaciones: «Mathematics has changed. Let's act like it», de Frank Calegari, y «Egoless mathematics in the AI era», de Karthik C. S., Amit Sahai y Jie Xue. Dos vídeos completan el hilo: «Mathematicians in the time of AI», de Yu Deng, y «Math 2.0», del propio Tao.

La sección de Lean 4 combina proyectos de formalización con aplicaciones. El Proyecto Stacks se ha formalizado en Lean y TechCrunch informa sobre el propósito de Axiom Math de mantener la basura generada por IA fuera de las matemáticas. Entre las aplicaciones están la diferenciación automática certificada, la integral de camino de Henstock-Kurzweil y el cálculo de Wick de operadores, el código genético, un problema de numberlink en zigzag con dos colores y KAPPA, que comprueba las demostraciones de artículos de estadística con Lean 4 y agentes basados en modelos de lenguaje. También hay nuevos resultados en teoría espectral de grafos y sobre las conjeturas de Kaplansky.

El resto de las lecturas técnicas se ocupa de otros asistentes de pruebas: cinco entradas de Isabelle/HOL del Archivo de Pruebas Formales (entre ellas el teorema de Abel-Ruffini, de Paulson), deques verificados con catenación en Rocq y ProofStudio, que lleva cinco asistentes de pruebas al navegador. En la sección de matemáticas, Voevodsky explica los orígenes de los fundamentos univalentes y Gaussianos comenta la demostración de los 200 TB sobre ternas pitagóricas.

La sección final recoge mis propios contenidos: los retos de Lean 4.

Lean 4

• Algebraic completeness of Feynman premeasures: The Henstock-Kurzweil path integral and operator wick calculus in Lean 4. ~ Yu. N. Berdinsky. #LeanProver #ITP #Math
• Automatic certified differentiation in Lean. ~ Ramy Shahin. #LeanProver #ITP #Math
• Axiom Math wants to keep AI slop out of mathematics. ~ Aditya Mehta. #LeanProver #ITP #AI4Math
• Kaplansky's conjectures fail for torsion-free hyperbolic groups in positive characteristic. ~ Nidhal Mghirbi, Seth Douglas. #LeanProver #ITP #AI4Math
• KAPPA: Checking the proofs in statistics papers with Lean 4 and language model agents. ~ Zihua She, Xiao Wang. #LeanProver #ITP #AI4Math
• Lemmas and conjectures in spectral graph theory. ~ Tristan Cazenave. #LeanProver #ITP #AI4Math
• Reasoning about the Genetic Code in Lean. ~ Colin T. Jones, Tyler R. Josephson. #LeanProver #ITP
• The Stacks Project, formalized in Lean. #LeanProver #ITP #AI4Math
• Two-colour zig-zag numberlink on rectangles: a forbidden-pattern characterization, a constructive polynomial-time algorithm, and a Lean verification. ~ Zzyv Zzyzek. #LeanProver #ITP

Isabelle/HOL

• Cauchy's functional equation (in Isabelle/HOL). ~ Michikazu Hirata. #IsabelleHOL #ITP #Math
• Extreme value theory (in Isabelle/HOL). ~ Michikazu Hirata. #IsabelleHOL #ITP #Math
• Finite-dimensional algebras and scalar towers. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Regular variation (in Isabelle/HOL). ~ Michikazu Hirata. #IsabelleHOL #ITP #Math
• The Abel-Ruffini theorem and the unsolvability of the quintic (in Isabelle/HOL). ~ Lawrence C. Paulson. #IsabelleHOL #ITP #Math

Rocq y otros asistentes de pruebas

• ProofStudio: Five proof assistants in the browser. ~ Yutaka Nagashima. #IsabelleHOL #LeanProver #RocqProver #HOL4 #HOL_Light #ITP
• Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. #RocqProver #OCaml

Matemáticas

• Formalisation as a concrete manifestation of mathematical understanding. ~ Filippo A. E. Nuccio. #Math #Formalisation
• Pitágoras y la demostración de los 200 TB. ~ Miguel Ángel Morales. #Math #ATP #SAT_Solving
• The origins and motivations of univalent foundations (A personal mission to develop computer proof verification to avoid mathematical mistakes). ~ Vladimir Voevodsky (2014). #Math

Inteligencia artificial para las matemáticas (AI4Math)

• Egoless mathematics in the AI era. ~ Karthik C. S., Amit Sahai, Jie Xue. #AI4Math
• It's a great time to be an amateur mathematician. ~ Nihar Gargava. #AI4Math
• Math 2.0. ~ Terence Tao. #AI4Math
• Mathematicians in the time of AI. ~ Yu Deng. #AI4Math
• Mathematics has changed. Let's act like it. ~ Frank Calegari. #AI4Math
• Slow maths. ~ Isabelle Gallagher. #AI4Math
• What does AI do for olympiad students?. ~ Beckett Bradford. #AI4Math

Retos de Lean 4 (RetoLean4)

• Reto 15 de Lean 4: Existe k ∈ ℕ tal que, para todo n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ. #RetoLean4 #LeanProver #ITP #Math
• Reto 16 de Lean 4: Para todo n ∈ ℕ, n(n+1)(2n+1) es divisible por 6. #RetoLean4 #LeanProver #ITP #Math
• Reto 17 de Lean 4: Las sucesiones convergentes son acotadas. #RetoLean4 #LeanProver #ITP #Math
• Reto 18 de Lean 4: Convergencia del producto de sucesiones convergentes. #RetoLean4 #LeanProver #ITP #Math
• Reto 19 de Lean 4: Las sucesiones convergentes son sucesiones de Cauchy. #RetoLean4 #LeanProver #ITP #Math
• Reto 20 de Lean 4: Si aₙ → L y M es una cota superior de aₙ, entonces L ≤ M. #RetoLean4 #LeanProver #LeanLang #ITP #Math
• Soluciones del reto 25 de Lean 4: Si la mezcla de dos sucesiones converge a L, entonces ambas convergen a L. #RetoLean4 #LeanProver #ITP #Math
• Reto 26 de Lean 4: Producto de una sucesión de límite cero por una sucesión acotada. #RetoLean4 #LeanProver #ITP #Math

Lista anterior

• Lecturas de la semana: 19 – 25 oct 2026. #AI #AI4Math #ITP #Lean4Challenge #LeanProver #Logic #LogicProgramming #Math #Prolog #RetoLean4