The readings shared in Bluesky on 24 November 2025 are:

• An introduction to formal real analysis (Lecture 21: Functions and derivatives). ~ Alex Kontorovich. #ITP #LeanProver #Math
• A perspective on interactive theorem provers in Physics. ~ Joseph Tooby-Smith. #ITP #LeanProver #Physics
• ITP 2025 Lean workshop. #ITP #LeanProver
• Gödel mirror: A paraconsistent calculus mechanized in Lean 4. ~ Jhet Chan. #ITP #LeanProver #Logic #Math
• Automatic geometry theorem proving using polynomial elaboration. ~ Mauricio Barba da Costa et als. #ITP #LeanProver #Math
• A topological rewriting of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. #ITP #CoqProver
• A Coq-based axiomatization of Tarski's mereogeometry. ~ Patrick Barlatier, Richard Dapoigny. #ITP #CoqProver
• Set theory with types. ~ Lawrence Paulson. #Logic #Math #CompSci #SetTheory #TypeTheory
• A new bridge links the strange math of infinity to computer science. ~ Joseph Howlett. #Math #CompSci
• Tableau methodology for propositional logics. ~ T. Jarmuzek, R. Gore. #Logic