Readings shared January 4, 2026
The readings shared in Bluesky on 4 January 2026 are:
- Terry Tao on the future of mathematics. #AI #Math #ITP #LeanProver
- Seemingly impossible programs in Lean. ~ Joachim Breitner. #ITP #LeanProver
- Pursuit of truth and beauty in Lean 4 (Formally verified theory of grammars, optimization, matroids). ~ Martin Dvořák. #ITP #LeanProver
- Computing and formalizing residuated lattices and relation algebras. ~ Peter Jipsen. #ITP #LeanProver
- cLean: A verified domain-specific language for GPU kernel programming in Lean 4. ~ Riyaz Ahuja. #ITP #LeanProver
- Lecture Notes: Computational mathematics and AI (A ten-lecture workshop series). ~ Lars Ruthotto. #AI #Math
- An introduction to proofs and the mathematical vernacular. ~ Martin Day. #Math
- Open textbook initiative (The American Institute of Mathematics (AIM)). #Math
- Open textbook library: Mathematics textbooks. #Math
- Emacs Lisp Elements: EPUB and PDF versions now available. ~ Protesilaos Stavrou. #Emacs #Lisp