The readings shared in Bluesky on 4 August 2025 are

• Cobblestone: Iterative automation for formal verification. ~ Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First. #ITP #CoqProver #AI #LLMs
• Reflections on Haskell@Meta. ~ Simon Marlow. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 3 August 2025 are

• AI at IMO 2025: a round-up. ~ Kevin Buzzard. #AI #LLMs #ITP #LeanProver #Math #IMO
• Formalization of harmonic analysis in Lean. ~ Wouter Bosse. #ITP #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (diciembre de 2017). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 2 August 2025 are

• Solving years-old math problems with Gemini 2.5 Deep Think. ~ Michel van Garrel. #LLMs #Math
• A formalization of multiplicative proof-nets in Rocq. ~ Rémi Di Guardia, Olivier Laurent. #ITP #Rocq
• Fixed-point-oriented programming: A concise and elegant paradigm. ~ Yong Qi Foo, Brian Sze-Kai Cheong, Michael D. Adams. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell (enero de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 1 August 2025 are

• Unconstrained optimization (in Isabelle/HOL). ~ Dustin Bryant. #ITP #IsabelleHOL #Math
• Seed-Prover: Deep and broad reasoning for automated theorem proving. ~ Luoxin Chen et als. #ITP #LeanProver #LLMs #Math
• NuminaMath-LEAN is a large-scale dataset of 100K mathematical competition problems formalized in Lean 4. #ITP #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (abril de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (marzo de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (febrero de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 31 July 2025 are

• The math is haunted. ~ Dan Abramov. #ProofAssistant #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell (julio de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2018). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 30 July 2025 are

• Universal pairs for diophantine equations (in Isabelle/HOL). ~ Marco David et als. #ITP #ProofAssistant #IsabelleHOL #Math
• #Exercitium: Problemas de programación con Haskell (mayo de 2022). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2022). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 29 July 2025 are

• Algorithmic conversion with surjective pairing: A syntactic and untyped approach. ~ Yiyun Liu, Stephanie Weirich. #FormalVerification #ProofAssistants #CoqProver
• Symbolic world models in Lean 4 for reinforcement learning. ~ Matěj Kripner. #ITP #LeanProver #MachineLearning
• Formal verification of the safegcd implementation. ~ Russell O'Connor, Andrew Poelstra. #FormalVerification #ProofAssistants #CoqProver
• Formal verification of pairing heaps in Rocq. ~ Cosmin-Ionut Visan. #FormalVerification #ProofAssistants #Rocq
• Verified functional graph algorithms using the Rocq prover (Coq). ~ Leopold Frieberger. #FormalVerification #ProofAssistants #Rocq
• Formal verification of leftist and skew heaps in Rocq. ~ Elena Marcela Dumitrache. #FormalVerification #ProofAssistants #Rocq
• Comparing codes: Spiral matrix (another matrix layer problem). ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Harmonic's IMO 2025 results (Harmonic's model Aristotle achieved gold medal performance, solving 5 problems). #FormalVerification #ProofAssistant #LeanProver #LLMs #Math #IMO
• #Exercitium: Problemas de programación con Haskell (noviembre de 2018). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (julio de 2022). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2022). #Haskell #ProgramaciónFuncional #Matemáticas

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.