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

The readings shared in Bluesky on 5 February 2025 are

• On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. #ITP #LeanProver #Mathlib
• Goedel-Prover: A new frontier in automated theorem proving. ~ Yong Lin et als. #LLMs #ITP #LeanProver
• New proofs probe the limits of mathematical truth. ~ Joseph Howlett. #Math

The readings shared in Bluesky on 4 February 2025 are

• Readings shared February 3, 2025. #ITP #LeanProver #IsabelleHOL #Haskell #Python #CommonLisp #Maxima #Math
• #Exercitium: Posiciones de las diagonales principales. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 3 February 2025 are

• A comprehensive survey of the Lean 4 theorem prover: Architecture, applications, and advances. ~ Xichen Tang. #ITP #LeanProver
• Differential privacy (in Isabelle/HOL). ~ Tetsuya Sato, Yasuhiko Minamide. #ITP #IsabelleHOL
• Differential privacy using quasi-Borel spaces. ~ Michikazu Hirata. #ITP #IsabelleHOL
• Maxima in the browser using Embedded Common Lisp on WASM. #Maxima #CoomonLisp #Math
• #Exercitium: La bandera tricolor. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 2 February 2025 are

• Transitive union-closed families (in Isabelle/HOL). ~ Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL
• Notes on Gödel’s and Scott’s variants of the ontological argument (Isabelle/HOL dataset). ~ Christoph Benzmüller, Dana Scott. #ITP #IsabelleHOL
• DeepSeek: A breakthrough in AI for math (and everything else). ~ David H Bailey. #DeepSeek #Math
• Some lessons from the OpenAI-FrontierMath debacle. ~ 7vik. #AI #Math
• Kazimierz Kuratowski, el talento y el compromiso de un matemático de Varsovia. ~ Marta Macho Stadler. #Math

The readings shared in Bluesky on 1 February 2025 are

• The continuous functional calculus in Lean. ~ Anatole Dedecker, Jireh Loreaux. #ITP #LeanProver #Math
• Formally verifying a transformation from MLTL formulas to regular expressions. ~ Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. #ITP #IsabelleHOL
• Formally verified binary-level pointer analysis. ~ Freek Verbeek, Ali Shokri, Daniel Engel, Binoy Ravindran. #ITP #IsabelleHOL
• A formal semantics of Core Erlang. ~ Ibrahim Abdelrahman Mohamedi. #ITP #IsabelleHOL #Erlang
• Context-dependent effects in guarded interaction trees. ~ Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal. #ITP #Coq
• Reasoning about weak isolation levels in separation logic. ~ Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal. #ITP #Coq
• Assisting mathematical formalization with a learning-based premise retriever. ~ Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu. #AI #LLMs #ITP #LeanProver #Math
• How to recognize artificial mathematical intelligence in theorem proving. ~ Markus Pantsar. #AI #Math #ITP
• LemmaHead: RAG assisted proof generation using large language models. ~ Tianbo Yang, Mingqi Yang, Hongyi Zhao, Tianshuo Yang. #AI #LLMs #ITP #LeanProver #Math
• Instantiation-based formalization of logical reasoning tasks using language models and logical solvers. ~ Mohammad Raza, Natasa Milic-Frayling. #LLMs #Reasoning #SMT #Z3
• From informal to formal (Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs). ~ Jialun Cao et als. #AI #LLMs #ITP #Coq #LeanProver #Math

The readings shared in Bluesky on 31 January 2025 are

• Solidifying modern SMT solvers. ~ Dominik Winterer. #SMT
• The Common Lisp Cheat Sheet. ~ Ashok Khanna. #CommonLisp
• #Exercitium: Ordenación por el máximo. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 30 January 2025 are

• Readings shared January 29, 2025. #ITP #IsabelleHOL
• A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abdulaziz, Arnd Hartmanns, Peter Lammich. #ITP #IsabelleHOL
• Analytic number theory exponent database. ~ Terence Tao et als. #ITP #LeanProver #Math
• Cellular methods in homotopy type theory. ~ Axel Ljungström, Loïc Pujet. #ITP #Agda

The readings shared in Bluesky on 29 January 2025 are

• Readings shared January 28, 2025. #ITP #LeanProver #Logic #Math #Prolog #LogicProgramming #Racket #FunctionalProgramming
• Mission-time linear temporal logic (in Isabelle/HOL). ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan. #ITP #IsabelleHOL
• Mission-time linear temporal logic to regular expressions (in Isabelle/HOL). ~ Zili Wang, Katherine Kosaian. #ITP #IsabelleHOL

The readings shared in Bluesky on 28 January 2025 are

• Readings shared January 26, 2025. #ITP #LeanProver #HOL_Light #Math
• The directed Van Kampen Theorem in Lean. ~ Henning Basoldm, Peter Bruin, Dominique Lawson. #ITP #LeanProver #Math
• The simplicity of Prolog. ~ Ties Westendorp. #Prolog #LogicProgramming
• Beautiful Racket (An introduction to language-oriented programming using Racket). ~ Matthew Butterick. #Racket #FunctionalProgramming
• New game posted on Lean Game Server: Reasoning. ~ Jad Abou Hawili./#/g/jadabouhawili/knightsandknaves-lean4game #ITP #LeanProver
• Lean for scientists and engineers. ~ Tyler Josephson. #ITP #LeanProver
• lean-mine: A collection of problems solved in Lean. #ITP #LeanProver #Math
• Baby Rudin project: An attempt to formalize every problem in Baby Rudin with natural language description. #ITP #LeanProver #Math
• Homo ratiocinator (Reckoning human). ~ Moshe Vardi. #Logic #Math

The readings shared in Bluesky on 26 January 2025 are

