Readings shared November 24, 2025
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