The readings shared in Bluesky on 9 May 2026 are:

• A shallow embedding of Datalog in Lean. ~ Ramy Shahin. #LeanProver #ITP
• Bennett's conjecture in Lean 4: Counter-models for the PSR-reducibility of Spinoza's propositions V and XIV. ~ Yuki Nakamura. #LeanProver #ITP
• Coherent rollout oracles for finite-horizon sequential decision problems. ~ Nishant Shukla. #LeanProver #ITP
• Global product intersection sets in semigroups. ~ Wouter van Doorn, Pietro Monticone, Quanyu Tang. #LeanProver #ITP #Math
• LeanDetective: a Lean Library that can assist with deductive reasoning in crime investigations such as murder mysteries. ~ Nilesh #LeanProver #ITP
• Mel Nathanson — How Harmonic's Aristotle solved some of my problems. #LeanProver #ITP #Aristotle #AI4Math
• Stokes' theorem for smooth singular cubes in Lean 4: True pullback, bridges to mathlib4, and chain-level d²=0. ~ David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz. #LeanProver #ITP #Math
• Aho-Corasick string matching (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP
• Certified qualitative analysis of the SIR ODE and reusable scalar lemmas in Isabelle/HOL. ~ David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz. #IsabelleHOL #ITP #Math
• Nash equilibria for finite games in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP
• The Banach–Tarski paradox in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Between Qed and truth (The permanent axiom trust boundary in machine-verified mathematics). ~ Ryan Christopher Fields. #CoqProver #ITP #Math
• Formal verification of Pohlig-Hellman algorithm for computing discrete logarithms with Coq. ~ Jeremiah Daniel A. Regalario et als. #CoqProver #ITP
• A general formalised framework for reasoning about display calculi. ~ Rajeev Goré, Anthony Peigné. #RocqProver #ITP #Logic
• Mizar: the first usable proof assistant for mathematics. ~ Lawrence Paulson. #Mizar #ATP #Math
• Categorical transformers. ~ Marco Perone. #Haskell #FunctionalProgramming
• Exception annotations: Lay of the Land. ~ Edsko de Vries. #Haskell #FunctionalProgramming
• MicroHs in the browser. ~ Lennart Augustsson. #Haskell #FunctionalProgramming
• Functional pearl: Binding boolean expressions and extended pattern matching. ~ Arthur Charguéraud, Yanni Lefki. #Ocaml #FunctionalProgramming
• A recent experience with ChatGPT 5.5 Pro. ~ Timothy Gowers. #AI4Math
• AI co-mathematician: Accelerating mathematicians with agentic AI. ~ Daniel Zheng et als. #AI4Math
• Verifier-backed hard problem generation for mathematical reasoning. ~ Yuhang Lai, Jiazhan Feng, Yee Whye Teh, Ning Miao. #AI4Math
• ‘Like space aliens landing’: Symposium weighs effect of AI on the future of mathematics. ~ Angikar Ghosal. #AI4Math
• Counting beyond the mind: The abacus and the origins of calculation. ~ Matthew A. McIntosh. #Math #CompSci
• Logarithms and slide rules: How calculation accelerated human reasoning. ~ Matthew A. McIntosh. #Math #History
• Reseña de «'Like space aliens landing': Symposium weighs effect of AI on the future of mathematics». #AI4Math
• Reseña de «AI co-mathematician: Accelerating mathematicians with agentic AI». #AI4Math
• Reseña de «Timothy Gowers: A recent experience with ChatGPT 5.5 Pro». #AI4Math