The readings shared in Bluesky on 19 January 2026 are:

• Broken proofs and broken provers. ~ Lawrence Paulson. #ITP #IsabelleHOL #RocqProver #LeanProver
• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #ITP #LeanProver #Math
• Formalization of amicable numbers theory. ~ Zhipeng Chen, Haolun Tang, Jingyi Zhan. #ITP #LeanProver
• Resolution of Erdős problem #728: a writeup of Aristotle's Lean proof. ~ Nat Sothanaphan. #AI #Math #LLMs #ITP #LeanProver
• Erdos Problems LLM Hunter (A collection of attempts by advanced Large Language Models (LLMs) to solve open mathematical problems from the Erdős Problems collection and MathOverflow). ~ Paata Ivanisvili. #AI #Math
• Logic programming with extensible types. ~ Ivan Perez, Angel Herranz. #Haskell #FunctionalProgramming #Prolog #LogicProgramming
• Some Haskell idioms we like. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Playing with Gödel’s incompleteness theorem in Prolog. ~ Kenichi Sasagawa. #Prolog #LogicProgramming #Logic
• Mathematics as natural science in the era of AI. ~ Siddhartha Gadgil. #Math #AI