Readings shared January 19, 2026
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