The readings shared in Bluesky on 25 May 2025 are

• Shallow expressions (in Isabelle/HOL). ~ Simon Foster. #ITP #IsabelleHOL
• Orgro: A mobile Org Mode file editor and viewer. #OrgMode

The readings shared in Bluesky on 24 May 2025 are

• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Munta: A verified model checker for timed automata (in Isabelle/HOL). ~ Simon Wimmer. #ITP #IsabelleHOL
• Learning Physics with functional programming and Haskell. ~ Esteban Marín. #Haskell #FunctionalProgramming #Physics
• Is AI making coders obsolete? (Are there problems with having AI tools take over coding from humans?). ~ Jennifer Goforth Gregory. #AIforCode

The readings shared in Bluesky on 23 May 2025 are

• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Solving guarded domain equations in presheaves over ordinals and mechanizing it. ~ Sergei Stepanenko, Amin Timany. #ITP #RocqProver #CategoryTheory
• Ineq-Comp: Benchmarking human-intuitive compositional reasoning in automated theorem proving on inequalities. ~ Haoyu Zhao et als. #LLMs #ITP #LeanProver #Math
• CLEVER: A curated benchmark for formally verified code generation. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver #AIforCode
• Formalisation of fairness notions in assignment problem. ~ Duc Minh Do. #ITP #IsabelleHOL

The readings shared in Bluesky on 22 May 2025 are

• A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. #ITP #ACL2 #Math
• Lean-auto: An interface between Lean 4 and automated theorem provers. ~ Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad. #ITP #LeanProver
• Lean-SMT: An SMT tactic for discharging proof goals in Lean. ~ Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark Barrett. #ITP #LeanProver
• The roots of Lisp. ~ Paul Graham (2002). #Lisp #Programming
• Las raíces de Lisp. ~ Paul Graham (2002). #Lisp #Programming
• LISP, el "lenguaje de DIOS". ~ LinuxChad. #Lisp #Programming

The readings shared in Bluesky on 21 May 2025 are

• Will computers prove theorems? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formalizing the future: Lean’s impact on mathematics, programming, and AI. ~ Leo De Moura. #ITP #LeanProver #Math #CompSci #AI
• A formalization of the correctness of the Floodsub protocol. ~ Ankit Kumar, Panagiotis Manolios. #ITP #ACL2
• OpenEvolve: Open-source implementation of AlphaEvolve. ~ Asankhaya Sharma. #AI #LLMs #AlphaEvolve #Math
• AlphaEvolveVerify: Verification of Google DeepMind's AlphaEvolve 48-multiplication matrix algorithm. ~ Deming Xu. #Python #Programming #Math
• Toward safe, flexible, and efficient software in Common Lisp. ~ Robert Smith. #CommonLisp
• Theorems and conjectures with Python. ~ Alessio Drivet. #Math #Python #Programming
• Analysis of selection noise in genetic algorithms. Nataliya M. Gulayeva, Joaquín Borrego-Díaz, Fernando Sancho-Caparrini. #GeneticAlgoritm
• org-expex: Expex glosses in Org-mode (Emacs org-mode extension to auto-create linguistic glosses). ~ David Diem. #Emacs #OrgMode

The readings shared in Bluesky on 20 May 2025 are

• Formalising the Bruhat-Tits tree. ~ Judith Ludwig, Christian Merten. #ITP #LeanProver
• Ordinal exponentiation in homotopy type theory. ~ Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #HoTT
• A Python frozenset interpretation of Dependent Type Theory. ~ Philip Zucker. #TypeTheory #Python #Logic
• Comparing code: LeetCode problems in Rust vs. Haskell. ~ James Bowen. #Haskell #FunctionalProgramming #Rust
• Symbolic sets for proving bounds on Rado numbers. ~ Tanbir Ahmed, Lamina Zaman, Curtis Bright #SAT #Python #Math
• Formatting academic papers in Emacs Orgmode. ~ Kenneth Flak. #Emacs #OrgMode

The readings shared in Bluesky on 19 May 2025 are

