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