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

The readings shared in Bluesky on 17 May 2025 are

• Formalizing the future: Lean’s impact on mathematics, programming, and AI. ~ Leo De Moura. #ITP #LeanProver #Math #CompSci #AI
• Will computers prove theorems? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Recursive definitions in Lean. ~ Joachim Breitner. #ITP #LeanProver #FunctionalProgramming
• Digitalizing Wick's theorem. ~ Joseph Tooby-Smith. #ITP #LeanProver
• The Haskell Unfolder Episode 44: State-based testing with quickcheck-lockstep. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 16 May 2025 are

• AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms. ~ AlphaEvolve team. #AI #LLMs #AlphaEvolve #Math
• AlphaEvolve: A coding agent for scientific and algorithmic discovery. ~ AlphaEvolve team. #AI #LLMs #AlphaEvolve #Math
• The collapse of GPT (Will future artificial intelligence systems perform increasingly poorly due to AI-generated material in their training data?). ~ Neil Savage. #AI #GPT
• La última IA de Google promete ser capaz de mejorarse a sí misma. De momento, ya está superando a los matemáticos humanos. ~ Marcos Merino. #AI #LLMs #AlphaEvolve #Math

The readings shared in Bluesky on 15 May 2025 are

• Heftia: The final word in Haskell effect system libraries (Part 1.1). ~ Riyo. #Haskell #FunctionalProgramming
• Quasiquoting for fun, profit, expressions and patterns. ~ MLabs. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 14 May 2025 are

• Formal P-category theory and normalization by evaluation in Rocq. ~ David G. Berry, Marcelo P. Fiore. #ITP #Rocq #CategoryTheory
• Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. #ITP #Rocq #OCaml
• Theorem prover Arend. ~ Fedor Part, Valery Isaev, and Sergey Sinchuk. #ITP #Arend
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 13 May 2025 are

• Course: Functional programming and theorem proving in Lean 4. ~ Leni Aniva, Abdalrhman Mohamed. #ITP #LeanProver #FunctionalProgramming
• Formalizing a proof in Lean using Github copilot and canonical. ~ Terence Tao. #ITP #LeanProver #Math
• APOLLO: Automated LLM and Lean collaboration for advanced formal reasoning. ~ Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh. #LLMs #ITP #LeanProver
• La gran ilusión de la IA: no piensa, no siente, pero habla como si lo hiciera. ~ Ramón López de Mántaras. #IA

The readings shared in Bluesky on 10 May 2025 are

• A tool to verify estimates, II: a flexible proof assistant. ~Terence Tao. #ITP #Python #Math
• How to (actually) prove it - New frontiers of mathematics & computing in Lean. ~ Kiran. #ITP #LeanProver #Math
• LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. #ITP #LeanProver #Mathlib
• How do undergraduates do mathematics? (A guide to studying mathematics at Oxford University). #Math