The readings shared in Bluesky on 12 June 2025 are

• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• Lean meta-theory: The proofs behind the proofs. ~ Mario Carneiro. #ITP #LeanProver
• Litex: Scale formal reasoning in AI age. ~ Jiachen Shen. #Logic #ATP #LitexLang
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #ITP #LeanProver #LLMs
• Can large language models verify system software? A case study using FSCQ as a benchmark. ~ Jianxing Qin et als. #LLMs #ITP #CoqProver #Rocq
• Reinventing records and variants. ~ Murat Kasimov. #Haskell #FunctionalProgramming