The readings shared in Bluesky on 19 July 2026 are:

• Building Shor's algorithm in Lean: An agentic formalization of quantum attacks on RSA-2048 and P-256. ~ Lei Zhang, Yusheng Zhao, Hongshun Yao, Xin Wang. #LeanProver #ITP
• Cantor measures with odd base do not admit Fourier frames. ~ Jaume de Dios Pont, Lukas Liehr, Mitchell A. Taylor. #LeanProver #ITP #Math
• Formalizing abstract simplicial complexes & stellar subdivisions in Lean. ~ Garett Cunningham, Daniel Zach, Stefan Friedl. #LeanProver #ITP #Math
• Interchange graphs of (0,1)-matrices are maximally Hamiltonian. ~ Jeffrey S. Baggett, Huiya Yan. #LeanProver #ITP
• Mathematicians put AI to work on Fermat's last theorem. ~ Matthew Sparkes. #LeanProver #AI4Math
• Minimum modulus for the unique multiset-sum problem. ~ José A. R. Fonollosa. #LeanProver #ITP
• Representing Lean proofs: Tactics, trajectories, search. ~ Elisaveta Samoylov. #LeanProver #ITP
• Anti-unification completeness analysis in PVS. ~ Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Temur Kutsia, Marcos Mercandeli-Rodrigues. #PVS #ITP
• Formalizing hyperspaces and operations on subsets of polish spaces over abstract exact real numbers. ~ Michal Konečný, Sewon Park, Holger Thies. #CoqProver #ITP #Math
• Verification of a DPLL transition system in Rocq. ~ Julia Dijkstra, Benedikt Ahrens. #RocqProver #ITP
• Conway's circle theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• First-order modal logic in HOL: Deep and shallow embeddings with automated faithfulness. ~ Christoph Benzmüller, Daniel Kirchner. #IsabelleHOL #ITP #Logic
• Formalizing paradoxes in grounded arithmetic using Isabelle/HOL. ~ Ananthajit Srikanth, Bryan Ford. #IsabelleHOL #ITP #Math
• Monadic second-order logic in HOL: Deep and shallow embeddings with automated faithfulness (Isabelle/HOL dataset). ~ Christoph Benzmüller, Daniel Kirchner. #IsabelleHOL #ITP #Logic
• New and formalized proofs for right-forward closures and core matrix interpretations. ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. #IsabelleHOL #ITP
• Polynomial commitment schemes (in Isabelle/HOL). ~ Tobias Rothmann. #IsabelleHOL #ITP
• Termination restricted to right-forward closures (in Isabelle/HOL). ~ René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, Johannes Waldmann. #IsabelleHOL #ITP
• The Chevalley-Warning theorem (in Isabelle/HOL). ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• A formalization of the mean-field derivation of the Vlasov equation: AI-assisted Lean formalization as a strategy game. ~ Joseph K. Miller. #AI4Math #LeanProver
• AIMO interpretability challenge. ~ Michal Štefánik et als. #AI4Math
• From solvers to research: Large language model-driven formal mathematics at the research frontier. ~ Eric Jiang, Xiao Liang, Yikai Zhang, Yingjia Wan, Mengting Li, Haikang Deng, Alexander K. Taylor, Justin Baker, Rushil Raghavan, Junyi Zhang, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei Wang. #AI4Math
• OpenProver: Agentic and interactive theorem proving with Lean 4. ~ Matěj Kripner, Milan Straka. #AI4Math #LeanProver
• The Ramanujan challenge for AI. ~ Michael Shalyt, Rotem Kalisch, Carsten Schneider, Hila Barkan, Elyasheev Leibtag, John Campbell, Shachar Weinbaum, Tali Monderer, Ashvni Narayanan, Ido Kaminer. #AI4Math
• Enterprise Haskell at H-E-B. ~ Joshua Miller. #Haskell #FunctionalProgramming
• GHC String interpolation. ~ Brandon Chinn. #Haskell #FunctionalProgramming
• Is there a future for a formally specified Haskell report?. ~ David Binder. #Haskell #FunctionalProgramming #LeanProver #ITP
• Stable Haskell. ~ Julian Ospald. #Haskell #FunctionalProgramming
• #RetoLean4: Enunciado del reto 10 (Si una sucesión converge a un límite no nulo, entonces sus términos están eventualmente acotados inferiormente por la mitad del valor absoluto del límite). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 9 (Unicidad del límite). #LeanProver #ITP #Math
• #Retolean4: Vídeo tutorial sobre cómo resolver el reto 9. #LeanProver #ITP #Math