The readings shared in Bluesky on 5 June 2026 are:

• A formal proof of the Ramanujan-Nagell theorem in Lean 4. ~ Barinder S. Banwait. #LeanProver #ITP #AI4Math
• Certificate-based verification of derivation-graph structural properties in Lean 4/Mathlib. ~ Megan Simons, Jonathan Washburn. #LeanProver #ITP
• Formal verification of the S-two AIR. ~ Jeremy Avigad, Anat Ganor, Lior Goldberg, David Levit, Ohad Nir, Yoav Seginer, Alon Titelman. #LeanProver #ITP
• From Itô to Black-scholes: A machine-verified derivation in Lean 4. ~ #LeanProver #ITP
• Keep the proof state live: snapshotting for efficient tactic search in Lean 4. ~ Austin Shen, Yunong Shi. #LeanProver #ITP
• Lean Pool: a repo for preserving substantial sorry-free formalizations that are valuable but do not fit naturally into mathlib’s scope. ~ Vasily Ilin et als. #LeanProver
• Positive quasimodular forms and linear programming bounds. ~ Seewoo Lee. #LeanProver #ITP #Math
• We can't agree to disagree, formally: Aumann's theorem and assumption accounting in Lean. ~ Ruize Chen, Ben Eltschig, Scott Duke Kominers, Ken Ono, Jujian Zhang. #LeanProver #ITP
• Abduction prover in Isabelle/HOL. ~ Yutaka Nagashima, Daniel Sebastian Goc. #IsabelleHOL #ITP
• Apply2Isar: Automatically converting Isabelle/HOL apply-style proofs to structured Isar. ~ Sage Binder, Hanna Lachnitt, Katherine Kosaian. #IsabelleHOL #ITP
• IsabelleBlueprint: a new project-layer tool for Isabelle/HOL formalizations, inspired by Lean Blueprint but built specifically for Isabelle. ~ Arthur. #IsabelleHOL #ITP
• The Busy Beaver function (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP
• The Gelfand–Naimark–Segal construction (in Isabelle/HOL). ~ Richard Schmoetten, Jacques D. Fleuriot. #IsabelleHOL #ITP #Math
• Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. #CoqProver #ITP
• A brief guide to autoformalization in mathematical physics. ~ James Squires. #AI4Math #LeanProver #Autoformalization
• A new declaration warns AI could threaten the foundations of mathematics. ~ Gayoung Lee. #AI4Math
• Auto formalisation of Goedel's second incompleteness theorem in binary recursive arithmetic. ~ Thierry Coquand. #AI4Math #Agda #ITP #Logic #Math
• Frontiers of AI for mathematical research. ~ Carina Hong. #AI4Math #LeanProver #ITP
• Just type it in Isabelle! AI agents drafting, mechanizing, and generalizing from human hints. ~ Kevin Kappelmann, Maximilian Schäffeler, Lukas Stevens, Mohammad Abdulaziz, Andrei Popescu, Dmitriy Traytel. #AI4Math #IsabelleHOL #ITP
• Lean-GAP: A dataset of formalized graduate algebra problems. ~ Seewoo Lee et als. #AI4Math #Autoformalization #LeanProver #ITP
• Leiden declaration on artificial intelligence and mathematics. #AI4Math
• Mathematicians issue Leiden Declaration on AI proof rules. ~ Marcus Schuler. #AI4Math
• Mathematicians say 'don't believe hype' on AI capabilities. ~ Andrew Zinin. #AI4Math
• Mathematicians warn of AI threats to profession as industry encroaches. ~ Jeremy Hsu. #AI4Math
• Proof-Refactor: Refactoring generated formal proofs into modular artifacts. ~ Yiming Fu, Peixuan Liu, Zichen Wang, Kun Yuan. #AI4Math #LeanProver #ITP
• Automatic formal verification for code generation. ~ Patrick Hillmann, Boris Hanin. #FormalVerification
• Practical uses of monads in Haskell. ~ Antoine Leblanc. #Haskell #FunctionalProgramming
• A computational toolkit for engagement and scalable assessment in a large Logic course. ~ Stephen M. Watt. #Logic #RacketLang
• #Calculemus: Demostraciones con Lean 4 de "Si a converge a L, entonces (∃ N)(∀ n ≥ N)[aₙ ≥ L - 1]". #LeanProver #Math
• #Calculemus: Demostraciones con Lean 4 de "Si aₙ converge a L y bₙ a M, entonces aₙ+bₙ converge a L+M". #LeanProver #Math
• #RetoLean4: Demostrar con Lean 4 que existen infinitos números primos. #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 3 (Si aₙ converge a L, entonces 2aₙ converge a 2L). #LeanProver #ITP #Math