The readings shared in Bluesky on 12 July 2026 are:

• Almost all primes are partially regular. ~ Evan Chen et als. #LeanProver #ITP #AI4Math
• Axioms for physical reasoning: codifying the Seiberg-Witten solution in Lean. ~ Michael R. Douglas. #LeanProver #ITP
• Euclean: Automated geometry problem formalization with unified verification in Lean. ~ Linbin Tang et als. #LeanProver #ITP #AI4Math
• Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4. ~ Arnaud Mayeux, Jujian Zhang. #LeanProver #ITP #Math
• Three roads to de Finetti’s theorem in Lean 4. ~ Cameron Freer. #LeanProver #ITP #AI4Math
• Axiomatic theory of hereditarily finite sets and its fragments (in Isabelle/HOL). ~ Štěpán Holub, Zuzana Haniková. #IsabelleHOL #ITP #Math
• Bessel functions of the first kind (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• Certified infinite descent criteria (in Isabelle/HOL). ~ Jamie Wright, Liron Cohen, Reuben Rowe, Andrei Popescu. #IsabelleHOL #ITP
• Complete elliptic integrals and the arithmetic–geometric mean (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• Correctness and complexity of BMSSP in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP
• Freiman's 3k - 4 theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Generalised hypergeometric series (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• Height bounds for height-balanced trees (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP
• Rademacher's series for the partition function (in Isabelle/HOL). ~ Manuel Eberl, Lawrence C. Paulson. #IsabelleHOL #ITP #Math
• The exponential and logarithmic integral (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• The incomplete gamma function (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
• Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. #RocqProver #ITP #FunctionalProgramming
• A (24₄, 32₃)-configuration on the Schur quartic with logarithmic Chern slope 14/5. ~ Bartosz Naskręcki, Piotr Pokora. #AI4Math
• MechMath agent team: LLM driven agents for mathematical research. ~ Yichuan Cao, Ruichen Qiu, Junqi Liu, Jiaqi Wang, Dakai Guo, Ruyong Feng, Lihong Zhi, Xiao-Shan Gao. #AI4Math
• Open problems solved by LLMs? A survey of verifiable mathematical discovery. ~ Ioannis Tzachristas, Georgios Tzachristas, Aifen Sui. #AI4Math
• Data-directed programming in Haskell (SICP 2.4.3). ~ kqr. #Haskell #FunctionalProgramming
• Tagged data in Haskell (SICP 2.4.2). ~ kqr. #Haskell #FunctionalProgramming
• Demostrando lo indemostrable. ~ Esteban Martínez Vañó. #Lógica #Matemática
• Lva² (vol. 3, núm. 2), nuevo número de la revista de «Retos matemáticos». ~ Miguel Ángel Morales. #Matemáticas
• #RetoLean4: Enunciado del reto 9 (Unicidad del límite). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 8 (Demostrar que una sucesión que posee infinitos términos con valor absoluto superior a 10 no puede converger a un límite cuyo valor absoluto sea menor que 5). #LeanProver #ITP #Math
• #Retolean4: Vídeo tutorial sobre cómo resolver el reto 8 (dirigido a quienes desean empezar a demostrar con Lean). #LeanProver #ITP #Math