The readings shared in Bluesky on 28 July 2025 are

• Gödel's first incompleteness theorem (in Lean4). #FormalVerification #ProofAssistant #LeanProver #Logic #Math
• Formalized formal logic (in Lean4). #FormalVerification #ProofAssistant #LeanProver #Logic #Math
• #Exercitium: Problemas de programación con Haskell (enero de 2019). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (diciembre de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 27 July 2025 are

• Formally verified suffix array construction (in Isabelle/HOL). ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. #FormalVerification #ProofAssistants #IsabelleHOL #Haskell #FunctionalProgramming
• McTT: A verified kernel for a proof assistant. ~ Junyoung Jang et als. #ProofAssistants #Rocq
• Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. #ProofAssistant #Agda
• Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. #FormalVerification #ProofAssistant #Agda
• A meta-modal logic for bisimulations (in Isabelle/HOL). ~ Alfredo Burrieza, Fernando Soler-Toscano, Antonio Yuste-Ginel. #ITP #IsabelleHOL
• Solving formal math problems by decomposition and iterative reflection. ~ Yichi Zhou et als. #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• Reseña de «Solving formal math problems by decomposition and iterative reflection». #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (febrero de 2019). #Haskell #ProgramaciónFuncional #Matemáticas

El artículo «Solving formal math problems by decomposition and iterative reflection» presenta Delta Prover, un nuevo sistema que resuelve problemas matemáticos complejos. Este agente utiliza un LLM que interactúa con el asistente de pruebas Lean 4. Mediante una descomposición de problemas y una reparación iterativa de las pruebas, el sistema aprende de los errores para construir demostraciones verificables. Alcanza un rendimiento del 95.9% de éxito en los problemas de miniF2F, superando a otros métodos sin necesitar un costoso reentrenamiento del modelo.

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