Readings shared February 14, 2026
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