Readings shared May 4, 2026
The readings shared in Bluesky on 4 May 2026 are:
- Compfiles: Catalog of math problems formalized in Lean. ~ David Renshaw et als. #LeanProver #ITP #Math
- Primitive pythagorean triples in lean and reduction modulo odd prime powers. ~ Luke Biddle. #LeanProver #Math
- Sobre la demostración del Problema #1196 de Erdős por GPT-5.4 Pro. ~ Francisco R. Villatoro. #LeanProver #AI4Math
- Nagata factoriality (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
- The algebra of iterative constructions (in Isabelle/HOL). ~ Kevin Batz, Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat, Todd Schmid. #IsabelleHOL #ITP
- Delooping generated groups in homotopy type theory. ~ Camil Champin, Samuel Mimram, Emile Oleon. #Agda #ITP #HoTT
- A monadic implementation of functional logic programs. ~ Michael Hanus, Kai-Oliver Prott, Finn Teegen. #Haskell #FunctionalProgramming
- Arboretum.hs: Symbolic manipulation for algebras of graphs. ~ Eugen Bronasco, Jean-Luc Falcone, Gilles Vilmart. #Haskell #FunctionalProgramming
- Why I still reach for Scheme and Lisp instead of Haskell. ~ Josep Bigorra. #Haskell #Scheme #Lisp #FunctionalProgramming
- Collatz conjecture in Prolog. ~ Markus Triska. #Prolog #LogicProgramming
- CKKS — Polynomials, the canonical embedding, and encoding. ~ Jeremy Kun. #Python #Programming #Math
- MathDuels: a self-play benchmark for mathematical reasoning. ~ Rabdos. #AI4Math
- MathDuels: Evaluating LLMs as problem posers and solvers. ~ Zhiqiu Xu, Shibo Jin, Shreya Arya, Mayur Naik. #AI4Math