Lecturas de la semana: 26 oct – 1 nov 2026
Aquí están las 27 lecturas que compartí en Mastodon durante la semana pasada.
El hilo principal de esta semana es, una vez más, el futuro de las matemáticas en la era de la IA, ahora con dos informes de la comunidad: "The mathematical sciences in an AI-enabled world", de Christoph Reisinger et al., y el informe del "Summit on math research in the age of AI". La serie Proofs and Prompts aporta a Tim Gehrunger sobre las revisiones por IA, a Patrick Morris sobre si deberíamos dejar de escribir artículos y a Alonso Castillo-Ramirez sobre el uso de la IA para corregir la literatura matemática. El blog de Terence Tao acoge a Gireeja Ranade sobre la educación y un problema de bienes públicos, Celina Zhao se pregunta en Science si se puede confiar en las demostraciones de la IA y Lauren Williams ofrece una valoración matizada de la capacidad de la IA para resolver problemas matemáticos en una charla sobre First Proof.
La sección de Lean 4 está dominada por la formalización a gran escala: Axiom ha formalizado la clasificación de los grupos simples finitos, la demostración más larga de la historia de las matemáticas. También incluye PaperFormalizer, un enfoque para autoformalizar artículos de investigación, las degeneraciones de álgebras de Jordan y la formalización del razonamiento sobre el código genético.
La sección de Isabelle/HOL trae cinco nuevas entradas del Archive of Formal Proofs: la irracionalidad de ζ(5), las formas modulares, una versión numerable del teorema de Dilworth, el problema del viajante mediante programación dinámica y la consistencia de NK con infinito y elección. Una lectura en español sobre los números reales, de Esteban Martínez, completa la lista.
La sección final recoge mi propio contenido: los retos de Lean 4 sobre sucesiones y límites.
Lean 4
- Degenerations of Jordan algebras. ~ Victor Bovdi, Ivan Kaygorodov, Yury Popov, Azamat Saydaliyev, Yury Volkov. #LeanProver #ITP #Math
- Formalizing the Enormous Theorem. #LeanProver #ITP #AI4Math #AI #Math
- PaperFormalizer: Author-in-the-loop autoformalization of research papers in Lean. ~ Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet. #LeanProver #ITP #AI4Math #Autoformalization
- Reasoning about the genetic code in Lean. ~ Colin T. Jones, Tyler R. Josephson. #LeanProver #ITP
- The classification of finite simple groups, formalized in Lean. #LeanProver #ITP #AI4Math #AI #Math
Isabelle/HOL
- Countable infinite version of Dilworth's theorem (in Isabelle/HOL). ~ Fabián Fernando Serrano Suárez, Thaynara Arielly de Lima, Mauricio Ayala-Rincón. #IsabelleHOL #ITP #Math
- HOL in HOL over a set-theoretic universe: consistency of NK with infinity and choice. ~ Christoph Benzmüller, Daniel Kirchner. #IsabelleHOL #ITP #Logic
- Modular forms (in Isabelle/HOL). ~ Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li. #IsabelleHOL #ITP #Math
- The irrationality of ζ(5) (in Isabelle/HOL). ~ Alex Raymond Hyman. #IsabelleHOL #ITP #Math
- Travelling Salesman via dynamic programming (in Isabelle/HOL). ~ Maksym Bortin. #IsabelleHOL #ITP
Inteligencia artificial para las matemáticas (AI4Math)
- AI is shaking up math. But can its proofs be trusted?. ~ Celina Zhao. #AI4Math
- AI reviews are the new normal. ~ Tim Gehrunger. #AI4Math
- AI, mathematics, education, and a public goods problem. ~ Gireeja Ranade. #AI4Math
- Could AI help correct the mathematical literature?. ~ Alonso Castillo-Ramirez. #AI4Math
- First Proof: A nuanced assessment of AI's ability to solve math problems. ~ Lauren Williams. #AI4Math
- Let's stop writing papers…. ~ Patrick Morris. #AI4Math
- Report of "Summit on math research in the age of AI". #AI4Math
- The mathematical sciences in an AI-enabled world (Opportunities, risks and community needs). ~ Christoph Reisinger, Rachel Bearon, Thomas Bloom, Jennifer Gaskell, David Leslie, Zubin Siganporia. #AI4Math
Matemáticas
- ¿Qué son los números reales? IV. ~ Esteban Martínez. #Math
Retos de Lean 4 (RetoLean4)
- Soluciones del reto 8 de Lean 4: Unicidad del límite de las sucesiones convergentes. #RetoLean4 #LeanProver #ITP #Math
- Soluciones del reto 10 de Lean 4: Si aₙ → L con L ≠ 0, entonces |aₙ| ≥ |L|/2 eventualmente. #RetoLean4 #LeanProver #ITP #Math
- Reto 11 de Lean 4: Si aₙ converge a L, entonces |aₙ| converge a |L|. #RetoLean4 #LeanProver #ITP #Math
- Reto 12 de Lean 4: Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ. #RetoLean4 #LeanProver #ITP #Math
- Reto 13 de Lean 4: Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|. #RetoLean4 #LeanProver #ITP #Math
- Reto 14 de Lean 4: Para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴. #RetoLean4 #LeanProver #ITP #Math
- Soluciones del reto 24 de Lean 4: La sucesión 1, -1, 1, -1,... no es convergente (2.ª versión). #RetoLean4 #LeanProver #ITP #Math
- Reto 25 de Lean 4: Si la mezcla de dos sucesiones converge a L, entonces ambas convergen a L. #RetoLean4 #LeanProver #ITP #Math
Lista anterior
- Weekly reads: Oct 19 – Oct 25, 2026. #AI #AI4Math #ITP #LeanProver #Logic #LogicProgramming #Math #Prolog #RetoLean4