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