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

The readings shared in Bluesky on 30 April 2025 are

• Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. #ITP #Coq #Rocq
• Verified hand-written Lean solutions to HumanEval. ~ Markus Himmel. #ITP #LeanProver

The readings shared in Bluesky on 29 April 2025 are

• Improving mathematical proving skills through interactive theorem proving. ~ Sana Stojanović Đurđević, Andrija Urošević, Filip Marić (2024). #ITP #IsabelleHOL #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math

The readings shared in Bluesky on 28 April 2025 are

• Tutte's theorem as an educational formalization project. ~ Pim Otte. #ITP #LeanProver #Math
• Haskelling my Python (Reimplementing Haskell lazy infinite lists using Python generators). ~ Unnamed Website. #Python #Haskell #FunctionalProgramming #Math
• Power series, power serious. ~ M. Douglas McIlroy (1998). #Haskell #FunctionalProgramming #Math
• Tree rewriting calculi for strictly positive logics. ~ Sofía Santiago-Fernández, David Fernández-Duque, Joost J. Joosten. #Logic

The readings shared in Bluesky on 27 April 2025 are

• Bitcoinolog: Reason about Bitcoin addresses with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Working with Common Lisp pathnames. ~ Nicolas Martyanoff. #CommonLisp
• AI for program verification. ~ Cristian Cadar, Abhik Roychoudhury. #AI #FormalVerification
• Introducing category theory (Version 26 Apr 2025). ~ Peter Smith. #CategoryTheory
• The levels of Emacs proficiency. ~ Vivek Haldar (2011). #Emacs

The readings shared in Bluesky on 25 April 2025 are

• Lean 4 formalization of the logic textbook "Logic Notes" by Lou van den Dries. ~ Will Bradley. #ITP #LeanProver #Logic #Math
• Neural theorem proving: Generating and structuring proofs for formal verification. ~ Balaji Rao, William Eiers, Carlo Lipizzi. #LLMs #ITP #IsabelleHOL
• Mathematical Logic (Math 570) Lecture Notes. ~ Lou van den Drie. #Logic #Math
• Implementing Unsure Calculator in 100 lines of Haskell. ~ Rodrigo Mesquita. #Haskell #FunctionalProgramming
• Integrating effectful and persistent. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Porting song recommendations to Haskell. ~ Mark Seemann. #Haskell #FunctionalProgramming
• Magical Haskell: A friendly approach to modern functional programming, type theory, and artificial intelligence. ~ Anton Antich. #Haskell #FunctionalProgramming #AI
• #Exercitium: Duplicación de cada elemento. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 24 April 2025 are

• On the averaging problem of ideal families related to Frankl's conjecture with formal proof by Lean 4. ~ Masahiro Hachimori, Kenji Kashiwabara. #ITP #LeanProver #Math
• #Exercitium: Sistema factorádico de numeración. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​". #LeanProver #IsabelleHOL #Math