The readings shared in Bluesky on 14 February 2026 are:

• Formalization of the Golay-Hopf machine: A unified algebraic framework for Hida, Iwasawa, and Yang-Baxter structures. ~ Yoshihiro Hasegawa. #ITP #LeanProver
• Learning Lean (part 1). ~ Rado Kirov. #ITP #LeanProver #Math
• Leaning on AI. ~ Rado Kirov. #LeanProver #ITP #AI4Math
• Learning Lean (part 2). ~ Rado Kirov. #ITP #LeanProver #Math
• Learning Lean (part 3). ~ Rado Kirov. #ITP #LeanProver #Math
• Learning Lean (part 4). ~ Rado Kirov. #ITP #LeanProver #Math
• Machine assistance and the future of research mathematics. ~ Terence Tao. #AI4Math #ITP #LeanProver
• PBLean: Pseudo-boolean proof certificates for Lean 4. ~ Stefan Szeider. #ITP #LeanProver
• Why formalize mathematics - more than catching errors. ~ Rado Kirov. #ITP #LeanProver #Math
• RustCompCert: A verified and verifying compiler for a sequential subset of Rust. ~ Jinhua Wu, Yuting Wang, Liukun Yu, Linglong Meng. #ITP #CoqProver #RustLang
• Generalized decidability via Brouwer trees. ~ Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh, Fredrik Nordvall Forsberg. #Agda #ITP
• Verified program extraction in number theory: The fundamental theorem of arithmetic and relatives. ~ Franziskus Wiesnet. #Minlog #Haskell #FunctionalProgramming
• LISP, Prolog and evolution. ~ Sami Badawi. #FunctionalProgramming #Lisp #Prolog #Haskell #Clojure
• Hilbert's program and infinity. ~ Richard Zach. #Logic #Math
• Accelerating mathematical and scientific discovery with Gemini Deep Think. ~ Thang Luong and Vahab Mirrokni. #AI4Math
• Accelerating scientific research with Gemini: Case studies and common techniques. ~ David P. Woodruff et als. #AI4Math
• LLMs for math research. ~ Dmitry Rybin. #AI4Math #ITP #LeanProver
• To be a frog with wings, should you choose (Recent progress on AI for mathematics and how to get involved). ~ Kevin Barreto. #AI4Math #ITP #LeanProver
• Towards autonomous mathematics research. ~ Tony Feng et als. #AI4Math