Readings shared July 18, 2025
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