The readings shared in Mastodon on 10 August 2026 are:

• A formalization of the mean-field derivation of the Vlasov equation (Mathematician in the loop: AI-assisted Lean formalization as a strategy game). ~ Joseph K. Miller. #LeanProver #ITP #AI4Math
• Certified program synthesis with a multi-modal verifier. ~ Yueyang Feng et als. #LeanProver #FormalVerification
• Every quasiperfect number has at least eight distinct prime factors. ~ Akira Toyohara, Ye Tao, Siqiong Yao. #LeanProver #ITP #AI4Math
• Fitting’s theorem and semirings of normal subgroups. ~ Damiano Testa. #LeanProver #ITP #AI4Math
• Formally certifying number field invariants. ~ Alain Chavarri Villarello, Sander R. Dahmen. #LeanProver #ITP #Math
• Game hopping in Lean. ~ Stefan Dziembowski, Grzegorz Fabiański, Daniele Micciancio, Rafał Stefański. #LeanProver #ITP
• Lean refactor: Multi-objective controllable proof optimization via agentic strategy search. ~ Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang. #LeanProver #ITP #AI4Math
• Lean4Lean: Verifying a typechecker for Lean, in Lean. ~ Mario Carneiro. #LeanProver #ITP
• LeanCSP: A framework for certifying constraint reformulation and solving in Lean. ~ Pablo Manrique, Stefan Szeider. #LeanProver #ITP
• MechGeo: Autoformalizing and proving euclidean geometry in Lean 4. ~ Hao Shen, Junyu Guo, Tian Cui, Yuxuan Xiao, Lihong Zhi. #AI4Math #LeanProver #ITP
• Postmortem for kernel soundness bug #14576. ~ Leonardo de Moura. #LeanProver #ITP
• The Lean theorem prover: design, evolution, and impact. ~ Leo de Moura. #LeanProver #ITP
• Topological semantics for scoped computational paths. ~ Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago M. L. de Veras. #LeanProver #ITP #Math
• Un error en el núcleo de Lean aprovechado por una IA para refutar la conjetura de Collatz. ~ Francisco R. Villatoro. #LeanProver #ITP #Math
• Verifying Verus: A Lean 4 formalization of the SST-to-AIR expression translation. ~ Shuge Rong. #LeanProver #ITP
• A deep embedding of HOL in HOL: soundness, completeness, consistency. ~ Christoph Benzmüller, Daniel Kirchner. #IsabelleHOL #ITP
• A formal counterexample to the cost-preserving single-source unsplittable flow conjecture (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP
• Completeness of the Q₀ higher-order logic (in Isabelle/HOL). ~ Asta Halkjær From, Jonathan Julian Huerta Munive, Anders Schlichtkrull. #IsabelleHOL #ITP #Logic
• Isabelle: the last 40 years (and the next). ~ Lawrence Paulson. #IsabelleHOL #ITP
• The Wallace-Simson line theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Verifying and generalizing simultaneous critical pairs. ~ René Thiemann. #IsabelleHOL #ITP #Math
• 0/1-Polytopes with exponentially small edge expansion. ~ Xiongxin Yang. #AI4Math
• A bijective proof of a partition theorem of Berkovich and Uncu. ~ Michal Mogielnicki, Ken Ono, Niels Voss, Jujian Zhang. #AI4Math #LeanProver #ITP
• Completeness of the model space does not force regularity for infinite-dimensional Lie groups. ~ Zongjian Han1, Fungo Liu. #AI4Math
• How we solved PutnamBench (A look at formally proving undergraduate competition mathematics). #AI4Math #IsabelleHOL
• Mathematical scientific discovery using large language models: a systematic literature review. ~ Vinita Gangaram Jansari et als. #AI4Math
• Mathematicians address artificial intelligence. ~ David H Bailey. #AI4Math
• Mathematicians are grappling with the possibility that AI might eclipse them. ~ Kai Williams. #AI4Math
• Polynomial-time MIMO detection at the maximum-likelihood threshold. ~ Dimitris Papailiopoulos. #AI4Math
• PutnamBench Leaderboard (Benchmarking formal mathematical reasoning on the Putnam Mathematical Competition). #AI4Math #LeanProver #IsabelleHOL #Coq
• PutnamBench: A Multilingual competition-mathematics benchmark for formal theorem-proving. ~ George Tsoukalas et als. #AI4Math
• Why the legendary Erdős problems are falling to AI. ~ Konstantin Kakaes. #AI4Math
• Twenty years of Pandoc. #Haskell #FunctionalProgramming
• Independent analysis of AI (Understand the AI landscape to choose the best model and provider for your use case). #AI
• La lista de los más listos de la clase: el análisis de la «inteligencia» de las IA (y sus precios) en una sola página. ~ @Alvy. #AI
• #RetoLean4: Enunciado del reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). #LeanProver #ITP #Math
• #RetoLean4: Enunciado del reto 14 (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 12 (Si aₙ → L, bₙ → M y L < M, entonces eventualmente aₙ < bₙ). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 13 (Desigualdad triangular inversa: ||x| - |y|| ≤ |x - y|). #LeanProver #ITP #Math
• #Retolean4: Vídeo tutorial sobre cómo resolver el reto 12. #LeanProver #ITP #Math
• #Retolean4: Vídeo tutorial sobre cómo resolver el reto 13. #LeanProver #ITP #Math