• Readings shared January 25, 2025. #ITP #Agda #Coq #Rocq #IsabelleHOL #Math #FunctionalProgramming #Haskell #JuliaLang
• Certified knowledge compilation with application to formally verified model counting. ~ Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule. #ITP #LeanProver
• Formalization of partial differential equations using HOL theorem proving. ~ Elif Deniz. #ITP #HOL_Light #Math
• Math Encounters: "You want proof? I'll give you proof! (Mathematical arguments from Euclid to Lean)". ~ Jeremy Avigad. #ITP #LeanProver #Math

The readings shared in Bluesky on 25 January 2025 are

• Readings shared January 24, 2025. #ITP #IsabelleHOL #Haskell #FunctionalProgramming #AI #LLMs #GenerativeAI #NeuroSymbolicAI
• Pinpointing the learning obstacles of an interactive theorem prover. ~ Sára Juhošová, Andy Zaidman, Jesper Cockx. #ITP #Agda
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• Combinatorial q-analogues (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Theta functions (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• The Rogers–Ramanujan identities (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Use monoids for construction. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Calculus for the modern engineer: Putting the joy back in learning advanced mathematics. ~ Jessy Grizzle. #Math #JuliaLang
• Calculus for the modern engineer (Textbook). ~ Jessy Grizzle et als. #Math #JuliaLang #LLMs

The readings shared in Bluesky on 24 January 2025 are

• Readings shared January 23, 2025. #ITP #IsabelleHOL #LeanProver #Python #Programming #Math #AI #LLMs
• Formally verified neurosymbolic trajectory learning via tensor-based linear temporal logic on finite traces. ~ Mark Chevallier, Filip Smola, Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL #NeuroSymbolicAI
• A new perspective on lenses. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Fast Haskell, Redux. ~ Jared Tobin. #Haskell #FunctionalProgramming
• Making my life easier with GADTs. ~ Lucas Escot. #Haskell #FunctionalProgramming
• Making my life harder with GADTs. Matt Parsons. #Haskell #FunctionalProgramming
• Making my life easier with two GADTs. ~ borar. #Haskell #FunctionalProgramming
• Modeling dataframes in Haskell using higher-kinded types. ~ Laurent P. René de Cotret. #Haskell #FunctionalProgramming
• Supercede’s house style for Haskell. ~ Jezen Thomas. #Haskell #FunctionalProgramming
• Tracing foreign function invocations. ~ Edsko de Vries, Zubin Duggal, Matthew Pickering. #Haskell #FunctionalProgramming
• What I've learned about writing AI apps so far. ~ Laurie Voss. #AI #LLMs
• AI mistakes are very different than human mistakes. ~ Bruce Schneier, Nathan E. Sanders. #AI #LLMs #GenerativeAI
• Cómo trabajar en el día a día con una IA y no morir en el intento. ~ @Alvy. #AI #LLMs
• DeepSeek: un nuevo modelo de IA especializado en razonamiento lógico, resolución de problemas y con licencia abierta MIT. No tiene nada que envidiar a los de OpenAI. ~ @Alvy. #AI #LLMs #DeepSeek
• DeepSeek: Into the unknown (Free access to DeepSeek-V3). #AI #LLMs #DeepSeek

The readings shared in Bluesky on 23 January 2025 are

• Readings shared January 22, 2025. #ITP #IsabelleHOL #Coq #Rocq #LeanProver #FunctionalProgramming #Haskell #Python #Math #AI
• Formalising an easy proof: Dirichlet's approximation theorem. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Hallucination detection and recovery: Initial experiment. ~ GasStationManager. #LLMs #ITP #LeanProver
• Advanced Python course. ~ Michael Foord. #Python #Programming
• ELIZA, la primera psicoterapeuta programada con IA, rescatada del olvido gracias a la arqueología informática. ~ @Alvy. #IA

The readings shared in Bluesky on 22 January 2025 are

• Readings shared January 21, 2025. #ITP #Lean4 #IsabelleHOL #Math #Prolog #LogicProgramming #AI #LLMs
• #Exercitium: Iguales al siguiente. #Haskell #Python #Matemáticas
• Formalising new mathematics in Isabelle: Diagonal Ramsey. ~ Lawrence C Paulson. #ITP #IsabelleHOL #Math
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• Advent of Code 2024: Haskell solution reflections for all 25 days. ~ Justin Le. #Haskell #FunctionalProgramming
• Scientific computing in Lean. ~ Tomas Skrivan. #ITP #LeanProver #Math
• Alpha-beta pruning explored, extended and verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
• Can a computer judge interestingness? ~ Michael Douglas. #AI #Math
• Formalising real algebraic geometry. ~ Artie Khovanov, Michael Nedzelsky, Wenda Li. #ITP #IsabelleHOL #Math
• The Mandelbrot set is connected (and other Lean explorations). ~ Geoffrey Irving. #ITP #LeanProver #Math
• Formalising theory of combinatorial optimisation. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL #Math
• Condensed type theory. ~ Johan Commelin. #ITP #LeanProver #Math
• How to prove Fermat's Last Theorem. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Structures in dependent type theory. ~ Jeremy Avigad. #ITP #LeanProver
• Comparative formalisation of Kneser's theorem. ~ Mantas Bakšys, Yaël Dillies. #ITP #IsabelleHOL #LeanProver #Math
• Lawvere theories in Lean. ~ Adam Topaz. #ITP #LeanProver #Math
• How to teach Fourier analysis to a large library of formalised mathematics. ~ Yaël Dillies. #ITP #LeanProver #Math
• Computer algebra and the formalisation of new mathematics. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• New Foundations: the story of a large formalisation project. ~ Sky Wilshaw. #ITP #LeanProver #Math
• The mathematics of Artificial Intelligence. ~ Gabriel Peyré. #AI #Math
• The Ramanujan Library (Automated discovery on the hypergraph of integer relations). ~ Itay Beit-Halachmi, Ido Kaminer. #Math #CompSci
• Wikenigma: An encyclopedia of unknowns. #Math #CompSci

The readings shared in Bluesky on 21 January 2025 are

• Readings shared January 20, 2025. #ITP #LeanProver #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #CommonLisp #JanetLang #AI #LLMs #Programming
• Proofs of the Praeclarum Theorema in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Describing domino tilings with Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Think of a number. ~ Kevin Buzzard. #AI #LLMs #Math
• Negatively associated random variables (in Isabelle/HOL). ~ Emin Karayel. #ITP #IsabelleHOL #Math
• Las series de Kempner, o qué ocurre cuando quito un dígito. ~ Miguel Ángel Morales. #Matemáticas

The readings shared in Bluesky on 20 January 2025 are

• Readings shared January 19, 2025. #ITP #LeanProver #FunctionalProgramming #Haskell #AI #LLMs
• #Exercitium: Primos consecutivos con media capicúa. #Haskell #Python #Matemáticas
• Classifying the groups of order pq in Lean. ~ Scott Harper, Peiran Wu. #ITP #LeanProver #Math
• Certifying rings of integers in number fields. ~ Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen. #ITP #LeanProver #Math
• Lean: First steps (22 - Recursion). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• [Lean: First steps (22 - Recursion) Video]. ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• Lean Together 2025. #ITP #LeanProver
• A formally verified IEEE 754 floating-point implementation of interval iteration for MDPs. ~ Bram Kohlen, Maximilian Schäffeler, Mohammad Abzulaziz, Arnd Hartmanns, Peter Lammich. #ITP #IsabelleHOL
• Interpreting Brainfuck in Haskell. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming
• Hasochism: The pleasure and pain of dependently typed Haskell programming. ~ Sam Lindley, Conor McBride. #Haskell #FunctionalProgramming
• An efficient algorithm for permutation iteration using a singly linked list. ~ Thomas Baruchel. #CommonLisp #Algorithms
• Janet: a functional and imperative programming language. #JanetLang #FunctionalProgramming
• Janet for mortals (a real book). ~ Ian Henry. #JanetLang #FunctionalProgramming
• Bauble: A playground for making 3D art with lisp and math. ~ Ian Henry et als. #JanetLang #FunctionalProgramming
• Building Bauble. ~ Ian Henry #JanetLang #FunctionalProgramming
• Awesome Janet: Curated list of libraries and tooling for the Janet programming language. ~ Matthew Carter. #JanetLang #FunctionalProgramming
• How developers interact with AI: A taxonomy of human-AI collaboration in software engineering. ~ Christoph Treude, Marco A. Gerosa. #AI #LLMs #Programming

The readings shared in Bluesky on 19 January 2025 are

• Readings shared January 18, 2025. #Haskell #Python #CommonLisp #ITP #Coq #Rocq #Logic #Math #AI #MachineLearning #LLMs
• A toy example of a verified compiler. ~ Marcus Rossel. #ITP #LeanProver
• A new perspective on lenses. ~ Sandy Maguire. #Haskell #FunctionalProgrammingo
• Foundations of Large Language Models. ~ Tong Xiao, Jingbo Zhu. #eBook #AI #LLMs
• Language models and structured data. ~ Mehwish Alam. #LLMs

The readings shared in Bluesky on 18 January 2025 are

• Readings shared January 17, 2025. #Haskell #Python #ITP #Coq #Rocq #LeanProver #Logic #Math #AI #LLMs #Reasoning
• #Exercitium: Mastermind. #Haskell #Python #Matemáticas
• Formal proofs in applied mathematics: A Coq formalization of simplicial Lagrange finite elements. ~ Houda Mouhcine. #ITP #Coq #Rocq #Math
• Neurosymbolic tools for effective coding and debugging. ~ Georgios Sakkas. #AI #MachineLearning #LLMs
• Iteration. ~ Joe Marshall. #CommonLisp
• Lisp tutorial. ~ Daniel Nussenbaum. #CommonLisp
• Release Common Lisp on your first day. ~ Dan's Musings. #CommonLisp
• Listopia: List manipulation library inspired by Haskell package Data.List. ~ Ito Dimercel. #CommonLisp #Haskell
• Lisp programming language (Full course for beginners). ~ Alberto Lerda. #CommonLisp
• Neuro symbolic reasoning and learning. ~ Paulo Shakarian, Chitta Baral, Gerardo I. Simari, Bowen Xi, Lahari Pokala. #Logic #AI #MachineLearning
• How I program with LLMs. ~ David Crawshaw. #LLMs #Programming

The readings shared in Bluesky on 17 January 2025 are

• Readings shared January 16, 2025. #ITP #LeanProver #Agda #Logic #Math #SAT #SMT #FunctionalProgramming #Haskell #Python #Matemáticas #AI #LLMs
• #Exercitium: Determinación de los elementos minimales. #Haskell #Python #Matemáticas
• Verified and optimized implementation of orthologic proof search. ~ Simon Guilloud, Clément Pit-Claudel. #ITP #Coq #Rocq #Logic
• Scaling mathlib: tooling and automation for an ever-growing mathematics library. ~ Michael Rothgang. #ITP #LeanProver
• Progress report on the Carleson Project. ~ Floris van Doorn. #ITP #LeanProver #Math
• Egg: An equality saturation tactic in Lean. ~ Marcus Rossel et als. #ITP #LeanProver
• lean-SMT. ~ Abdalrhman Mohamed. #ITP #LeanProver
• Toward functor quasi-categories in Lean. ~ Jack McKoen. #ITP #LeanProver
• Verified foundations for differential privacy. ~ Jean-Baptiste Tristan. #ITP #LeanProver
• Can AI models reason: Is data all you need? ~ Wayne Joubert. #AI #LLMs #Reasoning

The readings shared in Bluesky on 16 January 2025 are

• Readings shared January 15, 2025. #ITP #LeanProver #Logic #Math #CompSci #FunctionalProgramming #Haskell
• #Exercitium: Sucesión de números amigos. #Haskell #Python #Matemáticas
• #Exercitium: Suma de los números amigos menores que n. #Haskell #Python #Matemáticas
• Game "An introduction to constructive logic". ~ Mark Fischer et als./#/g/trequetrum/lean4game-logic #ITP #LeanProver #Logic
• Vertex algebras in Mathlib: coming soon? ~ Scott Carnahan. #ITP #LeanProver #Math
• Real world autoformalization. ~ Siddhartha Gadgil. #ITP #LeanProver #Math
• Building a formal verification framework for smart contracts. ~ Jakob von Raumer. #ITP #LeanProver
• The last mile: How do we make AI theorem provers which work in the real world for real users and not just on benchmarks? ~ Jason Rute. #ITP #LeanProver #AI
• Information theory in Lean: the DPI. ~ Lorenzo Luccioli. #ITP #LeanProver
• A nimble introduction to nimbers. ~ Violeta Hernández Palacios. #ITP #LeanProver #Math
• An agda2hs-compatible representation of exact real arithmetic. ~ Viktor Csimma. #ITP #Agda #FunctionalProgramming #Haskell
• Evaluating SAT and SMT solvers on large-scale sudoku puzzles. ~ Liam Davis, Tairan Ji. #SAT #SMT
• The Haskell Unfolder Episode 38: tasting and testing CUDA (map, fold, scan). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• U-MATH: A university-level benchmark for evaluating mathematical skills in LLMs. ~ Konstantin Chernyshev, Vitaliy Polshkov, Ekaterina Artemova, Alex Myasnikov, Vlad Stepanov, Alexei Miasnikov, Sergei Tilga. #LLMs #Math

The readings shared in Bluesky on 15 January 2025 are

• Readings shared January 14, 2025. #ITP #IsabelleHOL #Coq #Rocq #Haskell #FunctionalProgramming
• #Exercitium: Sucesión de números amigos. #Haskell #Matemáticas
• Root systems and root data in Mathlib. ~ Oliver Nash. #ITP #LeanProver
• An introduction to linters. ~ Damiano Testa. #ITP #LeanProver
• Efficient forward reasoning for Aesop. ~ Xavier Généreux, Jannis Limperg. #ITP #LeanProver
• The ∞-cosmos project: formalizing 1-, 2-, V-, and ∞-category theory. ~ Emily Riehl. #ITP #LeanProver
• Searching for proof improvements with tryAtEachStep. ~ David Renshaw. #ITP #LeanProver
• From Aristotle to the iPhone. ~ Moshe Vardi. #Logic #Math #CompSci

The readings shared in Bluesky on 14 January 2025 are

• Readings shared January 13, 2025. #ITP #Coq #Rocq #HOL4 #CommonLisp #Programming #Math
• An Isabelle/HOL framework for synthetic completeness proofs. ~ Asta Halkjær From. #ITP #IsabelleHOL
• An Isabelle formalization of co-rewrite pairs for non-reachability in term rewriting. ~ Dohan Kim, Teppei Saito, René Thiemann, Akihisa Yamada. #ITP #IsabelleHOL
• Formalizing simultaneous critical pairs for confluence of left-linear rewrite systems. ~ Christina Kirk, Aart Middeldorp. #ITP #IsabelleHOL
• Formalized Burrows-Wheeler transform. ~ Louis Cheung, Alistair Moffat, Christine Rizkallah. #ITP #IsabelleHOL
• Formalizing the one-way to hiding theorem. ~ Katharina Heidler, Dominique Unruh. #ITP #IsabelleHOL
• Further tackling Post correspondence problem and proof generation. ~ Akihiro Omori, Yasuhiko Minamide. #ITP #IsabelleHOL
• The formal theory of monads, univalently. ~ Niels van der Weide. #ITP #Coq #Rocq
• Hell (Haskell shell): Year in review. ~ Chris Done. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 13 January 2025 are

• Readings shared January 12, 2025. #ITP #Coq #Rocq #Math #HoTT #CommonLisp #LogicProgramming #Prolog #LPTP
• A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Rocq
• Coinductive proofs for temporal hyperliveness. ~ Arthur Correnson, Bernd Finkbeiner. #ITP #Coq #Rocq
• Reversible computation with stacks and "Reversible management of failures". ~ Matteo Palazzo, Luca Roversi. #ITP #Coq #Rocq
• Preservation of speculative constant-time by compilation. ~ Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte. #ITP #Coq #Rocq
• Proof recommendation system for the HOL4 theorem prover. ~ Nour Dekhil, Adnan Rashid, Sofiene Tahar. #ITP #HOL4
• The way of Lisp or the right thing. ~ Joe Marshall. #CommonLisp #Programming
• A road to Common Lisp. ~ Steve Losh (2018). #CommonLisp
• cl-digraph: an implementation of a mutable directed graph data structure for Common Lisp. ~ Steve Losh. #CommonLisp #Math

The readings shared in Bluesky on 12 January 2025 are

• Readings shared January 11, 2025. #ITP #LeanProver #Coq #Rocq #Agda #FunctionalProgramming #Haskell #Python #Math #CategoryTheory #ComputerSci #Education #GenAI
• Prouver que π est irrationnel avec MathComp-Analysis. ~ Reynald Affeldt. #ITP #Coq #Rocq #Math
• Reconciling impredicative axiom and universe. ~ Stefan Monnier. #ITP #Coq #Rocq #HoTT
• Vers une automatisation de la certification des propriétés de clôture pour Prolog. ~ Thierry Marianne, Fred Mesnard, Etienne Payet. #Prolog #LogicProgramming #LPTP
• Why I chose Common Lisp. ~ Dan's Musings. #CommonLisp
• Common Lisp community survey 2024 results. ~ Dan Haskin. #CommonLisp
• Common Lisp. #CommonLisp

The readings shared in Bluesky on 11 January 2025 are

• Readings shared January 10, 2025. #ITP #LeanProver #Logic #Math #Haskell #Python #ASP #LogicProgramming #AI #NeuroSymbolicAI #LLMs
• #Exercitium: Números amigos. #Haskell #Python #Matemáticas
• Categories and Haskell (An introduction to the mathematics behind modern functional programming). ~ Jan-Willem Buurlage. #CategoryTheory #Haskell #FunctionalProgramming
• LeanUniverse: A library for consistent and scalable Lean4 dataset management. ~ Aram H. Markosyan, Gabriel Synnaeve, Hugh Leather. #ITP #LeanProver
• Proxy-based small inversions: a case study in MetaCoq programming. ~ Pierre Corbineau, Basile Gros, Jean-François Monin. #ITP #Coq #Rocq
• On the correctness of Barron and Strachey’s cartesian product function. ~ Wouter Swierstra, Jason Hemann. #Haskell #FunctionalProgramming #ITP #Agda
• Alpha beta pruning with the selection monad. ~ Johannes Hartmann, Jeremy Gibbons. #Haskell #FunctionalProgramming
• Using GHC core to normalise student programs. ~ Matilda Blomqvist, Alex Gerdes. #Haskell #FunctionalProgramming
• Shallowly embedded functions. ~ Mart Lubbers, Pieter Koopman, Niek Janssen. #Haskell #FunctionalProgramming
• CoScheme: Compositional copatterns in Scheme. ~ Paul Downen, Adriano Corbelino II. #FunctionalProgramming
• Assessment in computer science education in the GenAI era (Prioritizing critical thinking over syntax mastery). ~ Orit Hazzan. #ComputerSci #Education #GenAI

The readings shared in Bluesky on 10 January 2025 are

• Readings shared January 9, 2025. #ITP #LeanProver #Logic #Math #FunctionalProgramming #Haskell #JavaScript #Python #AI #NeuralNetwork #ChatGPT
• #Exercitium: Máxima suma de caminos en un triángulo. #Haskell #Python #Matemáticas
• Teaching "Foundations of mathematics" with the LEAN theorem prover (Master's Thesis). #ITP #LeanProver #Logic #Math
• Learning to automatically solve logic grid puzzles. ~ Arindam Mitra, Chitta Baral (2015). #ASP #LogicProgramming
• Neuro-symbolic AI in 2024: A systematic review. ~ Brandon C. Colelough, William Regli. #AI #NeuroSymbolicAI
• Un comparador de modelos de Inteligencia Artificial. ~ @Alvy. #AI #LLMs

The readings shared in Bluesky on 9 January 2025 are

• Readings shared January 8, 2025. #ITP #IsabelleHOL #AI #MachineLearning #LLMs
• Teaching "Foundations of mathematics" with the LEAN theorem prover. ~ Mattia Luciano Bottoni, Alberto S. Cattaneo, Elif Sacikara. #ITP #LeanProver #Math
• Using a JavaScript component inside a Haskell application. ~ Mateusz Goślinowski. #Haskell #FunctionalProgramming #JavaScript
• Mathematics of neural networks (Lecture notes graduate course). ~ Bart M.N. Smets. #NeuralNetwork #Math
• Notes on mathematical logic (Vol. 1). ~ David W. Kueker. #Logic #Math
• Notes on mathematical logic (Vol. 2). ~ David W. Kueker. #Logic #Math
• ChatGPT: Cómo hacer (y mejorar) mi Trabajo de Fin de Carrera de la Universidad en un par de minutos. ~ Chema Alonso. #ChatGPT #Python #Programming

The readings shared in Bluesky on 8 January 2025 are

• Readings shared January 6, 2025. #ITP #IsabelleHOL #LeanProver #Lean4 #Agda #Coq #Rocq #HoTT #Math #AI #LLMs
• Notes on Gödel’s and Scott’s variants of the ontological argument (Isabelle/HOL dataset). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• Can AI models reason like a human? ~ Wayne Joubert. #AI #LLMs
• Artificial intelligence then and now (From engines of logic to engines of bullshit?). ~ Thomas Haigh. #AI #MachineLearning #LLMs

The readings shared in Bluesky on 6 January 2025 are

• Readings shared January 4, 2025. #ITP #IsabelleHOL #LeanProver #HOL_Light #Mizar #Math #Logic #Haskell #Python
• Computing huge Fibonacci numbers, by proof and by code. ~ Lawrence Paulson. #ITP #IsabelleHOL
• Lean: First steps (21 - Simple induction). ~ Tariq Rashid (@rzeta0@mastodon.social). #ITP #LeanProver #Lean4 #Math
• Mathematicians found – and fixed – an error in a 60-year-old proof. ~ Alex Wilkins.L#selection-733.0-733.66 #ITP #LeanProver #Math
• Large language models for mathematical analysis. ~ Ziye Chen, Hao Qi. #AI #LLMs #Math
• On planarity of graphs in homotopy type theory. ~ Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad. #ITP #Agda #HoTT
• Laws of quantum programming. ~ Mingsheng Ying, Li Zhou, Gilles Barthe. #ITP #Coq #Rocq #QuantumProgramming
• El libro recursivo de la recursividad. ~ @Alvy. #Programación

The readings shared in Bluesky on 3 January 2025 are

• Readings shared January 2, 2025. #Haskell #Python #Math
• #Exercitium: Mayor órbita de la sucesión de Collatz. #Haskell #Python #Matemáticas
• Proofs of the Nicomachus’s theorem in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Décomposition algébrique cylindrique en Coq/Rocq. ~ Quentin Vermande. #ITP #Coq #Rocq #Math
• Formalizing adhesive category theory in Rocq. ~ Samuel Arsac, Russell Harmer, Damien Pous. #ITP #Rocq
• Vérification de bout en bout d’une fonction de bibliothèque mathématique. ~ Paul Geneau de Lamarlière. #ITP #Coq #Rocq #Math
• Safe external calls from formally verified functional code: exiting the monad, and a BDD case study. ~ David Monniaux, Sylvain Boulmé. #ITP #Coq #Rocq
• Modular probabilistic programming with algebraic effects. ~ Oliver Goldstein, Ohad Kammar. #Haskell #FunctionalProgramming
• Parallel QuickHull algorithm in Haskell. ~ George Morgulis, Henry Lin. #Haskell #FunctionalProgramming
• Parallel SAT solver. ~ Yixuan Li, Jiaqian Li, Phoebe Wang. #Haskell #FunctionalProgramming
• Storable types: free, absorbing, custom. ~ Basile Clément, Camille Noûs, Gabriel Scherer. #OCaml #FunctionalProgramming
• Typechecking of overloading in programming languages and mechanized mathematics. ~ Arthur Charguéraud, Martin Bodin, Louis Riboulet. #OCaml #FunctionalProgramming
• Applying machine learning to number-theoretical data (A focus on class groups of imaginary quadratic fields). ~ Hugo Sträng. #AI #MachineLearning #Math

The readings shared in Bluesky on 3 January 2025 are

• Readings shared January 3, 2025. #ITP #Lean4 #IsabelleHOL #Coq #Rocq #Math #FunctionalProgramming #OCaml #Haskell #Python #AI #MachineLearning
• #Exercitium: Caminos en un triángulo. #Haskell #Python #Matemáticas
• Demostraciones con Isabelle/HOL del "Praeclarum theorema" de Leibniz. #ITP #IsabelleHOL #Logic
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als.. #ITP #LeanProver #Math
• Growing HOLMS, a HOL Light library for modal systems. ~ Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi, Leonardo Quartini. #ITP #HOL_Light #Logic
• Ascoli-Arzel`a theorem (Metric space version). ~ Keiichi Miyajima, Hiroshi Yamazaki. #ITP #Mizar #Math
• Universality of measure space. ~ Noboru Endou, Yasunari Shidama. #ITP #Mizar #Math
• Formalization of orthogonal complements of normed spaces. ~ Hiroyuki Okazaki. #ITP #Mizar #Math

The readings shared in Bluesky on 2 January 2025 are

• Readings shared January 1, 2025. #ITP #LeanProver #Lean4 #Mizar #Math #Haskell #Python
• #Exercitium: Ternas pitagóricas con suma dada. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 1 January 2025 are

• Readings shared December 31, 2024. #ITP #IsabelleHOL
• Lean: First steps (21 - Simple induction). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• Formal proof of transcendence of the number e (Part I). ~ Yasushige Watase. #ITP #Mizar #Math
• Formal proof of transcendence of the number e (Part II). ~ Yasushige Watase. #ITP #Mizar #Math
• #Exercitium: Suma de múltiplos de 3 o de 5. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 31 December 2024 are

• Readings shared December 30, 2024. #ITP #Coq #Rocq #FunctionalProgramming #Haskell #CommonLisp #EmacsLisp #Emacs #Logic #Math #CategoryTheory #AI
• A formal correctness proof of Edmonds' blossom shrinking algorithm. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL

The readings shared in Bluesky on 30 December 2024 are

• Readings shared December 29, 2024. #Haskell #Python #Math #AI #ITP
• Formal verification of a custom scheduling algorithm and specification of a Round-Robin implementation using Coq. ~ Christian Choa et als. #ITP #Coq #Rocq
• Formal verification of shortest job first scheduling algorithm in Coq. ~ Jian Lawrence Luteria et als. #ITP #Coq #Rocq
• Rocq prover: A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more. #ITP #Rocq
• Generalized Dijkstra in Haskell. ~ Lucas Escot. #Haskell #FunctionalProgramming
• Tutorial on good Lisp programming style. ~ Peter Norvig, Kent Pitman (1993). #CommonLisp #Programming
• Paradigms of artificial intelligence programming (Case studies in Common Lisp). ~ Peter Norvig. #eBook #AI #CommonLisp #Programming
• Emacs Lisp guide. ~ Chris Done. #Emacs #Lisp
• Category theory illustrated. ~ Jencel Panic. #CategoryTheory
• Mathematical expression and reasoning for computer science. ~ David Liu, Toniann Pitassi. #eBook #Logic #Math #CompSci
• How to use Emacs as a desktop environment in Linux with EXWM. ~ Ramces Red. #Emacs
• Historias de la IA: los autómatas. ~ Manuel de León. #IA #Autómatas

The readings shared in Bluesky on 29 December 2024 are

• Readings shared December 27, 2024. #ITP #IsabelleHOL #Math #Teaching #AI #LLMs #Emacs
• #Exercitium: Exponente en la factorización. #Haskell #Python #Matemáticas
• Machine-assisted proof. ~ Terence Tao. #Math #AI #ITP
• AMS Advisory Group on Artificial Intelligence. ~ Akshay Venkatesh, Mark C. Wilson. #Math #AI

The readings shared in Bluesky on 27 December 2024 are

• Readings shared December 26, 2024. #Haskell #Python #Math
• A generalization of the Cauchy–Davenport theorem (in Isabelle/HOL). ~ Mantas Bakšys. #ITP #IsabelleHOL #Math
• Formally verified approximate policy iteration. ~ Maximilian Schäffeler, Mohammad Abdulaziz. #ITP #IsabelleHOL
• Myths of mathematics teaching. ~ Daniel J. Velleman. #Math #Teaching
• Mathematics and machine creativity: A survey on bridging mathematics with AI. ~ Shizhe Liang, Wei Zhang, Tianyang Zhong. #AI #LLMs #Math
• AI: Beyond the headlines (The hype surrounding artificial intelligence has created misconceptions that may lead to missed opportunities). ~ Erdin Beshimov. #AI
• Dibujando figuras con Emacs. ~ Notxor. #Emacs

The readings shared in Bluesky on 26 December 2024 are

• Readings shared December 25, 2024. #Haskell #Python #Math #ITP #LeanProver #Lean4 #Lisp #Programming
• #Exercitium: Reconocimiento de potencias de 4. #Haskell #Python #Matemáticas

The readings shared in Bluesky on 25 December 2024 are

• Readings shared December 24, 2024. #ITP #Agda #Haskell #FunctionalProgramming #Haskell #Python #AI #LLMs #Math
• #Exercitium: El teorema de Navidad de Fermat. #Haskell #Python #Math
• Lean: First steps (20 - Contradictory cases). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• The bipolar Lisp programmer. ~ Mark Tarver. #Lisp #Programming

The readings shared in Bluesky on 24 December 2024 are

• Readings shared December 23, 2024. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization #Programming #JuliaLang #Python #MachineLearning #Golog #LogicProgramming
• #Exercitium: Producto de los elementos de la diagonal principal. #Haskell #Python #Matemáticas
• Teaching and learning proof in mathematics at university: new perspectives in education with proof assistants? ~ Cécile Ouvrier-Buffet. #ITP #Math #Education
• Data for mathematical copilots: Better ways of presenting proofs for machine learning. ~ Simon Frieder et als. #AI #LLMs #Math
• Compiling dependent type preconditions to runtime checks with Agda2Hs. ~ Jakob Naucke. #ITP #Agda #Haskell #FunctionalProgramming

The readings shared in Bluesky on 23 December 2024 are

• Readings shared December 21, 2024. #ITP #IsabelleHOL #Math #Haskell #FunctionalProgramming
• Formal mathematical reasoning: A new frontier in AI. ~ Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, Dawn Song. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization
• Can AI do maths yet? Thoughts from a mathematician. ~ Kevin Buzzard. #AI #ITP #Math
• The state of Julia for scientific machine learning. ~ Edward Berman, Jacob Ginesin. #Programming #JuliaLang #Python #MachineLearning
• LTLf synthesis on first-order agent programs in nondeterministic environments. ~ Till Hofmann, Jens Claßen. #AI #Golog #LogicProgramming

The readings shared in Bluesky on 21 December 2024 are

• Readings shared December 20, 2024. #ITP #Mizar #Math #Haskell #Python #AI
• Isabelle quick start guide. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• An imperative programmer tries to learn Haskell. ~ Thane Thomson. #Haskell #FunctionalProgramming
• Solving perfect numbers quickly with Haskell. ~ Andrew MacGillivray. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 20 December 2024 are

• Readings shared December 19, 2024. #ITP #IsabelleHOL #Mizar #Logic #Math #Haskell #FunctionalProgramming #LLMs
• #Exercitium: Reiteración de suma de consecutivos. #Haskell #Python #Matemáticas
• Formalize the octonions. ~ Alex Nelson (‪@pqnelson.bsky.social‬). #ITP #Mizar #Math
• Apriori knowledge in an era of computational opacity: The role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. #AI #Math

The readings shared in Bluesky on 19 December 2024 are

• Readings shared December 18, 2024. #ITP #Agda #Mizar #Math #AI
• A formalization of sequent calculus for classical implicational logic. ~ Frederik Krogsdal Jacobsen, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
• Elementary number theory problems (Part XV – Diophantine equations). ~ Karol Pąk, Artur Korniłowicz. #ITP #Mizar #Math
• Linear calculi: A comparison approach. ~ Ana Jorge Carvalho de Soares Almeida. #Haskell #FunctionalProgramming
• A survey of mathematical reasoning in the era of multimodal large language model: Benchmark, method & challenges. ~ Yibo Yan et als. #LLMs #Math #Reasoning

The readings shared in Bluesky on 18 December 2024 are

• Readings shared December 16, 2024. #ITP #LeanLang #Lean4 #Logic #SMT #Z3 # #Haskell #FunctionalProgramming #CommonLisp #Programming #AI #Math
• Intrinsic verification of parsers and formal grammar theory in dependent Lambek calculus. ~ Steven Schaefer et als. #ITP #Agda
• Proofs in the Wild. ~ Mike Dodds. #ITP #AI
• Loops in Mizar. ~ Alex Nelson (‪@pqnelson.bsky.social‬). #ITP #Mizar #Math
• Artificial intelligence: Principles and practice. ~ George F. Luger. #AI

The readings shared in Bluesky on 16 December 2024 are

• Readings shared December 15, 2024. #Haskell #FunctionalProgramming #CategoryTheory #AI #ITP #LeanProver #Math
• Lean: First steps (19 - Reductio ad absurdum). ~ Tariq Rashid. #ITP #LeanLang #Lean4 #Math
• Bottom-up computation using trees of sublists. ~ Shin-Cheng Mu. #Haskell #FunctionalProgramming
• 'Lean-style' tactics in Knuckledragger. ~ Philip Zucker. #Logic #SMT #Z3 #Python
• An example of goal-directed, calculational proof. ~ Roland Carl Backhouse, Walter Guttmann, Michael Winter. #Logic
• Pascal Costanza's Highly Opinionated Guide to Lisp. ~ Pascal Costanza. #CommonLisp #Programming
• Proposing and solving olympiad geometry with guided tree search. ~ Chi Zhang et als. #AI #Math

The readings shared in Bluesky on 15 December 2024 are

• Readings shared December 13, 2024. #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math
• Category theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. #Haskell #FunctionalProgramming #CategoryTheory
• The future of Math with o1 reasoning with Terence Tao, Mark Chen, and James Donovan. #AI #ITP #LeanProver #Math

The readings shared in Bluesky on 13 December 2024 are

• Readings shared December 12, 2024. #ITP #LeanLang #Lean4 #Math
• On extending incorrectness logic with backwards reasoning. ~ Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran. #ITP #IsabelleHOL
• Machine checked proofs and programs in algebraic combinatorics. ~ Florent Hivert. #ITP #Coq #Rocq #Math
• Univocity of intuitionistic and classical connectives. ~ Rodolfo C. Ertola-Biraben, Branden Fitelson. #ATP #Prover9 #Mace4 #Logic #Math

The readings shared in Bluesky on 12 December 2024 are

• Readings shared December 11, 2024. #ITP #IsabelleHOL #Logic #Math #SetTheory #Haskell #FunctionalProgramming
• Fermat’s Last Theorem — how it’s going. ~ Kevin Buzzard. #ITP #LeanLang #Lean4 #Math

The readings shared in Bluesky on 11 December 2024 are

• Readings shared December 10, 2024. #Haskell #Python #Math #Logic #SMT #Z3 #Python #LLMs #Prolog #LogicProgramming
• Isomorphic transfer infrastructure for nested types in Isabelle/HOL (Work in progress). ~ Gergely Buday, Andrei Popescu. #ITP #IsabelleHOL
• When is a call stack not a call stack? ~ Chris Smith. #Haskell #FunctionalProgramming
• Gödel's program in set theory. ~ Sandra Müller, Grigor Sargsyan. #Logic #Math #SetTheory
• Constructive theory of ordinals. ~ Thierry Coquand, Henri Lombardi, Stefan Neuwirth. #Logic #Math #SetTheory

The readings shared in Bluesky on 10 December 2024 are

• Readings shared December 9, 2024. #ITP #LeanLang #Lean4 #Haskell #FunctionalProgramming
• #Exercitium: Suma fila del triángulo de los impares. #Haskell #Python #Matemáticas
• Dyckhoff intuitionistic propositional prover. ~ Philip Zucker. #Logic #SMT #Z3 #Python
• Enhancing mathematical reasoning in LLMs with background operators. ~ Jiajun Chen, Yik-Cheung Tam. #LLMs #Prolog #LogicProgramming

The readings shared in Bluesky on 9 December 2024 are

• Readings shared December 8, 2024. #ITP #Agda #Coq #Haskell #FunctionalProgramming
• Information sign: Search and coupling (Metavariables, coupling, and formal proofs). ~ Leni Aniva. #ITP #LeanLang #Lean4
• Debugging your Haskell application with debuggable. ~ Edsko de Vries. #Haskell #FunctionalProgramming
• Myth and truth in Haskell asynchronous exceptions. ~ Kazu Yamamoto. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 8 December 2024 are

• Readings shared December 6, 2024. #Haskell #FunctionalProgramming #AI #LLMs #ITP #Math
• Gradual guarantee via step-indexed logical relations in Agda. ~ Jeremy G. Siek. #ITP #Agda
• Explicit weakening. ~ Philip Wadler. #ITP #Agda
• Formally verified hardening of C programs against hardware fault injection. ~ Basile Pesin, Sylvain Boulmé, David Monniaux, Marie-Laure Potet. #ITP #Coq
• Efficient, portable, census-polymorphic choreographic programming. ~ Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 6 December 2024 are

• Readings shared December 5, 2024. #ITP #LeanLang #Lean4 #Coq #Rocq #IsabelleHOL #Logic #Math #FunctionalProgramming #Haskell #OCaml #AI #LLMs
• You could have invented Fenwick trees. ~ Brent A. Yorgey. #Haskell #FunctionalProgramming
• AI for Math fund. ~ Terence Tao. #AI #ITP #Math
• (Re)imagining mathematics in a world of reasoning machines. ~ Akshay Venkatesh. #Math #ITP #AI
• On program synthesis and Large Language Models (Why it is unlikely new developments in machine intelligence will eventually make programming obsolete). ~ Hans Hüttel. #AI #LLMs #Programming
• Pourquoi existe-t-il de nombreux paradigmes de programmation? ~ Oscar Plaisant, Max Lemoine. #Programming #CompSci

The readings shared in Bluesky on 5 December 2024 are

• Readings shared December 4, 2024. #ITP #LeanLang #Logic #Math
• Lean: First steps (18 - Our Own Definition). ~ Tariq Rashid. #ITP #LeanLang #Lean4 #Math
• QuickSub: Efficient iso-recursive subtyping. ~ Litao Zhou, Bruno C.D.S. Oliveira. #ITP #Coq #Rocq
• Tail modulo cons, OCaml, and relational separation logic. ~ Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer. #ITP #Coq #OCaml #FunctionalProgramming
• The tensor product on Hilbert spaces (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL #Math
• The Haskell Unfolder Episode 37: Solving Advent of Code 2024 day 4. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• A Lean dataset for International Math Olympiad: Small steps towards writing math proofs for hard problems. ~ Roozbeh Yousefzadeh, Xuenan Cao. #LLMs #ITP #LeanLang #Lean4 #Math
• Amplifying human performance in combinatorial competitive programming. ~ Petar Veličković, Alex Vitvitskyi, Larisa Markeeva, Borja Ibarz, Lars Buesing, Matej Balog, Alexander Novikov. #AI #LLMs #Math
• OnlineProver: First experience with teaching formal proofs. ~ Joachim Kristensen et als. #Logic #Teaching

The readings shared in Bluesky on 4 December 2024 are

• Readings shared December 3, 2024. #ITP #LeanLang #IsabelleHOL #Coq #Rocq #Math #LLMs #ChatGPT
• Verified foundations for differential privacy. ~ Markus de Medeiros et als. #ITP #LeanLang
• Logic and linear algebra: An introduction. ~ Daniel Murfet. #Logic #Math

The readings shared in Bluesky on 3 December 2024 are

• Readings shared December 2, 2024. #ITP #LeanLang #Math #Calculemus #CategoryTheory #Math #Racket #FunctionalProgramming
• Lean: First steps (17 - Using our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• All your base are belong to U^s (Sort polymorphism for proof assistants). ~ Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter. #ITP #CoqLang #Rocq
• Mechanised safety verification for a distributed autonomous railway control system. ~ Robert Sachtleben, Anne Haxthausen, Jan Peleska. #ITP #IsabelleHOL
• The mathematician who—incidentally—helped mathematicians to stop worrying and love the computer. ~ Keith Devlin. #Math
• ChatGPT turns two: how the AI chatbot has changed scientists’ lives (How many researchers are using the AI tool? Nature gathers data and talks to members of the academic community). ~ Mariana Lenharo. #LLMs #ChatGPT