The readings shared in Bluesky on 5 July 2026 are:

• An explicit eventual p⁴-divisibility theorem for an Apery-type numerator family. ~ Zhipeng Chen, Qisheng Wang, Yan Feng. #LeanProver #ITP #Math
• Axiom-audited trustworthy formalization of game-theoretic commitment in Lean. ~ Jan Ondras. #LeanProver #ITP
• Classifying the groups of order p³ in Lean. ~ Li Xiang. #LeanProver #ITP #Math
• Formalization of formal group laws. ~ Wenrong Zou. #LeanProver #ITP #Math
• Formalized q-series: The Rogers-Ramanujan identities and beyond. ~ Kenny Lau, Seewoo Lee, Ken Ono. #LeanProver #ITP #Math
• Formalizing Scarf, Brouwer, and Nash in Lean. ~ Yuwei Lyu, Kai Li. #LeanProver #ITP #Math
• From agents to axioms: Verifier-gated Lean formalization for statistical learning theory. ~ Robert Sneiderman. #LeanProver #ITP
• Mechanizing proofs from a course on programming language semantics in Lean. ~ Hampus Toft. #LeanProver #ITP
• Reformalization of the Jordan curve theorem. ~ Simon Guilloud, Sankalp Gambhir, Samuel Chassot. #Mizar #LeanProver #HOL_Light #Agda #ITP
• The fundamental theorem of Asset Pricing, formalized in Lean 4. ~ Raphael Coelho. #LeanProver #ITP
• Formalization of 3-independence of simple tabulation hashing (in Isabelle/HOL). ~ Wei De Leong, Yong Kiam Tan, Seng Joe Watt. #IsabelleHOL #ITP
• Formalization of lower-bound certificates for optimal classical planning. ~ Dmitriy Traytel. #IsabelleHOL #ITP
• Greedy algorithms for cardinality-constrained submodular maximization. ~ Feier Lyu. #IsabelleHOL #ITP
• On the formalisation of Haag-Kastler nets in higher-order logic. ~ Richard H. J. Schmoetten. #IsabelleHOL #ITP
• Anti-unification completeness analysis in PVS. ~ Mauricio Ayala-Rincón et als. #PVS #ITP
• Formalization of the zigzag construction of path spaces of pushouts in homotopy type theory. ~ Vojtěch Štěpančík. #Agda #ITP #Math
• The educational proof assistant Waterproof in an introductory proof course: Proof construction and learning processes. ~ Pim Otte, Rogier Bos, Johan Commelin, Jim Portegies. #Waterproof #ITP #Teaching #Math
• Binomial coefficients with divisors avoiding an interval. ~ Hung M. Bui, Slava Naprienko, Kyle Pratt, Alexandru Zaharescu. #AI4Math
• Lean2Isabelle: Factorized cross-assistant proof translation. ~ Guanyu Liu, Jingkun Ma, Derek F. Wong. #AI4Math #LeanProver #IsabelleHOL #ITP
• Local reasoning models for mathematics (From installation, through concepts, to workflows with Ollama). ~ Paweł Przybyłowicz. #AI4Math
• The Ramanujan challenge for AI. ~ Gil Kalai. #AI4Math
• The jacobian challenge retro. ~ Rado Kirov. #AI4Math #LeanProver #ITP
• Haskell koan: Type-checked non-empty strings. ~ Mike Ledger. #Haskell #FunctionalProgramming
• #RetoLean4: Construcción en Lean 4 de las soluciones del reto 7 (La composición de inyectivas es inyectiva). #LeanProver #ITP #Math