The readings shared in Mastodon on 21 September 2026 are:

• A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs. ~ Shenghao Yang, Yanyan Dong. #LeanProver #ITP #AI4Math
• Descriptive complexity in Lean: completeness by first-order reductions. ~ Pierre Senellart, Anton Gnatenko. #LeanProver #ITP #AI4Math
• Formalization of Sullivan's no wandering domains theorem in Lean. ~ Ziang Li, Yusheng Luo. #LeanProver #ITP #AI4Math
• Henstock-Kurzweil gauge integral in the non–gaussian regime: a machine-verified construction. ~ Yuri N. Berdinsky. #LeanProver #ITP
• Lean metaprogramming etudes: execution is elaboration. ~ Philip Zucker. #LeanProver #ITP #FunctionalProgramming
• Lean-certified infinite counterexamples to written on the Wall II Conjecture 194. ~ Cameron Beeley. #LeanProver #ITP #AI4Math
• Mechanizing Gödel's incompleteness theorems and provability logic. ~ Shogo Saitou, Mashu Noguchi. #LeanProver #ITP #AI4Math
• Palindromic length in free groups: reflections, noncrossing matchings, and Catalan. ~ Junjie Liao. #LeanProver #ITP
• Fast chinese remaindering via product trees (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP
• Greibach’s hardest context-free language (in Isabelle/HOL). ~ Tobias Nipkow. #IsabelleHOL #ITP
• Napoleon's theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Strong normalization for Church-style system F (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP
• Structuring mathematics in dependent type theory. ~ Cyril Cohen. #RocqProver #ITP #Math
• A CERN for AI-assisted science? ~ Dimitris Koukoulopoulos. #AI4Math
• A beginning for mathematics. ~ Daniel Litt. #AI4Math
• AI and human approaches to mathematical problem solving. ~ Yang Ding. #AI4Math
• Awesome AI proofs (A curated list of mathematical proofs generated by artificial intelligent systems, verified by automated theorem prover, and a list of successes and mishaps). ~ Subhrajyoty Roy, Subrata Pal. #AI4Math
• Building open models for the mathematical community (An invitation from SAIR Foundation). #AI4Math
• Existential risk from AI: an exposition for mathematicians. ~ Xiaoyu He. #AI4Math
• Fast math/slow math. ~ Benjamin Antieau. #AI4Math
• Happy, those able to know the causes of things (An essay on LLMs and the Navier-Stokes equation). ~ Nestor Guillen. #AI4Math
• SOLVED: Navier-Stokes cracked by AI. | Numberphile ~ Tony Padilla. #AI4Math
• Stable singularity of the Euler equations on ℝ³. ~ Adarsh Ganeshram, Valentin Duruisseaux, Anima Anandkumar. #AI4Math #LeanProver #ITP
• Two responses to "A severe misalignment of AI in mathematics". ~ Timothy Nguyen, M. Levent Doğan. #AI4Math
• When inventing is not enough. ~ Lisa Valentini. #AI4Math
• Where will all the papers go? ~ David Craven. #AI4Math
• Why I didn’t sign the Fields medallists’ letter. ~ Tim Gowers. #AI4Math
• Search over algebraic graphs. ~ David Anekstein. #Haskell #FunctionalProgramming
• gptel: Emacs y la IA. ~ Notxor. #Emacs #AI
• #Calculemus: Demostraciones con Lean 4 del Reto 10 (Si aₙ → L con L ≠ 0, entonces |aₙ| ≥ |L|/2 eventualmente). #LeanProver #ITP #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 11 (Si aₙ converge a L, entonces |aₙ| converge a |L|). #LeanProver #ITP #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 12 (Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ). #LeanProver #ITP #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 6 (teorema del emparedado). #LeanProver #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 7 (La composición de funciones inyectivas es inyectiva). #LeanProver #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 8 (Sucesiones con infinitos términos grandes no convergen a límites pequeños). #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 9 (Unicidad del límite). #LeanProver #ITP #Math
• #RetoLean4: Enunciado del reto 19 (Las sucesiones convergentes son de Cauchy). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 18 (Convergencia del producto de sucesiones convergentes). #LeanProver #ITP #Math