The readings shared in Bluesky on 15 July 2025 are

• Using Lean like an external SMT solver from Python. ~ Philip Zucker. #ITP #LeanProver
• IMO 1996 P3: Lean 4 formalization. ~ David Renshaw. #ITP #LeanProver #Math
• #Exercitium: Problemas de programación con Haskell de junio de 2021. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de mayo de 2021. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de abril de 2021. #Haskell #FunctionalProgramming
• #Exercitium: Problemas de programación con Haskell de marzo de 2021. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 14 July 2025 are

• Exploiting instantiations from paramodulation proofs in Isabelle/HOL. ~ Lukas Bartl, Jasmin Blanchette, Tobias Nipkow. #ITP #IsabelleHOL
• Quantifying bounded rationality: Formal verification of Simon's satisficing through flexible stochastic dominance. ~ Jingyuan Li, Zhou Lin. #ITP #LeanProver
• Could we teach ∞-category theory to undergraduates or to a computer? ~ Emily Riehl. #ITP #LeanProver #Math
• Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. #ITP #Coq
• Towards solving more challenging IMO problems via decoupled reasoning and proving- ~ Zhenwen Liang et als. #LLMs #ITP #LeanProver #Math

The readings shared in Bluesky on 13 July 2025 are

• Formalizing quasi-categories in Lean. ~ Jack McKoen. #ITP #LeanProver
• A simple AI chatbot (ChatGPT clone) built entirely in Haskell. ~ Tushar Adhatrao. #Haskell #FunctionalProgramming #LLMs

The readings shared in Bluesky on 12 July 2025 are

• A formalization of divided powers in Lean. ~ Antoine Chambert-Loir, María Inés de Frutos-Fernández. #ITP #LeanProver #Math
• Completeness of the decreasing diagrams method for proving confluence of rewriting systems of the least uncountable cardinality. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. #ITP #CoqProver
• Marginal subsemigroups and commutators in inverse semigroups. ~ Gonçalo Araújo, João Araújo, Michael Kinyon #ATP #Prover9 #Math
• Proof theory and logic programming: Computation as proof search. ~ Dale Miller. #Logic #ProofTheory #LogicProgramming
• Teaching logic programming: a review. ~ Serhiy O. Semerikov et als. #LogicProgramming #Prolog #ASP #CLP
• Categorical semantics in Haskell. ~ Mohamed Amine Ayari. #Haskell #FunctionalProgramming #CategoryTheory
• Generic second-order matching, higher-order preunification and pattern unification - Implementations in Haskell. ~ Nikolai Kudasov et als. #Haskell #FunctionalProgramming
• CriticLean: Critic-guided reinforcement learning for mathematical formalization. ~ Zhongyuan Peng et als. #LLMs #ITP #LeanProver #Math
• ¿Por qué los usuarios de Emacs lo usan para todo? ~ Andros Fenollosa (2023). #Emacs

The readings shared in Bluesky on 11 July 2025 are

• Kimina-Prover: Applying test-time RL search on large formal reasoning models. ~ Haiming Wang et als. #LLMs #ITP #LeanProver
• AI for mathematical discovery (symbolic, neural and neuro-symbolic methods). ~ Moa Johansson. #AI #Math
• Cursos impartidos con materiales completos: apuntes, ejercicios y exámenes resueltos. #Lógica #ProgramaciónLógica #ProgramaciónFuncional #IA #RazonamientoAutomático

The readings shared in Bluesky on 10 July 2025 are

• The Haskell Unfolder Episode 46: Developing an application from scratch. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Curso "Razonamiento automático (2019-20)". #DemostraciónInteractiva #ProgramaciónFuncional #IsabelleHOL

The readings shared in Bluesky on 9 July 2025 are

• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math
• Doing Lean dirty: Lean as a Jupyter notebook replacement. ~ Philip Zucker. #ITP #LeanProver
• Robust, end-to-end correctness proofs of industrial divide and square root RTL designs. ~ Sol Swords, Cuong Chau. #ITP #ACL2
• The φ-weighted recognition hamiltonian: A self-adjoint operator unifying automorphic L-functions, E 8 symmetry, and cosmic dynamics. #ITP #LeanProver
• Computational p-adics (in Isabelle/HOL). ~ Jeremy Sylvestre. #ITP #IsabelleHOL #Math
• The oneway to hiding theorem (in Isabelle/HOL). ~ Katharina Kreuzer, Dominique Unruh. #ITP #IsabelleHOL
• Kraus maps (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL
• Parikh's theorem (in Isabelle/HOL). ~ Fabian Lehr. #ITP #IsabelleHOL
• Computer-assisted proofs for differential equations and dynamical systems. ~ Maxime Breden. #ITP #Math
• Comparing codes: Binary search in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Verified certificates via SAT and computer algebra systems for the Ramsey R(3,8) and R(3,9) problems. ~ Zhengyu Li et als. #SAT #CAS
• Bourbaki: Self-generated and goal-conditioned MDPs for theorem proving. ~ Matthieu Zimmer et als. #LLMs #ITP #LeanProver
• Clarifying before reasoning: A Coq prover with structural context. ~ Yanzhen Lu et als. #LLMs #ITP #CoqProver
• Curso "Lógica matemática y fundamentos (2019-20)". #Lógica #ProgramaciónFuncional #IsabelleHOL

The readings shared in Bluesky on 7 July 2025 are

• Lean: a theorem prover and programming language that enables correct, maintainable, and formally verified code. #ITP #LeanProver #FunctionalProgramming
• Curso "Razonamiento automático (2017-18)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL
• Curso "Lógica matemática y fundamentos (2018-19)". #Lógica #ProgramaciónFuncional #IsabelleHOL
• Curso "Razonamiento automático (2018-19)". #DemostraciónInteractiva #ProgramaciónFuncional #IsabelleHOL #Coq
• Curso "Informática (2019-20)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2019-20). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2019-20). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2019-20). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 5 July 2025 are

• The filter game (in Lean 4). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formal verification of quantum stabiliser codes by stabiliser formalism. ~ Qiuyi Feng. #ITP #CoqProver
• Formal methods at NASA: Past, present, and future. ~ Paul Miner, Natasha Neogi. #FormalMethods #ITP #PVS
• A proof-assisted conversion of signal temporal logic formulas into negative normal form. ~ Danil Berrah, François Pessaux, Alexandre Chapoutot. #ITP #Rocq
• Functorial flattening of the state monad via vector‐space projection (A formally verified collapse model in Lean 4). ~ Jinu Jang. #ITP #LeanProver
• A diagrammatic calculus for a functional model of natural language semantics. ~ Matthieu Pierre Boyer. #Haskell #FunctionalProgramming
• Implementing a type theory with observational equality, using normalisation by evaluation. ~ Matthew Sirman, Meven Lennon-Bertrand, Neel Krishnaswami. #Haskell #FunctionalProgramming
• AI4Research: A survey of artificial intelligence for scientific research. ~ Qiguang Chen et als. #AI
• Curso "Informática (2018-19)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2018-19). #Haskell #ProgramaciónFuncional
• Ejercicios de programación funcional con Haskell (curso 2018-19). #Haskell #ProgramaciónFuncional
• Exámenes de programación funcional con Haskell (curso 2018-19). #Haskell #ProgramaciónFuncional

The readings shared in Bluesky on 4 July 2025 are

• LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving. ~ Naoto Onda et als. #ITP #LeanProver #Math #LLMs
• An introduction logical foundations of types and programming language. ~ Brigitte Pientka. #TypeTheory
• Reflections on Haskell and Rust. ~ Sibi Prabakaran. #Haskell #FunctionalProgramming #Rust
• Category theory: Introducing the perfect language. ~ Richard Southwell #CategoryTheory
• Reseña de «LeanConjecturer: Automatic generation of mathematical conjectures for theorem proving». #ITP #LeanProver #Math #LLMs
• Curso "Razonamiento automático (2017-18)". #RazonamientoAutomático #DemostraciónInteractiva #IsabelleHOL
• Curso "Lógica matemática y fundamentos (2017-18)". #Lógica #IsabelleHOL