The readings shared in Bluesky on 14 April 2026 are:

• A formal proof of the Ramanujan-Nagell theorem in Lean 4. ~ Barinder S. Banwait. #LeanProver #ITP #AI4Math
• Formalization of De Giorgi-Nash-Moser theory in Lean. ~Scott Armstrong, Julia Kempe. #LeanProver #ITP #Math
• Formalizing building-up constructions of self-dual codes through isotropic lines in Lean. ~ Jae-Hyun Baek, Jon-Lark Kim. #LeanProver #ITP #Math
• From painfully explicit to implicit in Lean. ~ Rado Kirov. #LeanProver #ITP #FunctionalProgramming
• Kripke And Beth semantics in Lean. ~ Callan McGill. #LeanProver #ITP #Logic
• The Lean programming language and theorem prover. ~ Leo de Moura. #LeanProver #ITP #FunctionalProgramming
• Using the Lean 4 proof assistant to teach mathematics for engineers. ~ Peter Junglas. #LeanProver #ITP #Math #AI4Math
• VeriSoftBench: Repository-scale formal verification benchmarks for Lean. ~ Yutong Xin, Qiaochu Chen, Greg Durrett, Işil Dillig. #LeanProver #AI4Math
• Lean 4 (meta)programming cookbook. ~ Anirudh Gupta et als. #LeanProver #ITP #FunctionalProgramming
• AI and Isabelle: Experiences and perspectives. ~ Lawrence Paulson. #IsabelleHOL #ITP #AI4Math
• Munkres' general topology autoformalized in Isabelle/HOL. ~ Dustin Bryant, Jonathan Julián Huerta y Munive, Cezary Kaliszyk, Josef Urban. #IsabelleHOL #ITP #AI4Math #Autoformalization
• CARVe in Rocq: A library for substructural meta-theory. ~ Daniel Zackon et als. #RocqProver #ITP
• Lectures on AI for mathematics. ~ Xiaoyang Chen, Xiaoyang Chen. #AI4Math
• The AI revolution in math has arrived. ~ Konstantin Kakaes. #AI4Math
• The agentic researcher: A practical guide to AI-assisted research in mathematics and machine learning. ~ Max Zimmer, Nico Pelleriti, Christophe Roux, Sebastian Pokutta. #AI4Math
• A simple switch makes code differentiable. ~ Dan Piponi (sigfpe). #Haskell #FunctionalProgramming
• Howl (Haskell Open Wolfram Language interpreter); an implementation of a microscopic subset of the Wolfram Language (which powers Mathematica), in Haskell. ~ David Simmons-Duffin. #Haskell #FunctionalProgramming
• Type-level programming is still programming. ~ Michael Chavinda. #Haskell #FunctionalProgramming
• Education for logical thinking in the age of AI. ~ Robert Kowalski. #Logic #LogicProgramming
• Demostraciones con Lean 4 de "La sucesión aₙ = 1/n converge a 0". #LeanProver #Math
• Reseña de «AI and Isabelle: Experiences and perspectives». #AI4Math #IsabelleHOL #ITP
• Reseña de «Education for logical thinking in the age of AI». #Logic #LogicProgramming #Prolog
• Reseña de «Lectures on AI for mathematics». #AI4Math
• Reseña de «The AI revolution in math has arrived». #AI4Math
• Reseña de «The agentic researcher: A practical guide to AI-assisted research in mathematics and machine learning». #AI4Math
• Reseña de «Munkres' general topology autoformalized in Isabelle/HOL». #IsabelleHOL #ITP #AI4Math