The readings shared in Bluesky on 17 March 2025 are

• The calculated typer. ~ Zac Garby, Patrick Bahr, Graham Hutton. #Haskell #FunctionalProgramming
• #Exercitium: Primos equidistantes. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema del barbero. #IsabelleHOL #Lógica

The readings shared in Bluesky on 16 March 2025 are

• Permutations with no consecutive elements. ~ John D. Cook. #Math #Python #Programming
• #Exercitium: Anagramas. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 15 March 2025 are

• Revisiting an early critique of formal verification. ~ Lawrence Paulson. #ITP #Math #FormalVerification
• A proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. #ITP #ACL2 #Math
• Principles of rule-based programming. ~ Thom Frühwirth. #CHR #Constraint #LogicProgramming
• Mathematics for inference and machine learning. ~ Marc Deisenroth, Stefanos Zafeiriou. #Math #MachineLearning
• Introducción a la Introducción de Emacs. ~ Notxor. #Emacs
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema de los infectados. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2006-07)". #LogicProgramming #Prolog #AI #NLP #Constraints #Logic
• Curso "Lógica informática (2007-08)". #Lógica #Matemática #Computación

The readings shared in Bluesky on 14 March 2025 are

• La théorie des types, de Russell aux assistans à la demostration. ~ Thierry Coquand. #TypeTheory #ITP #Logic #Math
• Local look-ahead guidance via verifier-in-the-loop for automated theorem proving. ~ Sara Rajaee, Kumar Pratik, Gabriele Cesa, Arash Behboodi. #LLMs #LeanProver
• Algebra, topology, differential calculus, and optimization theory for computer science and machine learning. ~ Jean Gallier, Jocelyn Quaintance. #Math #CompSci #MachineLearning
• Las matemáticas son, sobre todo, hermosas. ~ Marta Macho-Stadler. #Matemáticas
• #Exercitium: Mastermind. #Haskell #FunctionalProgramming
• #Calculemus: La dama o el tigre. #IsabelleHOL #Lógica
• Curso "Razonamiento automático (2005-06)". #ATP #Otter #Mace #ITP #PVS
• Curso "Lógica informática (2006-07)". #Logic #Math #CompSci

The readings shared in Bluesky on 13 March 2025 are

• Course notes for "Formalising Mathematics 2025". ~ Bhavik Mehta et als. #ITP #LeanProver #Math
• LeanAgent: Lifelong learning for formal theorem proving. ~ Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, Anima Anandkumar. #LLMs #ITP #LeanProver #Math
• The Haskell Unfolder Episode 40: Understanding through a model. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Determinación de los elementos minimales. #Haskell #FunctionalProgramming #Math
• #Calculemus: El problema lógico del mal. #ITP #IsabelleHOL #Lógica
• Curso "Lógica informática (2005-06)". #Logic #Math #CompSci
• Curso "Programación declarativa (2005-06)". #LogicProgramming #Prolog

The readings shared in Bluesky on 12 March 2025 are

• A formal proof of the irrationality of ζ(3) in Lean 4. ~ Junqi Liu, Jujian Zhang, Lihong Zhi. #ITP #LeanProver #Math
• #Exercitium: La bandera tricolor. #Haskell
• #Calculemus: Teorema de Nicómaco. #IsabelleHOL #Lógica #Matemática
• Curso "Demostración automática de teoremas (2004-05)". #ATP #Otter #Mace #Logic #Math
• Curso "Programación lógica (2004-05)". #LogicProgramming #Prolog #AI #NLP #Constraints #MachineLearning
• Curso "Razonamiento automático (2004-05)". #ATP #Otter #Mace #Jape #Logic #ITP #PVS

The readings shared in Bluesky on 11 March 2025 are

• Extrinsic termination proofs for well-founded recursion in Lean. ~ Joachim Breitner. #ITP #LeanProver
• Knuth Bendix solver on Z3 AST. ~ Philip Zucker. #SMT #Z3
• Books on the history of mathematics, some thoughts. ~ Thony Christie. #Math
• LLMs can find mathematical reasoning mistakes by pedagogical chain-of-thought. ~ Zhuoxuan Jiang et als. #LLMs #Math
• Can proof assistants verify multi-agent systems? ~ Julian Alfredo Mendez, Timotheus Kampik. #MAS #FormalVerification #LeanProver #Scala
• DeepSeek vs. ChatGPT vs. Claude: A comparative study for scientific computing and scientific machine learning tasks. ~ Qile Jiang, Zhiwei Gao, George Em Karniadakis. #LLMs #Math
• Why do researchers care about small language models? ~ Stephen Ornes. #LLMs #SMLs
• Navigating between points with registers. ~ Daniel Liden. #Emacs
• #Exercitium: Ordenación por el máximo. #Haskell
• #Calculemus: Reto f(f(f(b))) = f(b). #IsabelleHOL #Lógica #Matemática
• Curso "Demostración automática de teoremas (2002-03)". #ATP #Otter #Mace #Logic #Math
• Curso "Programación lógica (2003-04)". #LogicProgramming #Prolog #AI
• Curso "Razonamiento automático (2003-04)". #ATP #Otter #Mace #ITP #Jape #PVS
• Curso "Lógica informática (2004-05)". #Logic #Math
• Curso "Programación declarativa (2004-05)". #LogicProgramming #Prolog

The readings shared in Bluesky on 10 March 2025 are

• The burden of proof: Automated tooling for rapid iteration on large mechanised proofs. ~ Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, John Wickerson. #ITP #IsabelleHOL
• MiniF2F in Rocq: Automatic translation between proof assistants (a case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesúss Gallego Arias, Marc Lelarge. #LLMs #Rocq #LeanProver #IsabelleHOL #Math
• Generating millions of Lean theorems with proofs by exploring state transition graphs. ~ David Yin, Jing Gao. #LLMs #LeanProver #Math
• New proofs expand the limits of what cannot be known (By proving a broader version of Hilbert’s famous 10th problem, two groups of mathematicians have expanded the realm of mathematical unknowability). ~ Joseph Howlett. #Math
• Les sept problèmes mathématiques du prix du millénaire. ~ Nicolas Bacaër et als. #Math
• How to get a Common Lisp job in 2055. ~ Sebastian Carlos. #CommonLisp
• #Exercitium: Iguales al siguiente. #Haskell
• #Calculemus: Celebración del día mundial de la lógica. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2003-04)" #LogicProgramming #Prolog

The readings shared in Bluesky on 9 March 2025 are

• Floating point numbers in Lean. ~ Joseph McKinsey. #ITP #LeanProver #Math
• Flean: Floating point numbers in Lean, mostly done! ~ Joseph McKinsey. #ITP #LeanProver #Math
• Curso "Lógica informática" (2003-04). #Logic #Math #CompSci

The readings shared in Bluesky on 8 March 2025 are

• Sum types and subtypes and unions. ~ Justin Le. #Haskell #FunctionalProgramming