The readings shared in Bluesky on 14 June 2026 are:

• A formally verified library of mathematical finance in Lean 4. ~ Raphael Coelho. #LeanProver #ITP
• A kernel-clean lean mechanization of Classical Lottery in Action and the Wakker-Debreu-Koopmans representation layer. ~ Jingyuan Li, Ilia Tsetlin, Fan Wang. #LeanProver #ITP
• An automated proof that R(B₈, B₁₀) = 37. ~ Jeremy Kalfus, Bernard Lidický. #LeanProver #ITP #Math
• Complex analysis in PNT+ and real analysis as a game. ~ Alex Kontorovich. #LeanProver #ITP #Math
• Formal foundations and proof-carrying certificates for q-ary covering codes in Lean 4. ~ Andreas Florath. #LeanProver #ITP
• Formalizing Schwartz functions and tempered distributions. ~ Moritz Doll. #LeanProver #ITP #Math
• Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4. ~ Arnaud Mayeux, Jujian Zhang. #LeanProver #ITP #Math
• HoTTLean: Formalizing the groupoid model of MLTT. ~ Steve Awodey, Mario Carneiro, Sina Hazratpour, Joseph Hua, Wojciech Nawrocki, Spencer Woolfson, Yiming Xu. #LeanProver #ITP
• The continuous functional calculus in Lean. ~ Anatole Dedecker, Jireh Loreaux. #LeanProver #ITP #Math
• A reusable Isabelle/HOL framework for propositional labelled natural deduction. ~ Arthur Freitas Ramos 📧, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP
• EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation. ~ Dominic Mulligan, Nathan Chong. #IsabelleHOL #ITP.
• Euler's exponential series as an infinite polynomial (in Isabelle/HOL). ~ Jacques D. Fleuriot. #IsabelleHOL #ITP #Math
• Fair games theorem (in Isabelle/HOL). ~ Lawrence C. Paulson. #IsabelleHOL #ITP #Math
• Feuerbach's theorem (in Isabelle/HOL). ~ Lawrence C. Paulson. #IsabelleHOL #ITP #Math
• Formalization and implementation of algebraic methods in geometry. ~ Filip Marić, Ivan Petrović, Danijela Petrović, Predrag Janičić. #IsabelleHOL #ITP #Math
• Isabelle/PIDE as platform for educational tools. ~ Makarius Wenzel, Burkhart Wolff. #IsabelleHOL #ITP
• Mechanized metasemantics of modal necessity: Valuation factorization and modal non-collapse. ~ Yong-Dock Kim. #IsabelleHOL #ITP
• Vosper's theorem and the Cauchy–Davenport theorem via the polynomial method. ~ Arthur Freitas Ramos , David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• A proof in Coq that core logic is not paraconsistent. ~ Joseph Vidal-Rosset. #CoqProver #ITP
• Extraction and search in Rocq: Theorems, definitions and their dependencies. ~ Jian Fang, Yingfei Xiong. #RocqProver #ITP
• Auto formalisation of Chaitin and of the surprise incompleteness theorem. ~ Thierry Coquand. #Agda #ITP #AI4Math
• A golden age of maths is dawning and mathematicians are freaking out. ~ Alex Wilkins. #AI4Math
• A problem of Andrews and Dhar on partitions. ~ Simon Mahns, Ken Ono, Jujian Zhang. #AI4Math #AxiomProver #LeanProver #ITP
• AI scores a ‘C–’ on its hardest math test yet. ~ Joseph Howlett. #AI4Math
• Artificial intelligence for mathematical reasoning: an integrated survey of language models, neuro-symbolic systems, and verified discovery. ~ Syed Rifat Raiyan, Mohsinul Kabir, Hasan Mahmud, Md Kamrul Hasan. #AI4Math
• DeepMind’s new AI found a strange new way to think. ~ Károly Zsolnai-Fehér. #AI4Math #LeanProver #ITP
• How Terry Tao became an evangelist for AI in math. ~ Kevin Hartnett. #AI4Math #LeanProver #ITP
• Les mathématiciens se positionnent face à l’IA. ~ François Lassagne. #AI4Math
• Pythagoras-Prover: Advancing efficient formal proving via augmented Lean formalisation. ~ Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia. #AI4Math #LeanProver #ITP
• Solving a chess puzzle with Claude and Prolog. ~ John D. Cook. #Prolog #LogicProgramming #LLMs
• eyelang: a small rule engine for Prolog-style Horn clauses over ordinary terms, lists, arithmetic, strings, and finite search. ~ Jos De Roo. #LogicProgramming