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

The readings shared in Bluesky on 20 May 2025 are

• Formalising the Bruhat-Tits tree. ~ Judith Ludwig, Christian Merten. #ITP #LeanProver
• Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #HoTT
• A Python frozenset interpretation of Dependent Type Theory. ~ Philip Zucker. #TypeTheory #Python #Logic
• Comparing code: LeetCode problems in Rust vs. Haskell. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Symbolic sets for proving bounds on Rado numbers. ~ Tanbir Ahmed, Lamina Zaman, Curtis Bright #SAT #Python #Math
• Formatting academic papers in Emacs Orgmode. ~ Kenneth Flak. #Emacs #OrgMode

The readings shared in Bluesky on 19 May 2025 are

• A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. #ITP #LeanProver #Math
• Towards a mechanization of fraud proof games in Lean. ~ Martín Ceresa, César Sánchez. #ITP #LeanProver
• Farey sequences and Ford circles (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Formal verification of a fail-safe cross-chain bridge. ~ Filip Marić, Bernhard Scholz, Pavle Subotić. #ITP #IsabelleHOL
• Verifying smart contract transformations using bisimulations. ~ Kegan McIlwaine, James Caldwell. #ITP #IsabelleHOL
• Formally specifying contract optimizations with bisimulations in Coq. ~ Derek Sorensen. #ITP #Coq #Rocq
• Math for programming (Learn the math, write better code). ~ Ronald T. Kneusel. #Math #Python #Programming
• Lisp. But why? ~ Raj. #CommonLisp #Programming

The readings shared in Bluesky on 18 May 2025 are

• Formalizing a proof in Lean using Claude and o4. ~ Terence Tao. #ITP #LeanProver #Math
• Formalizing a proof in Lean using Github Copilot only. ~ Terence Tao. #ITP #LeanProver #Math
• Formal proof of Dilworth’s theorem (in Isabelle/HOL). ~ Vivek Soorya Maadoori et als. #ITP #IsabelleHOL #Math
• Benchmarking energy calculations using formal proofs. ~ Ejike D. Ugwuanyi, Colin T. Jones, John Velkey, Tyler R. Josephson. #ITP #LeanProver
• Freer arrows and why you need them. ~ Grant Vandomelen, Yao Li. #Haskell #FunctionalProgramming
• Computer science and mathematics: A powerful synergy. ~ Khaled M.M. Alrantisi, Mohammad Imtiyaz Gulbarga. #Math #CompSci
• Tipos abstractos y polimorfismo en programación funcional. ~ Emanuel Goette. #Haskell #FunctionalProgramming