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