The readings shared in Bluesky on 18 October 2025 are:

• An introduction to formal real analysis (Lecture 12: Cauchy sequences II). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Pushdown automata (in Isabelle/HOL). ~ Kaan Taskin, Tobias Nipkow. #ITP #IsabelleHOL
• An effective method for solving a class of transcendental diophantine equations. ~ Zeyu Cai. #ITP #LeanProver #Math
• Functional reasoning for distributed systems with failures. ~ Haobin Ni, Robbert van Renesse, Greg Morrisett. #ITP #Rocq
• Ax-Prover: A deep reasoning agentic framework for theorem proving in mathematics and quantum physics. ~ Marco Del Tredici et als. #AI #Math #LLMs #ITP #LeanProver
• GAR: Generative adversarial reinforcement learning for formal theorem proving. Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang. #AI #Math #LLMs #ITP #LeanProver
• Mathematics with large language models as provers and verifiers. ~ Hieu Le Duc, Leo Liberti. #AI #Math #LLMs #ITP #LeanProver