The readings shared in Bluesky on 01 October 2025 are:

• A PVS library on the infinitude of primes. ~ Bruno Berto de Oliveira Ribeiro, Mariano M. Moscato, Thaynara Arielly de Lima, Mauricio Ayala-Rincón. #ITP #PVS #Math
• An introduction to formal real analysis (Lecture 7: Uniqueness and advanced limit theorems). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Agentic Lean Auformalization (ALA): An LLM collaborative approach to autoformalization in LEAN. ~ Patricio Gallardo, Maziar Raissi, Ke Zhang, Sudhir Murthy. #Autoformalization #ITP #LeanProver #LLMs
• Hilbert: Recursively building formal proofs with informal reasoning. ~ Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, Ke Ye. #AI #Math #LLMs #ITP #LeanProver
• Formalizing Mason-Stothers theorem and its corollaries in Lean 4. ~ Jineon Baek, Seewoo Lee. #ITP #LeanProver #Math
• Nominal sets in Rocq. ~ Fabrício Sanches Paranhos, Daniel Ventura. #ITP #Rocq #Math
• Category theory illustrated: Natural transformations. ~ Jencel Panic. #CategoryTheory