Readings shared January 24, 2026
The readings shared in Bluesky on 24 January 2026 are:
- Abel's limit theorem (in Isabelle/HOL). ~ Kangfeng Ye. #ITP #IsabelleHOL #Math
- A formalization of the downward Löwenheim-Skolem theorem in Coq. ~ Timothée Huneau. #ITP #CoqProver #Logic #Math
- Formally verified number-theoretic transform. ~ Alix Trieu. #ITP #RocqProver
- The HOL-Light library of multivariate real analysis in Rocq. ~ Claudio Sacerdoti Coen, Abdelghani Alidra, Frédéric Blanqui. #ITP #RocqProver #HOL_Light #Math
- Blurred drinker paradoxes and blurred choice axioms: Constructive reverse mathematics of the downward Löwenheim-Skolem theorem. ~ Dominik Kirst, Haoyi Zeng. #ITP #CoqProver #Logic #Math
- Elementary proofs of ring commutativity theorems. ~ Michael Kinyon, Desmond MacHale. #ATP #Prover9 #Math
- Verified polynomial-time reductions in Lean 4: formalizing the complexity of decision-relevant information. ~ Tristan Simas. #ITP #LeanProver
- Sequencelib: A computational platform for formalizing the OEIS in Lean. ~ Walter Moreira, Joe Stubbs. #ITP #LeanProver #Math
- Sequencelib: A platform for formalizing OEIS sequences in Lean 4. ~ Walter Moreira, Joe Stubbs. #ITP #LeanProver #Math
- Numina-Lean-agent: An open and general agentic reasoning system for formal mathematics. ~ Junqi Liu et als. #ITP #LeanProver #Math
- ChatGPT and AI enhancing undergrad math. ~ Matthias Kawski. #AI #Math
- AI for mathematics: Progress, challenges, and prospects. ~ Haocheng Ju, Bin Dong. #AI #Math #AI4Math #ITP #IsabelleHOL #CoqProver #LeanProver
- Sobre la resolución de problemas de Erdős usando inteligencia artificial generativa. ~ Francisco R. Villatoro. #AI #Math #ITP #LeanProver