The readings shared in Bluesky on 13 September 2025 are:

• Greibach normal form (in Isabelle/HOL). ~ Alexander Haberl, Tobias Nipkow, Akihisa Yamada. #ITP #IsabelleHOL
• Stratified datalog and program analysis (in Isabelle/HOL). ~ Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson. #ITP #IsabelleHOL

The readings shared in Bluesky on 12 September 2025 are

• Finiteness of symbolic derivatives in Lean. ~ Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner. #ITP #LeanProver #Math
• Modeling and proving in computational type theory using the Rocq prover. ~ Gert Smolka. #ITP #Rocq
• MPCTT textbook project (Modeling and proving in computational type theory using the Rocq prover). ~ Gert Smolka. #ITP #Rocq
• Introducing Gauss, an agent for autoformalization. #AI #Autoformalization #ITP #LeanProver #Math

The readings shared in Bluesky on 11 September 2025 are

• An introduction to Lean 4 (An introduction to formal verification). ~ Enric Cosme Llópez, Lü Gong. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 0: Introduction). ~ Filip Łajszczak. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 1: Defining sets and membership). ~ Filip Łajszczak. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 2: Subsets). ~ Filip Łajszczak. #ITP #LeanProver #Math
• Lean 4 with a Math Textbook (Part 3: Properties of subsets). ~ Filip Łajszczak. #ITP #LeanProver #Math
• A Lean 4 formalization of Pólya enumeration theorem. ~ Luka Opravš. #ITP #LeanProver #Math
• Haskell equations, thirty-eight years later. ~ Philip Wadler. #Haskell #FunctionalProgramming
• Better Haskell stack traces via user annotations. ~ Hannes Siebenhandl, Matthew Pickering. #Haskell #FunctionalProgramming
• Fraudulent publishing in the mathematical sciences. ~ Ilka Agricola, Lynn Heller, Wil Schilders, Moritz Schubotz, Peter Taylor, Luis Vega. #Math
• #Exercitium: Representación de Zeckendorf. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 10 September 2025 are

• An introduction to formal real analysis (Lecture 1: The story of real analysis. Lean tactics (exact, rfl, rewrite, ring_nf, use, intro, specialize, choose)). ~ Alex Kontorovich. #ITP #LeanProver #Math
• An introduction to formal real analysis (Lecture 2: Newton's computation of π. Formal definition of the limit of a sequence). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Real analysis, the game! ~ Alex Kontorovich. #ITP #LeanProver #Math
• Using Haskell in production. ~ Agentultra. #Haskell #FunctionalProgramming
• #Exercitium: Ventana deslizante. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 9 September 2025 are

• Higher order differential calculus in Mathlib. ~ Sébastien Gouëzel. #ITP #LeanProver #Math
• Ordinal exponentiation in homotopy type theory. ~ Tom de Jong et als. #ITP #Agda #HoTT #Math
• The story of mathematics. #Math
• La historia de las matemáticas: 35.000 años de números, año arriba, año abajo. ~ @Alvy. #Matemáticas
• #Exercitium: Renombramiento de un árbol. #Haskell #ProgramaciónFuncional
• #Exercitium: Divide si todos son múltiplos. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 8 September 2025 are

• Graph algorithms in board games! ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• #Exercitium: Empiezan con mayúscula. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 7 September 2025 are

Índice

• Course: Introduction to real analysis. ~ Alex Kontorovich. #Math #ITP #LeanProver
• Introduction to formal real analysis (Lecture 1). ~ Alex Kontorovich. #Math #ITP #LeanProver
• Introduction to formal real analysis (Lecture 2). ~ Alex Kontorovich. #Math #ITP #LeanProver
• #Exercitium: Límite de sucesiones. #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 6 September 2025 are

• An introduction to Lean 4. ~ E. Cosme Llópez, L. Gong. #ITP #LeanProver #FunctionalProgramming
• The gap between commercial and open-source LLMs for Olympiad-level math is shrinking. #AI #LLMs #Math

The readings shared in Bluesky on 5 September 2025 are

• Program verification is not all-or-nothing. ~ Lawrence Paulson. #FormalVerification
• The future of math is programming. ~ Ank Yog. #ITP #LeanProver #Math
• AI-driven formal theorem proving. #ITP #LeanProver #AI #LLMs
• Better Haskell stack traces via user annotations. ~ Hannes Siebenhandl, Matthew Pickering. #Haskell #FunctionalProgramming
• What is the Fourier transform?. ~ Shalma Wegsman. #Math
• #Exercitium: Intercalación de n copias. #Haskell #ProgramaciónFuncional
• #Exercitium: Eliminación de n elementos. #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 4 September 2025 are

• F91 in Lean. ~ Joachim Breitner. #ITP #LeanProver
• Lean: First steps. ~ Tariq Rashid. #ITP #LeanProver
• Acorn and the future of (AI?) theorem proving. ~ Guillermo Angeris. #ITP #LeanProver
• Lemmanaid: Neuro-symbolic lemma conjecturing. ~ Yousef Alhessi et als. #ITP #IsabelleHOL #LLMs
• Distributors (Unifying parsers, printers & grammars). ~ Eitan Chatav. #Haskell #FunctionalProgramming
• La red social de org-mode. ~ Notxor. #Emacs #OrgMode
• #Exercitium: N gramas. #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Sopa de letras. #Haskell #ProgramaciónFuncional #Matemáticas