The readings shared in Bluesky on 13 April 2025 are

• Completeness of decreasing diagrams for the least uncountable cardinality (in Isabelle/HOL). ~ Ievgen Ivanov. #ITP #IsabelleHOL #Math #SetTheory
• Efficient formal verification of quantum error correcting programs. ~ Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying. #ITP #Coq
• Mathematical reading list (University of Cambridge). #Math
• LLMs can't stop making up software dependencies and sabotaging everything. ~ Thomas Claburn. #AI #LLMs #Programming
• #Exercitium: Descomposiciones triangulares. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]". #LeanProver #IsabelleHOL #Math
• Curso "Razonamiento automático (2011-12)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 12 April 2025 are

• Evaluating AI's impact on Haskell open source development. ~ Matthew Pickering, Sam Derbyshire. #LLMs #Haskell #FunctionalProgramming
• #Exercitium: Índices de valores verdaderos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 11 April 2025 are

• Code generation via meta-programming in dependently typed proof assistants. ~ Mathis Bouverot-Dupuis, Yannick Forster. #ITP #Agda #Rocq #LeanProver
• A comparative review of ZFC, NBG, and MK axiom systems: Theoretical foundations and formalization in Coq. ~ Si Chen, Wensheng Yu. #ITP #Coq #Rocq #Math #SetTheory
• A (very niche) footgun in GHC.Generics. ~ welltypedwitch. #Haskell #FunctionalProgramming
• Refactoring strings in GHC. ~ Brandon Chinn. #Hakell #FunctionalProgramming
• #Exercitium: Código de las alergias. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[f⁻¹[u]​] ⊆ u". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 10 April 2025 are

• Canonical for automated theorem proving in Lean. ~ Chase Norman, Jeremy Avigad. #ITP #LeanProver #Math
• Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity (in Isabelle/HOL). ~ Filip Marić, Jelena Markovic. #ITP #IsabelleHOL
• Leanabell-prover: Posttraining scaling in formal reasoning. ~ Jingyuan Zhang et als. #LLMs #ITP #LeanProver
• Lemmanaid: Neuro-symbolic lemma conjecturing. ~ Yousef Alhessi et als. #LLMs #ITP #IsabelleHOL
• Reasoning about AI’s reasoning. ~ Höjer Key. #AI #LLMs #ITP #ATP
• Search index in 150 lines of Haskell. ~ kqr. #Haskell #FunctionalProgramming
• Distilling PEP 8 for teaching introductory programming. ~ Diana Kirk, Andrew Luxton-Reilly, Ewan Tempero. #Programming
• Why I program in Lisp. ~ Joe Marshall. #CommonLisp #FunctionalProgramming
• From blind solvers to logical thinkers: Benchmarking LLMs' logical integrity on faulty mathematical problems. ~ A M Muntasir Rahman et als. #LLMs #Math #Reasoning
• #Exercitium: Pim, Pam, Pum y divisibilidad. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 8 April 2025 are

• DMTL4: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. #ITP #LeanProver #Math
• Course Cs2120f24: Discrete mathematics and theory in Lean 4. ~ Kevin Sullivan. #ITP #LeanProver #Math
• Training making math proofs using Lean 4. ~ Krillof. #ITP #LeanProver #Math
• PEIRCE: Unifying material and formal reasoning via LLM-driven neuro-symbolic refinement. ~ Xin Quan, Marco Valentino, Danilo S. Carvalho, Dhairya Dalal, André Freitas. #AI #LLMs #ITP #IsabelleHOL #Prolog #LogicProgramming
• #Exercitium: Reiteración de una función. #Haskell #ProgramaciónFuncional #Matemáticas
• [#Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f⁻¹[fs ⊆ s"]]. #LeanProver #IsabelleHOL #Math

• Verified program extraction in number theory: The fundamental theorem of arithmetic and relatives. ~ Franziskus Wiesnet. #ITP #Minlog #Haskell #FunctionalProgramming #Math
• Central limit theorem in Lean. ~ Rémy Degenne. #ITP #LeanProver #Math
• Prime number theorem and more in Lean. ~ Alex Kontorovich. #ITP #LeanProver #Math
• Formalizing value distribution theory in Lean. ~ Stefan Kebekus. #ITP #LeanProver #Math
• Learn Lean 4 with PLFA (Programming Language Foundations in Agda) proofs. ~ rami3l. #ITP #LeanProver
• Chandra-Furst-Lipton (A digitisation of the number on the forehead model in Lean). ~ Yaël Dillies. #ITP #LeanProver #Math
• Toric varieties in Lean (Formalisation of toric varieties in Lean 4). ~ Yaël Dillies, Paul Lezeau, Patrick Luo, Michał Mrugała, Justus Springer, Andrew Yang. #ITP #LeanProver #Math
• Arithmetic progressions - almost periodicity (A digitisation of the Kelley-Meka bound on Roth numbers in Lean). ~ Thomas Bloom, Yaël Dillies. #ITP #LeanProver #Math
• Lecture notes for an introductory course in group theory. ~ Ben Selfridge. #ITP #LeanProver #Math
• Stronger SMT solvers for proof assistants (Proofs, quantifier simplification, strategy schedules). ~ Hans-Jörg Schurr. #ATP #SMT #ITP #IsabelleHOL
• An introduction to typeclass metaprogramming. ~ Alexis King. #Haskell #FunctionalProgramming
• meta_predicate declarations. ~ Markus Triska. #Prolog #LogicProgramming
• #Exercitium: Elementos de una matriz con algún vecino menor. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ⊆ u ↔ s ⊆ f⁻¹(u)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica matemática y fundamentos (2011-12)". #Lógica #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 6 April 2025 are

• Prolog vs LLMs: A complementary approach to AI (according to DeepSeek). #Prolog #LogicProgramming #LLMs #AI
• #Exercitium: Enumeración de árboles binarios. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ⊆ f⁻¹(f(s))". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2011-12)". #Lógica #ProgramaciónLógica #Prolog
• Temas de "Lógica informática" (curso 2011-12). #Lógica #ProgramaciónLógica #Prolog
• Ejercicios de "Lógica informática" (curso 2010-11). #Lógica

The readings shared in Bluesky on 5 April 2025 are

• Building AI for mathematical reasoning. ~ Chris Garcia. #Prolog #LogicProgramming #Logic #Math
• #Exercitium: Números triangulares con n cifras distintas. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "f(s ∪ t) = f(s) ∪ f(t)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 4 April 2025 are

• Learning Lean in the age of Artificial Intelligence. ~ Adolfo Neto. #ITP #LeanProver
• Guessing game: Haskell style. ~ kqr. #Haskell #FunctionalProgramming
• Function application needs to grow a spine already. ~ Thunderseethe. #Haskell #FunctionalProgramming
• Why you should maintain a personal LLM coding benchmark. ~ Edward Z. Yang. #LLMs #Programming
• #Exercitium: Trenzado de listas. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Informática (2011-12)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2011-12). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2011–12). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2011–12). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 3 April 2025 are

• Morley's theorem (in Isabelle/HOL). ~ Benjamin Puyobro. #ITP #IsabelleHOL #Math
• Category theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. #CategoryTheory #Math #Haskell #FunctionalProgramming
• LeanSolver: Solving theorems through large language models and search. ~ Avi Luciano Halevy #LLMs #ITP #LeanProver
• AlphaProof: when reinforcement learning meets formal mathematics. ~ Thomas Hubert. #AlphaProof #AI #Math
• #Exercitium: Biparticiones de una lista. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)". #LeanProver #IsabelleHOL #Math #Calculemus