The readings shared in Bluesky on 26 July 2025 are

• Higher order logic. ~ Mark Jago. #Logic
• My Emacs writing experience. ~ Sacha Chua. #Emacs #Org
• Finding the shape of my thoughts. ~ Sacha Chua. #Emacs #Org
• Writing experience: My decade with Org. ~ Álvaro Ramírez. #Emacs #OrgMode
• #Exercitium: Problemas de programación con Haskell (junio de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (marzo de 2019). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 25 July 2025 are

• A formalization of elementary linear algebra: Part I. ~ David Russinoff. #ITP #ACL2 #Math
• A formalization of elementary linear algebra: Part II. ~ David Russinoff. #ITP #ACL2 #Math
• A proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. #ITP #ACL2 #Math
• RV32I in ACL2. ~ Carl Kwan. #ITP #ACL2
• Extended abstract: Partial-encapsulate and its support for floating-point operations in ACL2. ~ Matt Kaufmann, J Strother Moore. #ITP #ACL2
• Lean FRO and Mathlib receive $10M from XTX Markets founder Alex Gerko to further advance the use of AI for mathematical research. #AI4Math #ITP #LeanProver #Math
• A Liquid Haskell kick-start. ~ Xavier Góngora. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de diciembre de 2019. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell de noviembre de 2019. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 24 July 2025 are

• Formally verifying automata for trusted decision procedures. ~ Zhaobo (Aeacus) Sheng. #ITP #LeanProver
• Competitive programming in Haskell: sparse tables. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Four ways of declaring interfaces in Haskell. ~ Marco Perone. #FunctionalProgramming #haskell
• Inlining in the Glasgow Haskell Compiler: empirical investigation and improvement. ~ Celeste Hollenbeck. #Haskell #FunctionalProgramming
• Type-level programming for safer resource management. ~ Fraser Tweedale. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 47: Pure parallelism. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• DeepMind and OpenAI achieve IMO Gold. What does it all mean? (What we know, what we would like to know, and what it may take years to know). ~ Ernest Davis, Gary Marcus. #AI #Math #LLMs
• #Exercitium: Problemas de programación con Haskell de enero de 2020. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 23 July 2025 are

• Seed-Prover: Reasoning wide and deep for automated math theorem proving. #AI #Math #LLMs #ITP #LeanProver
• Seed-Prover achieves IMO 2025 silver score. #AI #Math #LLMs #ITP #LeanProver
• #Exercitium: Problemas de programación con Haskell de febrero de 2020. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 22 July 2025 are

• A parametricity-based formalization of semi-simplicial and semi-cubical sets. ~ Hugo Herbelin, Ramkumar Ramachandra. #ITP #Rocq
• Comparing codes: Image rotation (Mutable arrays in Haskell). ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad. #LLMs #Math #IMO

The readings shared in Bluesky on 21 July 2025 are

• Representability and formalization of (distributive quasi) relation algebras. ~ Peter Jipsen. #ITP #LeanProver #IsabelleHOL #Rocq #Math
• #Exercitium: Problemas de programación con Haskell de abril de 2020. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell de marzo de 2020. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 18 July 2025 are

• Teaching software specification (Experience report). ~ Cameron Moy, Daniel Patterson. #CompSci #Teaching #ITP #LeanProver #ACL2
• CSLib: An open-source Lean 4 library formalizing a significant subsetof undergraduate-level computer science. ~ Clark Barrett et als. #ITP #LeanProver #CompSci
• Quantifiers for differentiable logics in Rocq (Extended abstract). ~ Jairo Miguel Marulanda-Giraldo et als. #ITP #Rocq
• Comparing codes: Binary search in a 2D matrix. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Leanabell-Prover-V2: Verifier-integrated reasoning for formal theorem proving via reinforcement learning. ~ Xingguang Ji et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 18 July 2025 are

• Formalization of derived categories in Lean/Mathlib. ~ Joël Riou. #ITP #LeanProver #Math
• A formalised approach to the composition of processes over linear resources. ~ Filip Smola. #ITP #IsabelleHOL
• Gödel's incompleteness theorems (in Isabelle/HOL). ~ Lawrence C. Paulson, with Janis Bailitis. #ITP #IsabelleHOL #Logic #Math
• Robust dynamic embedding for gradual typing. ~ Koen Jacobs et als. #ITP #Rocq
• Lean meets theoretical computer science: Scalable synthesis of theorem proving challenges in formal-informal pairs. ~ Terry Jingchen Zhang et als. #LLMs #ITP #LeanProver
• LeanTree: Accelerating white-box proof search with factorized states in Lean 4. ~ Matěj Kripner, Michal Sustr, Milan Straka. #LLMs #ITP #LeanProver
• Prover Agent: An agent-based framework for formal mathematical proofs. ~ Kaito Baba et als. #LLMs #ITP #LeanProver
• Scaling mathematical reasoning through data, tools, and generative selection. ~ Ivan Moshkov et als. #LLMs #ITP #LeanProver #Math
• ProofWala: Multilingual proof data synthesis and theorem-proving. ~ Amitayush Thakur et als. #ITP #LeanProver #CoqProver
• CLEVER: A curated benchmark for formally verified code generation. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver
• Lean Finder: Semantic search for Mathlib that understands user intents. ~ Jialin Lu et als. #ITP #LeanProver #Mathlib
• VeriBench: End-to-end formal verification benchmark for AI code generation in Lean 4. ~ Brando Miranda et als. #LLMs #ITP #LeanProver
• The Open Proof Corpus: A large-scale study of LLM-generated mathematical proofs. ~ Jasper Dekoninck et als. #LLMs #Math #Reasoning
• Proof or bluff? Evaluating LLMs on 2025 USA Math Olympiad. ~ Ivo Petrov et als. #LLMs #Math #Reasoning
• RealMath: A continuous benchmark for evaluating language models on research-level mathematics. ~ Jie Zhang et als. #LLMs #Math #Reasoning
• The calculated typer (Functional Pearl). ~ Zac Garby, Patrick Bahr, Graham Hutton. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de junio de 2020. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de mayo de 2020. #Haskell #FunctionalProgramming #Math

The readings shared in Bluesky on 17 July 2025 are

• Teaching mathematics with Lean: Interactive theorem provers in the classroom. ~ Paola Iannone, Gihan Marasingha, Athina Thoma. #ITP #LeanProver #Math
• Duality theory in linear optimization and its extensions (formally verified). ~ Martin Dvorak, Vladimir Kolmogorov. #ITP #LeanProver #Math
• Scott's representation theorem and the univalent Karoubi envelope. ~ Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens. #ITP #Rocq
• #Exercitium: Problemas de programación con Haskell de enero de 2021. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 16 July 2025 are

• Formalization of derived categories in Lean/Mathlib. ~ Joël Riou. #ITP #LeanProver #Math
• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• A complete formalization of Fermat’s Last Theorem for regular primes in Lean. ~ Alex J. Best et als. #ITP #LeanProver #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• A simple formalization of alpha-equivalence. ~ Kalmer Apinis, Danel Ahman. #ITP #Rocq
• Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. #ITP #CoqProver
• LISA: A modern proof system. ~ Simon Guilloud, Sankalp Gambhir, Viktor Kunčak. #ITP #Lisa #Math
• #Exercitium: Problemas de programación con Haskell de febrero de 2021. #Haskell #FunctionalProgramming