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

El hilo principal de esta semana es el papel de la IA en la práctica matemática y en la ética de la investigación. Casi todas las lecturas de AI4Math proceden de la serie Proofs and Prompts: Thomas Sinclair sobre la libertad de investigación, Hendrik De Bie sobre las declaraciones de uso de IA en los artículos de matemáticas, Michel Schellekens sobre la IA fiable, Thomas Koberda y Alex Kontorovich sobre el teorema dialéctico, y Benjamin Braun sobre la transformación de las matemáticas. Lawrence Paulson aporta una reflexión relacionada sobre el plagio en la era de la IA.

La sección de Lean 4 está dominada por nuevas formalizaciones: la refutación de la conjetura de Ramaekers, un contraejemplo al problema 108 de Erdős, la desigualdad de Vasc de once variables, las álgebras de banderas, la medida de irracionalidad del logaritmo de un número racional, los polítopos de pedigrí y las álgebras de relaciones de términos. También merece la pena leer «How to formalize all of mathematics», de Avigad, Buzzard, Commelin, Degenne, Morrison, Nash y Topaz.

Las últimas secciones recogen contenido propio: los retos de Lean 4 y una entrada sobre los números reales.

Lean 4

• A counterexample to Erdős problem 108 via arc graphs. ~ Jensen Kohlmeyer, Liam Kruer. #LeanProver #ITP #Math
• A Lean formalisation of the disproof of Ramaekers's conjecture. ~ Jeremy Tan. #LeanProver #ITP #Math
• An efficient, Lean 4 verified necessary and sufficient condition for membership in pedigree polytopes. ~ T.S. Arthanari. #LeanProver #ITP #AI4Math
• Exact rational certificates and a Lean formalization of the eleven-variable Vasc inequality. ~ Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao. #LeanProver #ITP
• Formalizing flag algebras in Lean. ~ Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang. #LeanProver #ITP #AI4Math
• How to formalize all of mathematics. ~ Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz. #LeanProver #ITP #AI4Math
• Lean 4 for mathematicians: a teacher's guide. #LeanProver #ITP #Math
• Mechanizing term relation algebras: the basic theory. ~ Jacopo Angeli. #LeanProver #ITP
• The irrationality measure of the logarithm of a rational number is 2. ~ Dan Brown. #LeanProver #ITP #Math

Inteligencia artificial para las matemáticas (AI4Math)

• Free inquiry in mathematics. ~ Thomas Sinclair. #AI4Math
• On AI statements in mathematics papers. ~ Hendrik De Bie. #AI4Math
• On our existential crisis and trustworthy AI. ~ Michel Schellekens. #AI4Math
• Plagiarism in the age of AI. ~ Lawrence Paulson. #AI
• The dialectical theorem. ~ Thomas Koberda, Alex Kontorovich. #AI4Math
• Transforming mathematics. ~ Benjamin Braun. #AI4Math

Retos de Lean 4

• Challenge 1: Prove in Lean 4 that the sequence 1/n converges to 0. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 2: The sequence 1, -1, 1, -1,... is not convergent. #LeanProver #ITP #Math #Lean4Challenge
• Enunciado del reto 23 de Lean 4: La sucesión constante aₙ = L converge a L. #RetoLean4 #LeanProver #ITP #Math
• Soluciones 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

Matemáticas

• ¿Qué son los números reales? III. ~ Esteban Martínez. #Math

Lista anterior

• Weekly reads: Oct 5 – Oct 11, 2026. #AI4Math #Autoformalization #CAS #FunctionalProgramming #Haskell #IsabelleHOL #ITP #LeanProver #Logic #Math #RetoLean4 #RocqProver