The readings shared in Mastodon on 24 August 2026 are:

• A Lean formalization of the main theorem of the paper "Low-rank univariate sum of squares has no spurious local minima". ~ Chenyang Yuan. #LeanProver #ITP #AI4Math
• A barrier-free synchronization algorithm for multi-engine AI accelerators. ~ Chungha Sung, Nikil V. Shyamsunder, Hanliang Zhang, Daniel Kroening, Joonwon Choi. #LeanProver #ITP
• A proof of the Regts–Sevenster conjecture, formalized. ~ William Whistler. #LeanProver #ITP #AI4Math
• Cardinality of topological bases of a finite set. ~ Lars Warren Ericson. #LeanProver #ITP #Math
• Erdős problem #501 in Lean 4. ~ Elliot Glazer. #LeanProver #ITP #Math #AI4Math
• A Lean 4 formalization of Pick's theorem, the polygonal Jordan curve theorem, the full Jordan curve theorem, and Radó's theorem. ~ Rado Kirov. #LeanProver #ITP #AI4Math
• Cantor measures with odd base do not admit Fourier frames. ~ Jaume de Dios Pont, Lukas Liehr, Mitchell A. Taylor. #LeanProver #ITP #Math
• Formalizing extended complex numbers, Möbius transformations, and cross ratio in Lean 4. ~ Fubin Yan, Kenneth W. Shum. #LeanProver #ITP #Math
• Lean formalization of bounded gaps between primes. ~ Evan Chen, Sidharth Hariharan, Kenny Lau, Bhavik Mehta, Ken Ono, Ashvin Swaminathan, Jesse Thorner, Yunzhou Xie. #LeanProver #ITP #AI4Math
• Lean formalization of complex analysis. ~ Fubin Yan et als. #LeanProver #ITP #Math
• Lean formalization of the Sabidussi compatibility conjecture. ~ Nikolay Ulyanov. #LeanProver #ITP #Math
• Math exercises in Lean. ~ Anna Immerwahr. #LeanProver #ITP #Math
• NUSLean: Lean 4 formalization of "A near-quadratic lower bound for sets with no unique sums". ~ Xinjie He. #LeanProver #ITP #Math
• On the existence problem of regular Gabor frames. ~ Jaume de Dios Pont, Lukas Liehr, Mitchell A. Taylor. #LeanProver #ITP #AI4Math
• Palomar: A public registry of Lean-verified mathematics. #LeanProver #ITP #AI4Math
• Palomar: a registry of Lean verified mathematics. ~Terence Tao. #LeanProver #ITP #AI4Math
• Sendov's conjecture in Lean. ~ Terence Tao. #LeanProver #ITP #Math
• Stable phase retrieval for spans of independent random variables. ~ Pedro Abdalla, Jaume de Dios Pont, João P. G. Ramos, Mitchell A. Taylor. #LeanProver #ITP #AI4Math
• Constrained input/output logic in HOL: An algebraic embedding. ~ Ali Farjami, Luca Pasetto. #IsabelleHOL #ITP
• A naive encoding of Russell's paradox in type theory. ~ Zhuoyuan Qu. #CoqProver #Agda #ITP #Math
• Formal verification of Romanov's triplet logic: A verified filter for sliding-window 3-CNF with application to structured formulas. ~ Dmitry V. Alexandrov. #RocqProver #ITP #AI4Math
• Changes in the classroom in the AI Era. ~ Benjamin Jaye, Galyna V. Livshyts. #AI4Math
• LLMs make mathematics easier. Now raise the bar. ~ Marijn J. H. Heule. #AI4Math
• Response to "The AI dissenter viewpoint". ~ Anatoly Vitold Stankyavichyus. #AI4Math
• A proof of the imbalance conjecture. ~ James Alexander Schreib, Yousof Yavari. #AI4Math #LeanProver
• Human mathematics in the age of reasoning machines. ~ Akshay Venkatesh. #AI4Math
• On protecting mathematics from LLM companies’ monopoly. ~ Tian Lan. #AI4Math
• The shape of math to come. ~ Alex Kontorovich. #AI4Math #LeanProver
• Imprecise probabilistic programming, precisely (Credal sets via graded monads, BDDs, and semiring-parametric inference). ~ Jack Liell-Cock, Sam Staton. #Haskell #FunctionalProgramming
• ediprolog: Emacs does interactive Prolog. ~ Markus Triska. #Prolog #LogicProgramming #Emacs
• stdin | LLM | stdout. ~ karthink. #Emacs #LLMs
• My advice for users wanting to switch to Emacs. ~ Daniel Pinkston. #Emacs
• #Calculemus: Demostraciones con Lean 4 del Reto 2 (La sucesión 1, -1, 1, -1,… no es convergente). #LeanProver #Math
• #Calculemus: Demostraciones con Lean 4 del Reto 3 (Si aₙ converge a L, entonces 2aₙ converge a 2L). #LeanProver #Math
• #RetoLean4: Enunciado del reto 15 ((∃ k ∈ ℕ)(∀ n ∈ N)[(n + k)² ≤ 2ⁿ⁺ᵏ]). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto (para todo n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴). #LeanProver #ITP #Math
• #Retolean4: Vídeo tutorial sobre cómo resolver el reto 14. #LeanProver #ITP #Math