The readings shared in Bluesky on 14 July 2025 are

• Exploiting instantiations from paramodulation proofs in Isabelle/HOL. ~ Lukas Bartl, Jasmin Blanchette, Tobias Nipkow. #ITP #IsabelleHOL
• Quantifying bounded rationality: Formal verification of Simon's satisficing through flexible stochastic dominance. ~ Jingyuan Li, Zhou Lin. #ITP #LeanProver
• Could we teach ∞-category theory to undergraduates or to a computer? ~ Emily Riehl. #ITP #LeanProver #Math
• Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. #ITP #Coq
• Towards solving more challenging IMO problems via decoupled reasoning and proving- ~ Zhenwen Liang et als. #LLMs #ITP #LeanProver #Math