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

The readings shared in Bluesky on 9 May 2025 are

• Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord and Julien Narboux. #ATP #ITP #IsabelleHOL #LeanProver #Coq #Rocq #Education
• Maths with Coq in L1, a pedagogical experiment. ~ Marie Kerjean, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Logic #Math #Teaching
• Teaching divisibility and binomials with Coq. ~ Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Math #Teaching
• A graphical interface for category theory proofs in Coq. ~ Luc Chabassier. #ITP #Coq #Rocq #CategoryTheory
• OnlineProver: Experience with a visualisation tool for teaching formal proofs. ~ Ján Perháč et als. #ITP #Logic #Teaching
• Minimal sequent calculus for teaching first-order logic: Lessons learned. ~ Jørgen Villadsen. #ITP #IsabelleHOL #Logic #Teaching
• ProofBuddy (How it started, how it's going). ~ Nadine Karsten, Kim Jana Eiken, Uwe Nestmann. #ITP #IsabelleHOL #Logic #Teaching
• Lean4 machine assisted proof framework for chip firing game & graphical Riemann-Roch. ~ Dhyey Dharmendrakumar Mavani. #ITP #LeanProver
• Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. #ITP #Coq #Rocq
• Analyzing API design via algebraic laws. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Beginnings of a Haskell game engine. ~ Mitchell Vitez. #Haskell #FunctionalProgramming
• Scrap your iteration combinators. ~ Tom Ellis. #Haskell #FunctionalProgramming
• From Haskell to a new structured combinator processor. ~ Yukang Xie et als. #Haskell #FunctionalProgramming
• Lógicas de orden superior y verificación formal. ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
• Lógicas de orden superior y verificación formal (Slides). ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq

The readings shared in Bluesky on 8 May 2025 are

• SAT-solving the poset cover problem. ~ Chih-Cheng Rex Yuan, Bow-Yaw Wang. #ATP #SAT_solvers #Z3
• FormalMATH: Benchmarking formal mathematical reasoning of large language models. ~ Zhouliang Yu et als. #LLMs #Autoformalization #Math #ITP #LeanProver
• Beyond theorem proving: Formulation, framework and benchmark for formal problem-solving. ~ Qi Liu et als. #LLMs #ITP #LeanProver
• The Haskell Unfolder Episode 43: Monomorphism restriction and defaulting. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• What is programming?… and what is programming in the age of artificial intelligence? ~ Sebastian Nicolajsen, Claus Brabrand. #Programming

The readings shared in Bluesky on 6 May 2025 are

• Sophie Germain’s theorem (in Isabelle/HOL). ~ Benoît Ballenghien. #ITP #IsabelleHOL #Math
• Recamán’s sequence. ~ John D. Cook. #Math #Python
• 25 useful tips for Emacs (for beginners and advanced users). Raoul Comninos. #Emacs

The readings shared in Bluesky on 5 May 2025 are

• Compiling Haskell into Lean: A common abstract syntax for Haskell and interactive theorem provers. ~ Talitha Holcombe. #Haskell #FunctionalProgramming #ITP #LeanProver
• Avaliando a habilidade do ChatGPT de realizar provas de dedução natural em lógica proposicional e lógica de predicados. ~ Francisco Leonardo Batista Martins et als. #LLLms #ChatGPT #Logic
• Typed Lisp, a primer. ~ Musa Al-hassy (2019). #CommonLisp #Haskell

The readings shared in Bluesky on 4 May 2025 are

• Formalizing resource ownership semantics of spinlocks with the Coq proof assistant. ~ Sebastian Luis S. Ortiz et als. #ITP #Coq #Rocq
• Formalizing reversible computations for synchronous dataflow languages with infinite lists. ~ Sosuke Moriguchi et als. #ITP #Coq #Rocq
• Formal verification of blockchain nonforking in DAG-based BFT consensus with dynamic stake. ~ Alessandro Coglio, Eric McCarthy. #ITP #ACL2
• The minimal megaparsec tutorial. ~ Clément Hurlin. #Haskell #FunctionalProgramming
• Mathematician solves algebra's oldest problem using intriguing new number sequences. ~ University of New South Wales. #Math
• A hyper-Catalan series solution to polynomial equations, and the Geode. ~ N.J. Wildberger, Dean Rubine. #Math
• Entrevista a Jeffrey Ullman (ACM Turing Award). ~ Camilo Chacón Sartori. #Computación

The readings shared in Bluesky on 2 May 2025 are

• A proof of concept tool to verify estimates. ~ Terence Tao. #Math #AI #LLMs #ChatGPT #Python
• Advancing mathematics by guiding human intuition with AI. ~ Alex Davies et als. (2021). #Math #AI
• Semantics of probabilistic programs using s-finite kernels in dependent type theory. ~ Reynald Affeldt, Cyril Cohen, Ayumu Saito. #ITP #Rocq
• DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL #LLMs
• Frontier of formal theorem proving with large language models: Insights from the DeepSeek-Prover. ~ Huajian Xin. #ITP #LeanProver #LLMs #DeepSeek
• Automated theorem provers as the hub of the AI math ecosystem. ~ Stephan Schulz. #Math #AI #ITP

The readings shared in Bluesky on 1 May 2025 are

• DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. ~ Z.Z. Ren et als. #LLMs #ITP #LeanProver
• Mathematical beauty, truth and proof in the age of AI. ~ Jordana Cepelewicz. #Math #AI #ITP
• Logical modelling in CS education: Bridging the natural language gap. ~ Tristan Kneisel, Fabian Vehlken, Thomas Zeume. #Logic #Education
• Iltis: An interactive, web-based system for teaching formal foundations of computer science. #Logic #Education
• Introduction to Iltis: An interactive, web-based system for teaching logic. ~ Gaetano Geck et als. (2018). #Logic #Teaching
• Iltis: Learning Logic in the Web. ~ Gaetano Geck et als. (2022). #Logic #Teaching
• Clear: A formal verification framework for smart contracts in Lean. ~ Julian Sutherland. #ITP #LeanProver