The readings shared in Mastodon on 31 August 2026 are:

• A Lean 4 verification report for subregular affine cells and the level −1 vertex algebra of type D, ~ Sihai Jin. #LeanProver #ITP #Math
• A formalized proof of Bondy’s minimum-degree longest-cycle conjecture. ~ Lech Mazur. #LeanProver #ITP #AI4Math
• Even integral parts of powers of square roots. ~ Ralf Stephan. #LeanProver #ITP #AI4Math
• Formalization of Harder-Narasimhan theory. ~ Yijun Yuan. #LeanProver #ITP #AI4Math
• Improved bounds for the smallest 4-chromatic graph of girth six. ~ Glauco Rampone. #LeanProver #ITP #AI4Math
• MathAdv: What theorem provers know, reason, formalize, and generalize. ~ Jiaxin Yuan et als. #LeanProver #ITP #AI4Math
• Number theory game (An introduction to integer arithmetic and formal proofs). ~ kostya88. #LeanProver #ITP #Math
• ProofJudge: Tool-grounded LLM evaluation of formal proof quality in Mathlib. ~ Shane Caldwell. #LeanProver #ITP #AI4Math
• Prove2Me: An open collaborative platform for scaling math formalization. ~ Shuze Chen, Xiaoyang Lu, Kunal Marwaha, Tianyi Peng, Henry Yuen. #LeanProver #ITP #AI4Math
• Laurent series expansions on an annulus (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• Miquel's theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Multitape Turing machine substrate (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. #IsabelleHOL #ITP
• Multitape alphabet enlargement (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. #IsabelleHOL #ITP
• Multitape alphabet reduction (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. #IsabelleHOL #ITP
• Multitape alphabet roundtrip (in Isabelle/HOL). ~ András Z. Salamon, Michael Wehar. #IsabelleHOL #ITP
• Proving total correctness of top-down solvers with widening and narrowing. ~ Sarah Tilscher, Alexandra Graß, Helmut Seidl, Yannick Stade. #IsabelleHOL #ITP
• Trace based semantics for rely guarantee (in Isabelle/HOL). ~ Marialena Hadjikosti, Andrei Popescu, Jamie Wright. #IsabelleHOL #ITP
• A simple formalization of alpha-equivalence. ~ Kalmer Apinis, Danel Ahman. #RocqProver #ITP
• Autoformalizing the calculation of π₃(S²). ~ Daniel Carranza, Chunyi Liu, Emily Riehl, Egbert Rijke. #Agda #ITP #AI4Math
• Autonomous mathematical discovery in an open-world multi-agent environment. ~ Stephen Chung, Wenyu Du, William J. Wesley. #AI4Math
• Evaluating mathematical merit (AI-reproducible work, human mathematical contribution, and a residual evaluation framework). ~ Qi Guo. #AI4Math
• Mathematics and the LLM: 2026 (A letter to the mathematical community, to be published in the Notices of the AMS). ~ Marco Gualtieri. #AI4Math
• Statement on AI usage for PhD students. ~ Manuel Rivera. #AI4Math
• What is mathematics now, and what should it be? ~ Jeremy Avigad. #AI4Math
• A curmudgeon tries a language server. ~ kqr. #Haskell #FunctionalProgramming #Emacs #Lisp
• Haskell diagrams: Tessellations. ~ Marcelo Garlet Milani. #Haskell #FunctionalProgramming
• (WITH-AI …) ~ Joe Marshall. #CommonLisp #AI4Coding
• Will it Lisp? ~ Joe Marshall. #CommonLisp #VibeCoding
• Does computer science need computers? ~ Ben Brubaker. #CompSci
• Un cuerno finito-infinito. ~ Miguel Ángel Morales. #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 5 (5²ⁿ - 2³ⁿ es divisible por 17). #LeanProver #Math
• #Calculemus: Demostraciones en Lean 4 del Reto 4 (Existen infinitos números primos). #LeanProver #Math
• #RetoLean4: Enunciado del reto 17 (las sucesiones convergentes están acotadas). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 16 (para todo n ∈ N, n(n+1)(2n+1) es divisible por 6). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 15 ((∃ k ∈ ℕ)(∀ n ∈ N)[(n + k)² ≤ 2ⁿ⁺ᵏ]). #LeanProver #ITP #Math
• #RetoLean4: Enunciado del reto 16 (para todo n ∈ N, n(n+1)(2n+1) es divisible por 6). #LeanProver #ITP #Math