• A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. #ITP #LeanProver #Math
• Towards a mechanization of fraud proof games in Lean. ~ Martín Ceresa, César Sánchez. #ITP #LeanProver
• Farey sequences and Ford circles (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Formal verification of a fail-safe cross-chain bridge. ~ Filip Marić, Bernhard Scholz, Pavle Subotić. #ITP #IsabelleHOL
• Verifying smart contract transformations using bisimulations. ~ Kegan McIlwaine, James Caldwell. #ITP #IsabelleHOL
• Formally specifying contract optimizations with bisimulations in Coq. ~ Derek Sorensen. #ITP #Coq #Rocq
• Math for programming (Learn the math, write better code). ~ Ronald T. Kneusel. #Math #Python #Programming
• Lisp. But why? ~ Raj. #CommonLisp #Programming

The readings shared in Bluesky on 18 May 2025 are

• Formalizing a proof in Lean using Claude and o4. ~ Terence Tao. #ITP #LeanProver #Math
• Formalizing a proof in Lean using Github Copilot only. ~ Terence Tao. #ITP #LeanProver #Math
• Formal proof of Dilworth’s theorem (in Isabelle/HOL). ~ Vivek Soorya Maadoori et als. #ITP #IsabelleHOL #Math
• Benchmarking energy calculations using formal proofs. ~ Ejike D. Ugwuanyi, Colin T. Jones, John Velkey, Tyler R. Josephson. #ITP #LeanProver
• Freer arrows and why you need them. ~ Grant Vandomelen, Yao Li. #Haskell #FunctionalProgramming
• Computer science and mathematics: A powerful synergy. ~ Khaled M.M. Alrantisi, Mohammad Imtiyaz Gulbarga. #Math #CompSci
• Tipos abstractos y polimorfismo en programación funcional. ~ Emanuel Goette. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 17 May 2025 are

• Formalizing the future: Lean’s impact on mathematics, programming, and AI. ~ Leo De Moura. #ITP #LeanProver #Math #CompSci #AI
• Will computers prove theorems? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Recursive definitions in Lean. ~ Joachim Breitner. #ITP #LeanProver #FunctionalProgramming
• Digitalizing Wick's theorem. ~ Joseph Tooby-Smith. #ITP #LeanProver
• The Haskell Unfolder Episode 44: State-based testing with quickcheck-lockstep. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 16 May 2025 are

• AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms. ~ AlphaEvolve team. #AI #LLMs #AlphaEvolve #Math
• AlphaEvolve: A coding agent for scientific and algorithmic discovery. ~ AlphaEvolve team. #AI #LLMs #AlphaEvolve #Math
• The collapse of GPT (Will future artificial intelligence systems perform increasingly poorly due to AI-generated material in their training data?). ~ Neil Savage. #AI #GPT
• La última IA de Google promete ser capaz de mejorarse a sí misma. De momento, ya está superando a los matemáticos humanos. ~ Marcos Merino. #AI #LLMs #AlphaEvolve #Math

The readings shared in Bluesky on 15 May 2025 are

• Heftia: The final word in Haskell effect system libraries (Part 1.1). ~ Riyo. #Haskell #FunctionalProgramming
• Quasiquoting for fun, profit, expressions and patterns. ~ MLabs. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 14 May 2025 are

• Formal P-category theory and normalization by evaluation in Rocq. ~ David G. Berry, Marcelo P. Fiore. #ITP #Rocq #CategoryTheory
• Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. #ITP #Rocq #OCaml
• Theorem prover Arend. ~ Fedor Part, Valery Isaev, and Sergey Sinchuk. #ITP #Arend
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 13 May 2025 are

• Course: Functional programming and theorem proving in Lean 4. ~ Leni Aniva, Abdalrhman Mohamed. #ITP #LeanProver #FunctionalProgramming
• Formalizing a proof in Lean using Github copilot and canonical. ~ Terence Tao. #ITP #LeanProver #Math
• APOLLO: Automated LLM and Lean collaboration for advanced formal reasoning. ~ Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh. #LLMs #ITP #LeanProver
• La gran ilusión de la IA: no piensa, no siente, pero habla como si lo hiciera. ~ Ramón López de Mántaras. #IA

The readings shared in Bluesky on 10 May 2025 are

• A tool to verify estimates, II: a flexible proof assistant. ~Terence Tao. #ITP #Python #Math
• How to (actually) prove it - New frontiers of mathematics & computing in Lean. ~ Kiran. #ITP #LeanProver #Math
• LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. #ITP #LeanProver #Mathlib
• How do undergraduates do mathematics? (A guide to studying mathematics at Oxford University). #Math

The readings shared in Bluesky on 9 May 2025 are

• Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord and Julien Narboux. #ATP #ITP #IsabelleHOL #LeanProver #Coq #Rocq #Education
• Maths with Coq in L1, a pedagogical experiment. ~ Marie Kerjean, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Logic #Math #Teaching
• Teaching divisibility and binomials with Coq. ~ Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Math #Teaching
• A graphical interface for category theory proofs in Coq. ~ Luc Chabassier. #ITP #Coq #Rocq #CategoryTheory
• OnlineProver: Experience with a visualisation tool for teaching formal proofs. ~ Ján Perháč et als. #ITP #Logic #Teaching
• Minimal sequent calculus for teaching first-order logic: Lessons learned. ~ Jørgen Villadsen. #ITP #IsabelleHOL #Logic #Teaching
• ProofBuddy (How it started, how it's going). ~ Nadine Karsten, Kim Jana Eiken, Uwe Nestmann. #ITP #IsabelleHOL #Logic #Teaching
• Lean4 machine assisted proof framework for chip firing game & graphical Riemann-Roch. ~ Dhyey Dharmendrakumar Mavani. #ITP #LeanProver
• Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. #ITP #Coq #Rocq
• Analyzing API design via algebraic laws. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Beginnings of a Haskell game engine. ~ Mitchell Vitez. #Haskell #FunctionalProgramming
• Scrap your iteration combinators. ~ Tom Ellis. #Haskell #FunctionalProgramming
• From Haskell to a new structured combinator processor. ~ Yukang Xie et als. #Haskell #FunctionalProgramming
• Lógicas de orden superior y verificación formal. ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
• Lógicas de orden superior y verificación formal (Slides). ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq

The readings shared in Bluesky on 8 May 2025 are

• SAT-solving the poset cover problem. ~ Chih-Cheng Rex Yuan, Bow-Yaw Wang. #ATP #SAT_solvers #Z3
• FormalMATH: Benchmarking formal mathematical reasoning of large language models. ~ Zhouliang Yu et als. #LLMs #Autoformalization #Math #ITP #LeanProver
• Beyond theorem proving: Formulation, framework and benchmark for formal problem-solving. ~ Qi Liu et als. #LLMs #ITP #LeanProver
• The Haskell Unfolder Episode 43: Monomorphism restriction and defaulting. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• What is programming?… and what is programming in the age of artificial intelligence? ~ Sebastian Nicolajsen, Claus Brabrand. #Programming

The readings shared in Bluesky on 6 May 2025 are

• Sophie Germain’s theorem (in Isabelle/HOL). ~ Benoît Ballenghien. #ITP #IsabelleHOL #Math
• Recamán’s sequence. ~ John D. Cook. #Math #Python
• 25 useful tips for Emacs (for beginners and advanced users). Raoul Comninos. #Emacs

The readings shared in Bluesky on 5 May 2025 are

• Compiling Haskell into Lean: A common abstract syntax for Haskell and interactive theorem provers. ~ Talitha Holcombe. #Haskell #FunctionalProgramming #ITP #LeanProver
• Avaliando a habilidade do ChatGPT de realizar provas de dedução natural em lógica proposicional e lógica de predicados. ~ Francisco Leonardo Batista Martins et als. #LLLms #ChatGPT #Logic
• Typed Lisp, a primer. ~ Musa Al-hassy (2019). #CommonLisp #Haskell

The readings shared in Bluesky on 4 May 2025 are

• Formalizing resource ownership semantics of spinlocks with the Coq proof assistant. ~ Sebastian Luis S. Ortiz et als. #ITP #Coq #Rocq
• Formalizing reversible computations for synchronous dataflow languages with infinite lists. ~ Sosuke Moriguchi et als. #ITP #Coq #Rocq
• Formal verification of blockchain nonforking in DAG-based BFT consensus with dynamic stake. ~ Alessandro Coglio, Eric McCarthy. #ITP #ACL2
• The minimal megaparsec tutorial. ~ Clément Hurlin. #Haskell #FunctionalProgramming
• Mathematician solves algebra's oldest problem using intriguing new number sequences. ~ University of New South Wales. #Math
• A hyper-Catalan series solution to polynomial equations, and the Geode. ~ N.J. Wildberger, Dean Rubine. #Math
• Entrevista a Jeffrey Ullman (ACM Turing Award). ~ Camilo Chacón Sartori. #Computación

The readings shared in Bluesky on 2 May 2025 are

• A proof of concept tool to verify estimates. ~ Terence Tao. #Math #AI #LLMs #ChatGPT #Python
• Advancing mathematics by guiding human intuition with AI. ~ Alex Davies et als. (2021). #Math #AI
• Semantics of probabilistic programs using s-finite kernels in dependent type theory. ~ Reynald Affeldt, Cyril Cohen, Ayumu Saito. #ITP #Rocq
• DeepIsaHOL progress report: current machine learning for the Isabelle proof assistant. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL #LLMs
• Frontier of formal theorem proving with large language models: Insights from the DeepSeek-Prover. ~ Huajian Xin. #ITP #LeanProver #LLMs #DeepSeek
• Automated theorem provers as the hub of the AI math ecosystem. ~ Stephan Schulz. #Math #AI #ITP

The readings shared in Bluesky on 1 May 2025 are

• DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. ~ Z.Z. Ren et als. #LLMs #ITP #LeanProver
• Mathematical beauty, truth and proof in the age of AI. ~ Jordana Cepelewicz. #Math #AI #ITP
• Logical modelling in CS education: Bridging the natural language gap. ~ Tristan Kneisel, Fabian Vehlken, Thomas Zeume. #Logic #Education
• Iltis: An interactive, web-based system for teaching formal foundations of computer science. #Logic #Education
• Introduction to Iltis: An interactive, web-based system for teaching logic. ~ Gaetano Geck et als. (2018). #Logic #Teaching
• Iltis: Learning Logic in the Web. ~ Gaetano Geck et als. (2022). #Logic #Teaching
• Clear: A formal verification framework for smart contracts in Lean. ~ Julian Sutherland. #ITP #LeanProver

The readings shared in Bluesky on 30 April 2025 are

• Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. #ITP #Coq #Rocq
• Verified hand-written Lean solutions to HumanEval. ~ Markus Himmel. #ITP #LeanProver

The readings shared in Bluesky on 29 April 2025 are

• Improving mathematical proving skills through interactive theorem proving. ~ Sana Stojanović Đurđević, Andrija Urošević, Filip Marić (2024). #ITP #IsabelleHOL #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #LeanProver #Math

The readings shared in Bluesky on 28 April 2025 are

• Tutte's theorem as an educational formalization project. ~ Pim Otte. #ITP #LeanProver #Math
• Haskelling my Python (Reimplementing Haskell lazy infinite lists using Python generators). ~ Unnamed Website. #Python #Haskell #FunctionalProgramming #Math
• Power series, power serious. ~ M. Douglas McIlroy (1998). #Haskell #FunctionalProgramming #Math
• Tree rewriting calculi for strictly positive logics. ~ Sofía Santiago-Fernández, David Fernández-Duque, Joost J. Joosten. #Logic

The readings shared in Bluesky on 27 April 2025 are

• Bitcoinolog: Reason about Bitcoin addresses with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Working with Common Lisp pathnames. ~ Nicolas Martyanoff. #CommonLisp
• AI for program verification. ~ Cristian Cadar, Abhik Roychoudhury. #AI #FormalVerification
• Introducing category theory (Version 26 Apr 2025). ~ Peter Smith. #CategoryTheory
• The levels of Emacs proficiency. ~ Vivek Haldar (2011). #Emacs

The readings shared in Bluesky on 25 April 2025 are

• Lean 4 formalization of the logic textbook "Logic Notes" by Lou van den Dries. ~ Will Bradley. #ITP #LeanProver #Logic #Math
• Neural theorem proving: Generating and structuring proofs for formal verification. ~ Balaji Rao, William Eiers, Carlo Lipizzi. #LLMs #ITP #IsabelleHOL
• Mathematical Logic (Math 570) Lecture Notes. ~ Lou van den Drie. #Logic #Math
• Implementing Unsure Calculator in 100 lines of Haskell. ~ Rodrigo Mesquita. #Haskell #FunctionalProgramming
• Integrating effectful and persistent. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Porting song recommendations to Haskell. ~ Mark Seemann. #Haskell #FunctionalProgramming
• Magical Haskell: A friendly approach to modern functional programming, type theory, and artificial intelligence. ~ Anton Antich. #Haskell #FunctionalProgramming #AI
• #Exercitium: Duplicación de cada elemento. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 24 April 2025 are

• On the averaging problem of ideal families related to Frankl's conjecture with formal proof by Lean 4. ~ Masahiro Hachimori, Kenji Kashiwabara. #ITP #LeanProver #Math
• #Exercitium: Sistema factorádico de numeración. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 23 April 2025 are

• Bullshit universities: the future of automated education. ~ Robert Sparrow, Gene Flenady. #GenerativeAI #Education
• #Exercitium: Suma de cadenas. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∪ f⁻¹[v]​] ⊆ f[s] ∪ v". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 22 April 2025 are

• The inverse method is a good fit for Datalog theorem proving. ~ Philip Zucker. #Datalog #Logic
• In between myth and reality: AI for math (a case study in category theory). ~ Răzvan Diaconescu. #LLMs #Math
• #Exercitium: Cuadrado más cercano. #Haskell #Python #CommonLisp
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ∩ t = f(s ∩ f⁻¹(t)". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 21 April 2025 are

• A formalisation of Aristotle’s assertoric syllogistic in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Karol Wapniarski. #ITP #IsabelleHOL #Logic
• Non-circular trigonometric proofs of the pythagorean theorem in Lean4: A comparison. ~ Paul Pajo. #ITP #LeanProver #Math
• Enhancing AI trustworthiness through automated reasoning: A novel method for explaining deep learning and LLM reasoning. ~ Julia Connolly, Oliver Stanton, Sarah Veronica, Liam Whitmore. #LLMs #Reasoning #ITP
• SLip: Lisp system in your browser. ~ Mihai Bazon. #CommonLisp
• #Exercitium: Divisores de un número con final dado. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] \ f[t] ⊆ f[s \ t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 20 April 2025 are

• Readings shared April 19, 2025. #Algorithms #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #MachineLearning #Math #Python #SMT #Z3
• Gridbach: Un proyecto para comprobar de forma distribuida la famosa conjetura de Goldbach. ~ @Alvy #Matemáticas
• Gridbach: The grid-computing system that calculates verification of the mathematical problem "Goldbach conjecture". #Math
• #Exercitium: Órbita prima. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 19 April 2025 are

• Knuckledragger: A low barrier proof assistant. ~ Philip Zucker. #ITP #SMT #Z3 #Python
• Neural theorem proving tutorial. ~ Sean Welleck. #MachineLearning #ITP #LeanProver
• Listing prime numbers periodically. ~ Han-Lin Li, Shu-Cherng Fang, Way Kuo, Nianrui Lin. #Math #Algorithms
• #Exercitium: Ordenada cíclicamente. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∩ t] ⊆ f[s] ∩ f[t]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 18 April 2025 are

• #Exercitium: Eliminación de las ocurrencias aisladas. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 17 April 2025 are

• Formalization of Fraïssé limits in Lean. ~ Gabin Kolly. #ITP #LeanProver #Math
• A readable and computable formalization of the Streamlet consensus protocol. ~ Mauro Jaskelioff, Orestis Melkonian, James Chapman. #ITP #Agda
• The Haskell Unfolder Episode 42: Logic programming with typedKanren. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Emparejamiento de árboles. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]​". #LeanProver #IsabelleHOL #Math

The readings shared in Bluesky on 15 April 2025 are

• Simplified and verified: A second look at a proof-producing union-find algorithm. ~ Lukas Stevens, Rebecca Ghidini. #ITP #IsabelleHOL
• First-order rewriting (in Isabelle/HOL). ~ René Thiemann et als. #ITP #IsabelleHOL
• Proof terms for term rewriting (in Isabelle/HOL). ~ Christina Kirk. #ITP #IsabelleHOL
• The Kolmogorov-Chentsov theorem (in Isabelle/HOL). ~ Christian Pardillo-Laursen, Simon Foster. #ITP #IsabelleHOL #Math
• Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. ~ Numina & Kimi Team. #LLMs #LeanProver
• Mathematical reasoning & proofs. ~ Alistair Savage. #Math
• Decomposing factorial of 300K as the product of 300K factors larger than 100K. ~ Gustavo. #Programming #RacketLang #FunctionalProgramming #Math
• Emacs Lisp elements (A big picture view of the Emacs Lisp programming language). ~ Protesilaos Stavrou. #Emacs #Lisp
• The Barium experiment. ~ Tom Szilagyi. #CommonLisp
• #Exercitium: Separación por posición. #Haskell #ProgramaciónFuncional #Matemáticas
• #Calculemus: Demostraciones con Lean4 y con Isabelle/HOL de "Monotonía de la imagen de conjuntos". #LeanProver #IsabelleHOL #Math

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⁻¹(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

The readings shared in Bluesky on 30 March 2025 are

• Towards mechanized verification of Verilog equivalence checking. ~ Michalis Pardalos, Laura Pozzi, John Wickerson. #ITP #Coq
• Introducing clean, a formal verification DSL for zk circuits in Lean4. ~ Giorgio Dell'Immagine. #ITP #LeanProver
• #Exercitium: Regiones determinadas por n rectas del plano. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "La unión del conjunto de los números naturales pares e impares es el conjunto de los naturales". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Informática (2010-11)". #Haskell #ProgramaciónFuncional #Algorítmica #CálculoSimbólico #Maxima
• Temas de "Programación funcional" (2010-11). #Haskell #ProgramaciónFuncional
• Ejercicios de "Informática de 1º de Matemáticas" (2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Exámenes de "Programación funcional con Haskell" Vol. 2 (Curso 2010–11). #Haskell #ProgramaciónFuncional #Matemáticas
• Introducción al cálculo simbólico con Maxima. #CálculoSimbólico #Maxima #Matemáticas

The readings shared in Bluesky on 29 March 2025 are

• Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. #ITP #LeanProver
• #Exercitium: Ampliación de matrices por columnas. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 28 March 2025 are

• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• Verified collaboration: How Lean is transforming mathematics, programming, and AI. ~ Leonardo de Moura. #ITP #LeanProver #Math #Programming #AI
• The philosophical problem of induction, and the problem of Fetzer. ~ Lawrence Paulson. #Philosophy #Math #CompSci
• #Exercitium: Emparejamiento binario. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "(s \ t) ∪ t = s ∪ t". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2009-10)". #Lógica #Matemática #Computación
• Temas de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Ejercicios de "Lógica informática" (2009-10). #Logic #Math #CompSci
• Soluciones de exámenes de Lógica informática (2000-07). #Logic #Math #CompSci
• Curso "Programación declarativa (2009-10)". #Haskell #FunctionalProgramming #Prolog #LogicProgramming
• Temas de "Programación funcional con Haskell" (2009-10). #Haskell #FunctionalProgramming
• Introducción a la programación lógica con Prolog. #Prolog #LogicProgramming
• Ejercicios de programación funcional con Haskell (versión del 20 de septiembre de 2007). #Haskell #FunctionalProgramming
• Ejercicios de programación lógica con Prolog (Versión de 20 de septiembre de 2007). #Prolog #LogicProgramming

The readings shared in Bluesky on 27 March 2025 are

• Formalization of optimality conditions for smooth constrained optimization problems. ~ Chenyi Li et als. #ITP #LeanProver
• Formalization of algorithms for optimization with block structures. ~ Chenyi Li, Zichen Wang et als. #ITP #LeanProver
• Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. #ITP #Coq #Rocq #Logic
• Automated reasoning in blockchain: Foundations, applications, and frontiers. ~ Hojer Key. #ITP #Blockchain
• Functional programming in Haskell. ~ Graham Hutton. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 41: Generic monoids. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Decomposing a factorial into large factors. ~ Terence Tao. #Math
• Mathematics of the “I Ching”. ~ Peter Rowlett. #Math #TeXLaTeX
• Apuntes de programación lógica (Hasta Prolog y más allá). ~ Joaquín Arias. #LogicProgramming #Prolog #CLP
• #Exercitium: Ordenación de estructuras. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (s ∩ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 26 March 2025 are

• Formal proof of Dilworth's theorem (in Isabelle/HOL). ~ Vivek Soorya Maadoori et als. #ITP #IsabelleHOL #Math
• Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong, Tianming Liu. #AI #Math
• LogicLearner: A tool for the guided practice of propositional logic proofs. ~ Amogh Inamdar et als. #Logic
• #Exercitium: Numeración de las ternas de números naturales. #Haskell #ProgramaciónFuncional #Matemáticas
• Curso "Informática (2009-10)". #Haskell #ProgramaciónFuncional #Maxima

The readings shared in Bluesky on 25 March 2025 are

• Teaching "Foundations of Mathematics" with the Lean theorem prover. ~ Mattia Luciano Bottoni, Alberto Cattaneo, Elif Sacikara. #ITP #LeanProver #Math
• Ten Commandments of the Church of Emacs. #Emacs
• #Exercitium: Alfabeto comenzando en un carácter. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ (s ∪ t) = s". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 24 March 2025 are

• Formal verification of machine learning models in Lean. ~ Matéo H. Petel. #ITP #LeanProver #MachineLearning
• Why Lisp syntax works. ~ Fernando Borretti. #Lisp #Programming
• MathGPT: Your personal math solver (Get instant homework help from your on-demand AI math solver). #AI #LLMs #Math
• MathGPT: una herramienta para resolver problemas matemáticos y ayudar con los deberes. ~ @Alvy. #IA #LLMs #Matemáticas
• Exercitium (Un reto diario de programación). #Exercitium #Haskell #ProgramaciónFuncional
• #Exercitium: Ramas de un árbol. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ t = t ∩ s". #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Programación lógica (2008-09)". #ProgramaciónLógica #Prolog #IA
• Curso "Razonamiento automático (2008-09)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

The readings shared in Bluesky on 23 March 2025 are

• A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. #ITP #Coq #IsabelleHOL #HOL_Light #Mizar #LeanProver #Math
• Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu (2019). #ITP #Coq #SetTheory
• A formal proof in Coq of Cantor-Bernstein-Schroeder’s theorem without axiom of choice (2019). #ITP #Coq #SetTheory
• A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu (2020). #ITP #Coq #SetTheory
• A formalization of properties of continuous functions on closed intervals. Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalization of the equivalence among completeness theorems of real number in Coq. ~ Yaoshun Fu, Wensheng Yu (2020). #ITP #Coq #Math
• Formalizing calculus without limit theory in Coq. ~ Yaoshun Fu, Wensheng Yu (2021). #ITP #Coq #Math
• A formalization of topological spaces in Coq. ~ Sheng Yan, Yaoshun Fu, Dakai Guo, and Wensheng Yu (2022). #ITP #Coq #Math #SetTheory
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). #ITP #Coq #Math #SetTheory
• Implementation of Bourbaki's elements of mathematics in Coq: Part one, theory of sets. ~ José Grimm (2009). #ITP #Coq #SetTheory
• Implementation of Bourbaki’s elements of mathematics in Coq: Part two, ordered sets, cardinals, integers. ~ José Grimm (2018). #ITP #Coq #Math
• Concurrent games in Agda. ~ Amy Yin. #ITP #Agda
• #Exercitium: Valores de polinomios representados con vectores. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones con Lean4 y con Isabelle/HOL de "s \ (t ∪ u) ⊆ (s \ t) \ u". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 22 March 2025 are

• Non-obvious Haskell idiom: Guard-sequence. ~ kqr. #Haskell #FunctionalProgramming
• Learn Haskell by example. ~ Phillip Hagenlocher. #Haskell #FunctionalProgramming
• #Exercitium: Segmentos maximales con elementos consecutivos. #Haskell #ProgramaciónFuncional
• Demostraciones con Lean4 y con Isabelle/HOL de "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)". #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 21 March 2025 are

• Case study: Verified Vampire proofs in the LambdaPi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suad. #ATP #Vampire #Dedukti
• A hundred pull requests for Liquid Haskell. ~ Facundo Domínguez. #Liquid #Haskell #FunctionalProgramming #SMT
• Artificial intelligence learns to reason. ~ Melanie Mitchell. #AI #LLMs #Reasoning
• #Exercitium: Lista cuadrada. #Haskell #ProgramaciónFuncional
• Demostraciones de "(a ∖ b) ∖ c ⊆ a ∖ (b ∪ c)" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus
• Curso "Lógica informática (2008-09)". #Lógica #Matemática #Computación
• Curso "Programación declarativa (2008-09)". #ProgramaciónFuncional #Haskell #ProgramaciónLógica #Prolog

The readings shared in Bluesky on 19 March 2025 are

• A trickier lower bound proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Can LLMs enable verification in mainstream programming? ~ Aleksandr Shefer et als. #LLMs #Programming #FormalVerification
• Towards AI-assisted academic writing. ~ Daniel J. Liebling et als. #AI #LLMs
• VisuAlgo: Visualising data structures and algorithms through animation. #Programming #CompSci
• VisuAlgo muestra visualmente cómo funcionan los algoritmos, las estructuras de datos y cómo resolver problemas. ~ @Alvy. #Programación #Computación
• #Exercitium: Matrices de Toepliz. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones de "Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 19 March 2025 are

• #Exercitium: Máximos locales. #Haskell #ProgramaciónFuncional #Matemáticas
• Demostraciones de "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" con Lean4 y con Isabelle/HOL. #LeanProver #IsabelleHOL #Math #Calculemus

The readings shared in Bluesky on 18 March 2025 are

• Lessons learned with the Z3 SAT/SMT solver. ~ John D. Cook. #SMT #Z3
• Teaching logic programming: a review. ~ Serhiy O. Semerikov, Iryna S. Mintii, Natalia V. Moiseienko. #LogicProgramming #Prolog #ASP #CLP #Datalog
• Series vs. streams. ~ Joe Marshall. #CommonLisp
• #Exercitium: Suma si todos los valores son justos. #Haskell #ProgramaciónFuncional
• #Calculemus: Demostrar con Isabelle/HOL que las relaciones reflexivas y circulares son simétricas. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2007-08)". #ProgramaciónFuncional #Haskell #ProgramaciónLógica #Prolog
• Curso "Programación lógica (2007-08)". #ProgramaciónLógica #Prolog #IA
• Curso "Razonamiento automático (2007-08)". #RazonamientoAutomático #Otter #Mace2 #Prover9 #Mace4 #DemostraciónInteractiva #IsabelleHOL

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

The readings shared in Bluesky on 7 March 2025 are

• A formalisation of addition chains. ~ Laurent Théry. #ITP #Coq #Rocq
• QED in context (An observation study of proof assistant users). ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C. Pierce, Andrew Head #ITP #LeanProver #Coq #Rocq
• On the formalization of the simplicial model of HoTT. ~ Kunhong Du. #ITP #Agda #HoTT
• A gentle introduction to categorical logic and type theory. ~ Eric Schmid. #Math #CategoryTheory #TypeTheory
• MathMistake checker: A comprehensive demonstration for step-by-step math problem mistake finding by prompt-guided LLMs. ~ Tianyang Zhang et als. #LLMs #Math
• A survey on Large Language Models for code generation. ~ Nam Huynh, Beiyu Lin. #LLMs #Programming
• Markov chain of thought for efficient mathematical reasoning. ~ Wen Yang, Minpeng Liao, Kai Fan. #LLMs #Math #Reasoning
• Assisting mathematical formalization with a learning-based premise retriever. ~ Yicheng Tao et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 6 March 2025 are

• Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. #ITP #Coq #Rocq
• Lean-STaR: Learning to interleave thinking and proving. ~ Haohan Lin et als. #LLMs #ITP #LeanProver
• MA-LoT: Multi-agent lean-based long chain-of-thought reasoning enhances formal theorem proving. ~ Ruida Wang et als. #LLMs #ITP #LeanProver
• FANS: Formal answer selection for natural language math reasoning using Lean4. ~ Jiarui Yao, Ruida Wang, Tong Zhang. #LLMs #ITP #LeanProver
• From informal to formal (Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs). ~ Jialun Cao et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 5 March 2025 are

• Language partitioning for mission-time linear temporal logic (in Isabelle/HOL). ~ Zili Wang, Katherine Kosaian, Alec Rosentrater. #ITP #IsabelleHOL
• Unos profesores avisan de que la IA supone una amenaza para el pensamiento crítico de los estudiantes: "escribir también es pensar". ~ Marcos Merino. #AI #Education

The readings shared in Bluesky on 4 March 2025 are

• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #LLMs #ITP #LeanProver
• Gold-medalist performance in solving olympiad geometry with AlphaGeometry2. ~ Yuri Chervonyi et als. #AI #AlphaGeometry #Math
• NL2FOL: Translating natural language to first-order logic for logical fallacy detection. ~ Abhinav Lalwani et als. #LLMs #Logig #SMT
• Utilizing ChatGPT in a data structures and algorithms course: A teaching assistant's perspective. ~ Pooriya Jamie, Reyhaneh Hajihashemi, Sharareh Alipour. #LLMs #CompSci
• Performance review on LLM for solving Leetcode problems. ~ Lun Wang et als. #LLMs #Programming
• InductionBench: LLMs fail in the simplest complexity class. ~ Wenyue Hua et als. #LLMs #Reasoning

The readings shared in Bluesky on 2 March 2025 are

• Faithful logic embeddings in HOL (A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• BiCoq: Bigraphs formalisation with Coq. ~ Cécile Marcon et als. #ITP #Coq #Rocq

The readings shared in Bluesky on 2 March 2025 are

• Waterproof: Transforming a proof assistant into an educational tool. ~ Aalt Jelle Wemmenhove. #ITP #Coq #Math #Education
• Computer assisted mathematical proofs: using the computer to verify computers. ~ Herman Geuvers. #ITP #Math
• An invitation to Blueprint-driven formalisation of mathematical research in Lean. ~ Pietro Monticone. #ITP #LeanProver #Math
• An invitation to Blueprint-driven formalisation of mathematical research in Lean (Codes). ~ Pietro Monticone. #ITP #LeanProver #Math
• Formalizing MLTL formula progression in Isabelle/HOL. ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Rozier. #ITP #IsabelleHOL #Logic
• Applying purity to the imperative world. ~ Jeremy Bowers. #Haskell #FunctionalProgramming
• ¿Podemos creer la prueba de la conjetura? ~ Marta Macho Stadler. #Math #CompSci

The readings shared in Bluesky on 1 March 2025 are

• Functional pearl: How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. #FunctionalProgramming #Haskell
• A combinatorial identities benchmark for theorem proving via automated theorem generation. ~ Beibei Xiong et als. #LLMs #ITP #LeanProver #Math
• Herald: A natural language annotated Lean 4 dataset. ~ Guoxiong Gao et als. #LLMs #ITP #LeanProver #Math
• LeanProgress: Guiding search for neural theorem proving via proof progress prediction. ~ Suozhi Huang et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 28 February 2025 are

• Is mathematics obsolete? ~ Jeremy Avigad. #Math #ITP #LeanProver #AI #LLMs
• Faithful logic embeddings in HOL (A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level). ~ Christoph Benzmüller. #ITP #IsabelleHOL #Logic
• Mathematical introduction to deep learning: Methods, implementations, and theory. ~ Arnulf Jentzen, Benno Kuckuck, Philippe von Wurstemberger. #AI #DeepLearning #Math
• Teaching LLMs according to their aptitude: Adaptive reasoning for mathematical problem solving. ~ Xin Xu et als. #AI #LLMs #Math
• Homo ratiocinator (reckoning human). ~ Moshe Y. Vardi. #Logic #CompSci
• PPA: Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman. ~ Manuel Panichelli. #Haskell #FunctionalProgramming #Logic

The readings shared in Bluesky on 27 February 2025 are

• Compactness theorem for first-order logic (in Isabelle/HOL). ~ Sophie Tourret, Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
• CuDIP: Enhancing theorem proving in LLMs via curriculum learning-based direct preference optimization. ~ Shuming Shi et als. #AI #LLMs #ATP #Logic #Math
• TheoremExplainAgent: Towards multimodal explanations for LLM theorem understanding. ~ Max Ku et als. #AI #LLMs #ATP #Logic #Math
• ChatGPT vs. DeepSeek: A comparative study on AI-based code generation. ~ Md Motaleb Hossen Manik. #AI #LLMs #Programming

The readings shared in Bluesky on 26 February 2025 are

• Big-Math: A large-scale, high-quality math dataset for reinforcement learning in language models. ~ Alon Albalak et als. #LLMs #Math
• UGMathBench: A diverse and dynamic benchmark for undergraduate-level mathematical reasoning with large language models. ~ Xin Xu et als. #LLMs #Math
• Empowering LLMs with logical reasoning: A comprehensive survey. ~ Fengxiang Cheng et als. #LLMs #Math #Reasoning

The readings shared in Bluesky on 25 February 2025 are

• Towards a formalized theory of solid modules. ~ Dagur Asgeirsson. #PhDThesis #ITP #LeanProver #Math
• Prove your colorings: Formal verification of cache coloring of Bao hypervisor. ~ Axel Ferréol, Laurent Corbin, Nikolai Kosmatov. #ITP #Coq #Rocq
• Logic.py: Bridging the gap between LLMs and constraint solvers. ~ Pascal Kesseli, Peter O'Hearn, Ricardo Silveira Cabral. #LLMs #Logic #SAT #SMT

The readings shared in Bluesky on 24 February 2025 are

• Formalising Brauer group and group cohomology in Lean4.~ Jujian Zhang. #ITP #LeanProver #Math
• The Haskell road to logic, math and programming. ~ Kees Doets, Jan van Eijck (2004). #Haskell #FunctionalProgramming #Logic #Math
• Bind and traverse with Kleisli morphisms. ~ Murat Kasimov. #CategoryTheory #Haskell #FunctionalProgramming
• Elements of Clojure. ~ Zachary Tellman. #Clojure #Lisp #FunctionalProgramming
• Open Reasoning Data (1,748,344 questions and 300,119 chain-of-thought traces to train open models). #AI #LLMs
• Material abierto para construir modelos de razonamiento general: 1.600.000 preguntas y 270.000 trazas de cadenas de pensamiento. ~ Por @Alvy. #AI #LLMs

The readings shared in Bluesky on 23 February 2025 are

• Power operator for lists (in Isabelle/HOL). ~ Štěpán Holub, Martin Raška, Štěpán Starosta, Tobias Nipkow. #ITP #IsabelleHOL
• Strands Rocq: Why is a security protocol correct, mechanically? ~ Matteo Busi, Riccardo Focardi, Flaminia L. Luccio. #ITP #Rocq #Coq
• Fracterm calculus for partial meadows. ~ Jan A. Bergstra, Alban Ponse. #ATP #Prover9 #Mace4 #Math
• How to deepen your understanding of Mizar. ~ Alex Nelson. #ITP #Mizar

The readings shared in Bluesky on 22 February 2025 are

• Lambda calculus and Lisp, part 1. #LambdaCalculus #Lisp
• Lambda calculus and Lisp, part 2. #LambdaCalculus #Emacs #Lisp

The readings shared in Bluesky on 21 February 2025 are

• Machine-assisted proofs (February 19, 2025). ~ Terence Tao. #ITP #LeanProver #AI #Math
• Formalisation of combinatorial optimisation in Isabelle/HOL: Network flows. ~ Thomas Ammer. #ITP #IsabelleHOL #Math
• A Coq implementation of a theory of tagged objects. ~ Matthew Gates, Alex Potanin. #ITP #Coq #Rocq
• Formal analysis of electrical circuit network topologies using theorem proving, ~ Kubra Aksoy, Adnan Rashid1, Osman Hasan, Sofiene Tahar. #ITP #IsabelleHOL
• Learn programming with OCaml (Algorithms and data structures). ~ Sylvain Conchon, Jean-Christophe Filliâtre. #OCaml #FunctionalProgramming
• Formalizing complex mathematical statements with LLMs: A study on mathematical definitions. ~ Lan Zhang, Marco Valentino, Andre Freitas. #LLMs #Math #Autoformalization #ITP #IsabelleHOL
• Diverse inference and verification for advanced reasoning. ~ Iddo Drori et als. #LLMs #ITP #LeanProver #Autoformalization
• Advice for writing proofs. ~ Evan Chen (2023). #Math
• Intro to proofs for the morbidly curious. ~ Evan Chen (2024). #Math

The readings shared in Bluesky on 20 February 2025 are

• Simplifying formal proof-generating models with ChatGPT and basic searching techniques. ~ Sangjun Han et als. #LLMs #ITP #LeanProver
• Proving olympiad inequalities by synergizing LLMs and symbolic reasoning. ~ Zenan Li et als. #LLMs #ITP #LeanProver #Math
• The role of GitHub Copilot on software development: A perspective on productivity, security, best practices and future directions. ~ Suresh Babu Nettur et als. #LLMs #Programming
• Competitive programming with large reasoning models. ~ OpenAI. #LLMs #Programming
• A brief introduction to olympiad inequalities. ~ Evan Chen. #Math
• Topics in inequalities: Theorems and techniques. ~ Hojoo Lee. #Math
• 567 nice and hard inequalities. ~ Nguyen Duy Tung. #Math
• #Exercitium: Lista cuadrada. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 19 February 2025 are

• Automating math (Computers can already help verify proofs. One day soon, AI may be able to come up with new ones). ~ Adam Marblestone. #ITP #LeanProver #AI #LLMs #Math
• These years in Common Lisp: 2023-2024 in review. ~ Vincent Dardel. #CommonLisp
• From informal to formal - Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs. ~ Jialun Cao et als. #LLMs #Reasoning #Math #ITP #LeanProver #Coq
• ProofWala: Multilingual proof data synthesis and theorem-proving. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver #Coq
• Integrating arithmetic learning improves mathematical reasoning in smaller models. ~ Neeraj Gangwar, Suma P Bhat, Nickvash Kani. #ITP #Math #Reasoning
• Theorem prover as a judge for synthetic data generation. ~ Joshua Ong Jun Leang et als. #LLMs #ITP
• A mechanistic interpretation of syllogistic reasoning in auto-regressive language models. ~ Geonhee Kim, Marco Valentino, André Freitas. #LLMs #Logic #Reasoning
• Teaching LLMs according to their aptitude: Adaptive reasoning for mathematical problem solving. ~ Xin Xu et als. #LLMs #Math
• LLMs for mathematical modeling: Towards bridging the gap between natural and mathematical languages. ~ Xuhan Huang et als. #LLMs #Math
• Step guided reasoning: Improving mathematical reasoning using guidance generation and step reasoning. ~ Lang Cao et als. #LLMs #Reasoning #Math
• #Exercitium: Máximos locales. #Haskell #Python #CommonLisp #Math

The readings shared in Bluesky on 18 February 2025 are

• Large language models and mathematical reasoning failures. ~ Johan Boye, Birger Moell. #AI #LLMs #Math
• #Exercitium: Matrices de Toepliz. #Haskell #Python #CommonLisp #Math

The readings shared in Bluesky on 17 February 2025 are

• Natural transformations as a basis of control. ~ Murat Kasimov. #Haskell #FunctionalProgramming
• To type or not to type? ~ Jonathan Chun. #Python #Programming
• Diverse inference and verification for advanced reasoning. ~ Iddo Drori et als. #AI #LLMs #ITP #LeanProver
• MathConstruct: Challenging LLM reasoning with constructive proofs. ~ Mislav Balunović et als. #AI #LLMs #Math
• MathGAP: Out-of-distribution evaluation on problems with arbitrarily complex proofs. ~ Andreas Opedal et als. #AI #LLMs #Math
• Personalizando Emacs. ~ Ivan Agosto. #Emacs

The readings shared in Bluesky on 16 February 2025 are

• The relationship between category theory, lambda calculus, and functional programming in Haskell. ~ Antonio Montano. #Haskell #FunctionalProgramming #CategoryTheory #LambdaCalculus
• Logical reasoning in large language models: A survey. ~ Hanmeng Liu et als. #LLMs #Logic #Reasoning

The readings shared in Bluesky on 15 February 2025 are

• Prospects for formalizing the theory of weak infinite-dimensional categories. ~ Emily Riehl. #ITP #LeanProver #Math

The readings shared in Bluesky on 14 February 2025 are

• Language models for verifiable mathematical automation (Interaction, integration, and autoformalization). ~ Qiaochu Jiang. #ITP #IsabelleHOL #LLMs #Autoformalization
• The Haskell Unfolder Episode 39: Deriving strategies). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Primos equidistantes. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 13 February 2025 are

• A Coq formalization of unification modulo exclusive-or. ~ Yichi Xu, Daniel J. Dougherty, Rose Bohrer. #ITP #Coq
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• A proof of Hilbert basis theorem and an extension to formal power series (in Isabelle/HOL). ~ Benjamin Puyobro, Benoît Ballenghien, Burkhart Wolff. #ITP #IsabelleHOL #Math
• Why Amazon is betting on 'automated reasoning' to reduce AI's hallucinations. ~ Belle Lin. #AI #LLMs #ITP
• On LLM-generated logic programs and their inference execution methods. ~ Paul Tarau. #LLMs #LogicProgramming #Prolog
• LP-LM: No hallucinations in question answering with logic programming. ~ Katherine Wu, Yanhong A. Liu. #LLMs #LogicProgramming #Prolog
• Improving autoformalization using type checking. ~ Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut. #Autoformalization #LLMs #ITP #LeanProver #Math
• What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper et als. #LLMs #Math
• A model for learning-curve estimation in efficient neural architecture search and its application in predictive health maintenance. ~ David Solís-Martín, Juan Galán-Páez, Joaquín Borrego-Díaz. #AI
• 50 years of programming language evolution through the software Heritage looking glass. ~ Adèle Desmazières, Roberto Di Cosmo, Valentin Lorentz. #Programming

The readings shared in Bluesky on 12 February 2025 are

• STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. #LLMs #ITP #LeanProver #IsabelleHOL
• Competitive programming with large reasoning models. ~ OpenAI. #LLMs #Programming

The readings shared in Bluesky on 11 February 2025 are

• Examining false positives under inference scaling for mathematical reasoning. ~ Yu Wang, Nan Yang, Liang Wang, Furu Wei. #LLMs #Math #Reasoning
• MATH-perturb: Benchmarking LLMs' math reasoning abilities against hard perturbations. ~ Kaixuan Huang et als. #LLMs #Math #Reasoning
• Embedding self-correction as an inherent ability in large language models for enhanced mathematical reasoning. ~ Kuofeng Gao, Huanqia Cai, Qingyao Shuai, Dihong Gong, Zhifeng Li. #LLMs #Math #Reasoning
• Streams in Common Lisp. ~ jcs. #CommonLisp
• Functional streams. ~ Atabey Kaygun. #CommonLisp
• Programming techniques: Generating prime numbers in Common Lisp. ~ Mitchell Chung. #CommonLisp #Math

The readings shared in Bluesky on 10 February 2025 are

• Feedback loops guide AI to proof checking. ~ Chris Edwards. #AI #ITP #LeanProver #Coq
• Verified certificates via SAT and computer algebra systems for the Ramsey R(3,8) and R(3,9) problems. ~ Zhengyu Li, Conor Duggan, Curtis Bright, Vijay Ganesh. #SAT #CAS
• Proving the coding interview: A benchmark for formally verified code generation. ~ Quinn Dougherty, Ronak Mehta. #AI #LLMs #Python #ITP
• ATLAS: Autoformalizing theorems through lifting, augmentation, and synthesis of data. ~ Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, Tao Luo. #LLMs #ITP #LeanProver #Math #Autoformalization
• Can Transformers reason logically? A study in SAT solving. ~ Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, Wenke Lee. #LLMs #Reasoning #SAT_Solvers
• #Exercitium: Anagramas. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 9 February 2025 are

• What is a quotient? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Systems correctness practices at AWS: Leveraging formal and semi-formal methods. ~ Marc Brooker, Ankush Desai. #FormalMethods #ITP #LeanProver
• Turner, Bird, Eratosthenes: An eternal burning thread. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• Chatbot software begins to face fundamental limitations. ~ Anil Ananthaswamy. #LLMs

The readings shared in Bluesky on 8 February 2025 are

• Verification of the CVM algorithm with a new recursive analysis technique. ~ Emin Karayel, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan, Seng Joe Watt. #ITP #IsabelleHOL
• Review of "Haskell in depth" by Vitaly Bragilevsky. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Cervantes, la cuadratura del círculo y la búsqueda del punto fijo. ~ Tomás Domínguez Benavides. #Matemáticas

The readings shared in Bluesky on 6 February 2025 are

• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #ITP #LeanProver #Math
• Simplifying formal proof-generating models with ChatGPT and basic searching techniques. ~ Sangjun Han, Taeil Hur, Youngmi Hur, Kathy Sangkyung Lee, Myungyoon Lee, Hyojae Lim. #LLMs #ChatGPT #ITP #LeanProver
• Elisp cheatsheet for Python programmers. ~ Charles Choi. #Python #Emacs #Elisp
• La categoría de conjuntos abstractos. ~ Luis Turcio. #CategoryTheory
• Exercitium: Diagonales principales. #Haskell #Python #CommonLisp #Math