The readings shared in Bluesky on 31 May 2025 are

• Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. ~ Viviana del Barco et als. #ITP #LeanProver #Math
• Lean4Lean: Mechanizing the metatheory of Lean. ~ Mario Carneiro. #ITP #LeanProver
• HoTTLean: Formalizing the meta-theory of HoTT in Lean. ~ Joseph Hua et als. #ITP #LeanProver #HoTT
• Towards modular composition of inductive types using Lean meta-programming. ~ Ramy Shahin. #ITP #LeanProver
• Löb’s theorem and provability predicates in Rocq. ~ Janis Bailitis1, Dominik Kirst, Yannick Forster. #ITP #Rocq #Logic #Math
• A Coq formalization of Lagois connections for secure information flow. ~ Casper Stahl et als. #ITP #Coq #Rocq
• Verifying Z3 RUP proofs with the interactive theorem provers Coq/Rocq and Agda. ~ Harry Bryant et als. #ITP #Coq #Rocq #Agda
• Efficient program extraction in elementary number theory using the proof assistant Minlog. ~ Franziskus Wiesnet. #ITP #Minlog #Haskell #FunctionalProgramming #Math

The readings shared in Bluesky on 30 May 2025 are

• Certified algorithms for numerical semigroups in Rocq. ~ Massimo Bartoletti, Stefano Bonzio, Marco Ferrara. #ITP #Rocq #Math
• Agent-based logics in dependent type theory. ~ Colm Baston. #ITP #Agda
• RocqStar: Leveraging similarity-driven retrieval and agentic systems for Rocq generation. ~ Nikita Khramov, Andrei Kozyrev, Gleb Solovev, Anton Podkopaev. #ITP #Rocq #GenerativeAI
• VERINA: Benchmarking verifiable code generation. ~ Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, Dawn Song. #AIforCode #ITP #LeanProver

The readings shared in Bluesky on 29 May 2025 are

• Geometric reasoning in Lean: from algebraic structures to presheaves. ~ Kenji Maillard, Yiming Xu. #ITP #LeanProver #Math
• Construire des preuves mathématiques. ~ Thierry Coquand, William Rowe-Pirra. #ITP #Coq
• Formalizing colimits in Cat. ~ Mario Carneiro, Emily Riehl. #ITP #LeanProver
• A collection of formalized statements of conjectures in Lean, using Mathlib. #ITP #LeanProver #Math
• A formal analysis of algorithms for matroids and greedoids. ~ Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa. #ITP #IsabelleHOL
• Kimina: Interactive mathematical proof assistant. #AI #ITP #LeanProver #Math
• Context-free grammars and languages (in Isabelle/HOL). ~ Tobias Nipkow et als. #ITP #IsabelleHOL
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, Axel Ljungström. #ITP #Agda
• Mechanized safety of Jolteon consensus in Agda. ~ Orestis Melkonian, Mauro Jaskelioff, and James Chapman. #ITP #Agda
• Implementing Löb’s theorem in Emacs Lisp. ~ John Wiegley. #Emacs #Lisp #Logic #Math

The readings shared in Bluesky on 28 May 2025 are

• Formalizing Fermat: an update. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Algebraic geometry in Mathlib. ~ Andrew Yang. #ITP #LeanProver #Math
• REAL-Prover: Retrieval augmented Lean prover for mathematical reasoning. ~ Ziju Shen et als. #AI #TheoremProving #LeanProver #Math
• Faithful logic embeddings in HOL (Deep and shallow). ~ Christoph Benzmüller. #ITP #TheoremProving #IsabelleHOL #Logic #Math

The readings shared in Bluesky on 27 May 2025 are

• Formalizing a classification theorem for low-dimensional solvable Lie algebras in Lean. ~ Viviana del Barco, Gustavo Infanti, Exequiel Rivas, Paul Schwahn. #ITP #LeanProver #Math
• Simprocs for the working mathematician. ~ Yaël Dillies Paul Lezeau. #ITP #LeanProver
• Proof assistants and type theory. ~ Judah Towery. #ITP #LeanProver #Math
• A foundationally verified intermediate verification language. ~ Joshua M. Cohen. #ITP #CoqProver #Wyh3
• The way of code (The timeless art of Vibe Coding). ~ Rick Rubin. #Programming #Tao

The readings shared in Bluesky on 25 May 2025 are

• Shallow expressions (in Isabelle/HOL). ~ Simon Foster. #ITP #IsabelleHOL
• Orgro: A mobile Org Mode file editor and viewer. #OrgMode

The readings shared in Bluesky on 24 May 2025 are

• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Munta: A verified model checker for timed automata (in Isabelle/HOL). ~ Simon Wimmer. #ITP #IsabelleHOL
• Learning Physics with functional programming and Haskell. ~ Esteban Marín. #Haskell #FunctionalProgramming #Physics
• Is AI making coders obsolete? (Are there problems with having AI tools take over coding from humans?). ~ Jennifer Goforth Gregory. #AIforCode

The readings shared in Bluesky on 23 May 2025 are

• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Solving guarded domain equations in presheaves over ordinals and mechanizing it. ~ Sergei Stepanenko, Amin Timany. #ITP #RocqProver #CategoryTheory
• Ineq-Comp: Benchmarking human-intuitive compositional reasoning in automated theorem proving on inequalities. ~ Haoyu Zhao et als. #LLMs #ITP #LeanProver #Math
• CLEVER: A curated benchmark for formally verified code generation. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver #AIforCode
• Formalisation of fairness notions in assignment problem. ~ Duc Minh Do. #ITP #IsabelleHOL

The readings shared in Bluesky on 22 May 2025 are

• A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. #ITP #ACL2 #Math
• Lean-auto: An interface between Lean 4 and automated theorem provers. ~ Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad. #ITP #LeanProver
• Lean-SMT: An SMT tactic for discharging proof goals in Lean. ~ Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark Barrett. #ITP #LeanProver
• The roots of Lisp. ~ Paul Graham (2002). #Lisp #Programming
• Las raíces de Lisp. ~ Paul Graham (2002). #Lisp #Programming
• LISP, el "lenguaje de DIOS". ~ LinuxChad. #Lisp #Programming

The readings shared in Bluesky on 21 May 2025 are

• Will computers prove theorems? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formalizing the future: Lean’s impact on mathematics, programming, and AI. ~ Leo De Moura. #ITP #LeanProver #Math #CompSci #AI
• A formalization of the correctness of the Floodsub protocol. ~ Ankit Kumar, Panagiotis Manolios. #ITP #ACL2
• OpenEvolve: Open-source implementation of AlphaEvolve. ~ Asankhaya Sharma. #AI #LLMs #AlphaEvolve #Math
• AlphaEvolveVerify: Verification of Google DeepMind's AlphaEvolve 48-multiplication matrix algorithm. ~ Deming Xu. #Python #Programming #Math
• Toward safe, flexible, and efficient software in Common Lisp. ~ Robert Smith. #CommonLisp
• Theorems and conjectures with Python. ~ Alessio Drivet. #Math #Python #Programming
• Analysis of selection noise in genetic algorithms. Nataliya M. Gulayeva, Joaquín Borrego-Díaz, Fernando Sancho-Caparrini. #GeneticAlgoritm
• org-expex: Expex glosses in Org-mode (Emacs org-mode extension to auto-create linguistic glosses). ~ David Diem. #Emacs #OrgMode