The readings shared in Bluesky on 5 February 2025 are

• On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. #ITP #LeanProver #Mathlib
• Goedel-Prover: A new frontier in automated theorem proving. ~ Yong Lin et als. #LLMs #ITP #LeanProver
• New proofs probe the limits of mathematical truth. ~ Joseph Howlett. #Math