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⁻¹(f(s)) ⊆ 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

The readings shared in Bluesky on 2 April 2025 are

• Basic probability in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Mathlib #Math
• GOL in GOL in HOL: Verified circuits in Conway's game of life. ~ Magnus O. Myreen, Mario Carneiro. #ITP #HOL4
• Unfolding trees breadth-first in Haskell. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• Faking ADTs and GADTs in languages that shouldn't have them. ~ Justin Lê. #Haskell #FunctionalProgramming
• Proof or bluff? Evaluating LLMs on 2025 USA math olympiad. ~ Ivo Petrov et als. #LLMs #Math
• TAUT2 (Here you will find various types of randomly-generated, self-correcting logic excercises). #Logic
• Logica (Tools for thought). #Logic
• Curso de programación lógica. ~ Ana Pradera. #Lógica #ProgramaciónLógica #Prolog
• Enseñanza del sistema de deducción natural en lógica proposicional aplicando programación lógica. ~ Joaquín Arias, Iván Ramírez. #Lógica #ProgramaciónLógica #Prolog
• Apuntes de lógica: desde Aristóteles hasta Prolog. ~ Joaquín Arias. #Lógica #ProgramaciónLógica #Prolog
• #Exercitium: Mayor producto de las ramas de un árbol. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i))". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso: Demostración asistida por ordenador (2010-11). #ITP #IsabelleHOL #Lógica

The readings shared in Bluesky on 1 April 2025 are

• A small Prolog on the Z3 AST. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
• STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. #AI #LLMs #ITP #LeanProver
• The disconnect between AI benchmarks and math research (Evaluating AI systems on their ability to be a mathematical copilot). ~ Ralph Furman. #AI #LLMs #Math
• The cultural divide between mathematics and AI (A reflection on cultural differences observed at the 2025 Joint Mathematics Meeting). ~ Ralph Furman. #AI #LLMs #Math
• #Exercitium: Número de pares de elementos adyacentes iguales en una matriz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s)". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Razonamiento automático (2010-11)". #ITP #IsabelleHOL #Logic #Math
• Deducción natural en lógica proposicional con Isabelle/HOL. #Lógica #IsabelleHOL
• Deducción natural en lógica de primer orden con Isabelle/HOL. #Lógica #IsabelleHOL
• Introducción a la demostración asistida por ordenador con Isabelle/HOL (versión de 7 de agosto de 2010). #ITP #IsabelleHOL

The readings shared in Bluesky on 31 March 2025 are

• Formally verifying a transformation from MLTL formulas to regular expressions. ~ Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. #ITP #IsabelleHOL
• #Exercitium: Elemento más repetido de manera consecutiva. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "Los primos mayores que 2 son impares". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2010-11)". #Logic #Math #CompSci
• Temas de "Lógica informática" (2010-11). #Logic #Math #CompSci
• Ejercicios de "Lógica informática" (2010-11). #Logic #Math #CompSci
• Ejercicios de deducción natural proposicional. #Logic #Math
• Ejercicios de deducción natural en lógica de primer orden. #Logic #Math