The readings shared in Mastodon on 27 July 2026 are:

• A Lean tactic for normalizing expressions in an algebra over a ring. ~ Arend Mellendijk. #LeanProver #ITP
• An end-to-end verification of Keller’s conjecture. ~ James Gallicchio, Cayden Codel, Jeremy Avigad, Marijn J. H. Heule. #LeanProver #ITP #Math
• Cofinite zeros of high derivatives. ~ Eric Hou. #LeanProver #ITP #Math
• Formalizing the Bruck–Ryser–Chowla theorem: Combinatorial design theory in Lean. ~ Eric Jonathan Wang, Elif Uskuplu. #LeanProver #ITP
• Formalizing the Wu-Ritt characteristic set method in Lean 4. ~ Yuxuan Xiao, Hao Shen, Junyu Guo, Dingkang Wang, Lihong Zhi. #LeanProver #ITP #Math
• From Dag-Like proofs to boolean circuits in Lean. ~ Lorenzo Saraiva, Edward Hermann Haeusler. #LeanProver #ITP
• grind: An SMT-inspired tactic for Lean 4. ~ Kim Morrison, Leonardo de Moura. #LeanProver #ITP
• Formal verification of an explicit counterexample to the jacobian conjecture. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• On the formal verification of polynomial commitments: two KZG constructions and the algebraic group model. ~ Tobias Rothmann. #IsabelleHOL #ITP
• Formalising standard deontic logic and dyadic deontic logic in Rocq. ~ Sophie Krijgsman. #RocqProver #ITP #Logic
• Dependent types for compiler calculation. ~ Mitchell Pickard. #Agda #ITP
• Topology in synthetic domain theory and its formalisation in Agda. ~ Runze Xue. #Agda #ITP #Math
• An audited human-AI loop for trustworthy Lean formalization: axiom-budget auditing, a goal-directed state report, and a conditional general-relativity case study. ~ Paweł Kapłański. #AI4Math #LeanProver #ITP
• Case study: proving sqrt(2) irrational with LPTP and an LLM. ~ Fred Mesnard, Étienne Payet, Wim Vanhoof. #AI4Math #LPTP #Prolog
• Case study: solving P-99 with LPTP and an LLM. ~ Fred Mesnard, Thierry Marianne, Étienne Payet, Wim Vanhoof. #AI4Math #LPTP #Prolog
• Encontrado un contraejemplo de la conjetura jacobiana con Claude Fable 5. ~ Miguel Ángel Morales. #AI4Math
• Human mathematicians are being outcounterexampled. ~ Kevin Buzzard. #AI4Math
• Interview: Terence Tao on AI. #AI4Math
• LeanFlow: A case study in workflow-driven Lean autoformalization. ~ Lazar Milikic, Simon Guilloud, Khanh Nguyen, Viktor Kuncak. #AI4Math #LeanProver #ITP
• Mathematical discovery in the wild: AI-guided proofs in Banach space theory. ~ Antonio Acuaviva, Pablo Acuaviva. #AI4Math
• Mathematics in the age of AI. ~ Terence Tao. #AI4Math
• On some problems from the Kourovka notebook. ~ Wouter van Doorn, Elias Judin, Pietro Monticone, Daniel Morrison. #AI4Math #LeanProver #ITP #Aristotle
• Should we trust AI-generated formal proofs in Lean 4? ~ MathOverflow. #AI4Math
• Tau Ceti: a repository of formal mathematics, directed by human-written roadmaps, implemented and maintained by AI contributors, subject to adversarial review. ~ Kim Morrison et als. #AI4Math #LeanProver #ITP
• Terence Tao on AI in mathematics (and beyond). #AI4Math
• How to read mathematics? (A study guide). ~ Petra Schwer. #Math
• Open weights and american AI leadership. #AI