Readings shared May 9, 2026
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 d2=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