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

The readings shared in Bluesky on 2 December 2024 are

• Readings shared December 1, 2024. #ITP #IsabelleHOL #Math
• Proofs of "If uₙ tends to a y vₙ tends to b, then uₙvₙ tends to ab" in Lean4. #ITP #Lean4 #Math #Calculemus
• Lean: First steps (15 - Zero product). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (16 - Writing our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• Category theory in programming. ~ Noah Ma. #CategoryTheory #Math #Racket #FunctionalProgramming

The readings shared in Bluesky on 1 December 2024 are

• Readings shared November 30, 2024. #Lean4 #FunctionalProgramming
• The sum-of-squares function and Jacobi's two-square theorem (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math

The readings shared in Bluesky on 30 November 2024 are

• Readings shared November 29, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Calculemus #MachineLearning #LLMs #AIMO #AlphaProof #AlphaGeometry #Haskell #FunctionalProgramming #Programming #FormalVerification #Dafny
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto. #Lean4 #FunctionalProgramming

The readings shared in Bluesky on 29 November 2024 are

• Readings shared November 28, 2024. #ITP #IsabelleHOL #Logic #Math #Haskell #FunctionalProgramming
• Proof of "If the limit of the sequence u(n) is a and c ∈ ℝ, then the limit of u(n)c is ac" in Lean4. #ITP #Lean4 #Math #Calculemus
• Machine learning and mathematics (The twin catalysts poised to accelerate twenty-first century mathematics: formalisation and machine learning). ~ Harald Carlens. #Math #ITP #Lean4 #MachineLearning #LLMs #AIMO #AlphaProof #AlphaGeometry
• Deep embedding of intuitionistic linear logic. ~ Filip Smola, Jacques D. Fleuriot. #ITP #IsabelleHOL #Logic #Math
• Brillo: Painless 2D vector graphics, animations, and simulations powered by GLFW (Fork of gloss). ~ Adrian Sieber. #Haskell #FunctionalProgramming
• Effectiveness of Large Language Models to generate formally verified C code. ~ Merlijn Sevenhuijsen. #LLMs #Programming #FormalVerification
• dafny-annotator: AI-assisted verification of Dafny programs. ~ Gabriel Poesia, Chloe Loughridge, Nada Amin. #LLMs #Dafny #FormalVerification

The readings shared in Bluesky on 28 November 2024 are

• Readings shared November 27, 2024. #Haskell #FunctionalProgramming #AI #MachineLearning #Math
• Semantics for linear-time temporal logic with finite observations. ~ Rayhana Amjad, Rob van Glabbeek, Liam O'Connor. #ITP #IsabelleHOL #Logic #Math
• Competitive Programming in Haskell: stacks, queues, and monoidal sliding windows. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 27 November 2024 are

• Readings shared November 26, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Prolog #LogicProgramming #Z3 #SMT #AI #Education
• Haskell: A great procedural language. ~ kqr. #Haskell #FunctionalProgramming
• The ultimate guide to Haskell Strings. ~ Julian Ospald. #Haskell #FunctionalProgramming
• Linear algebra done right. ~ Sheldon Axler. #eBook #Math
• What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper, Anibal M. Medina-Mardones, Bartłomiej Lewandowski, Angus Gruen, Piotr Kucharski, Sergei Gukov. #AI #MachineLearning #Math

The readings shared in Mastodon on 26 November 2024 are

• Readings shared November 25, 2024. #ITP #Lean4 #Rocq #FunctionalProgramming #CommonLisp
• Impossibility of the dissection of a cube (in Isabelle/HOL). ~ Thomas Holme Surlykke. #ITP #IsabelleHOL #Math
• Two theorems on hermitian matrices (in Isabelle/HOL). ~ Sage Binder, Zilin Jiang. #ITP #IsabelleHOL #Math
• Ground lambda Prolog. ~ Philip Zucker. #Prolog #LogicProgramming #Z3 #SMT
• In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl. ~ Stefan Neuwirth, Henri Lombardi, Thierry Coquand. #Logic #Math
• Grupos y capturas reemplazando texto con expresiones regulares. ~ Fernando Briano. #Emacs
• Lean: First steps (18 - Our own definition). ~ Tariq Rashid. #ITP #Lean4 #Math
• IA Generativa: Estrategias de uso para docentes desde infantil a bachillerato. ~ Pablo Haya. #AI #Education

The readings shared in Mastodon on 25 November 2024 are

• Readings shared November 24, 2024. #ITP #Lean4 #Math #AI #LLMs #Programming #Education
• Cryptography experiments in Lean 4: SHA-3 implementation. ~ Gérald Doussot. #ITP #Lean4 #FunctionalProgramming
• Scaling up mechanized proof automation for small-step semantics. ~ Sandrine Blazy, Alain Delaët, Denis Merigoux. #ITP #Rocq
• Counting connected components of a graph. ~ Atabey Kaygun. #FunctionalProgramming #CommonLisp

The readings shared in Mastodon on 24 November 2024 are

• Readings shared November 23, 2024. #Math #SetTheory #Bluesky
• Lean: First steps (Appendix B - Libraries). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (17 - Using our own lemma). ~ Tariq Rashid. #ITP #Lean4 #Math
• Papers with computer-checked proofs. ~ Daniel J. Bernstein. #ITP
• Does AI mean the end of teaching programming? ~ Alfred Thompson. #AI #Programming #Education
• Are Large Language Models memorizing bug benchmarks? ~ Daniel Ramos, Claudia Mamede, Kush Jain, Paulo Canelas, Catarina Gamboa, Claire Le Goues. #LLMs #Programming

The readings shared in Mastodon on 23 November 2024 are

• Readings shared November 22, 2024. #Logic #Math #FCA #ConExp #AI
• 'A place of joy': why scientists are joining the rush to Bluesky. ~ Smriti Mallapaty. #Bluesky
• Axiomatic set theory (Version of 23 November 2024). ~ Tom Leinster. #Math #SetTheory

The readings shared in Mastodon on 22 November 2024 are

• Readings shared November 21, 2024. #ITP #Lean4 #Coq #Haskell #OCaml #FunctionalProgramming #ITP #Prolog #LogicProgramming #Math
• The elementary theory of free Steiner triple systems. ~ Silvia Barbina, Enrique Casanovas. #Logic #Math
• FCA (Formal Concept Analysis) using the Concept Explorer in 2024. ~ Edith Vargas-GarcÍa, Andreas Wachtel. #FCA #ConExp
• Conferencia Leonardo Torres Quevedo: ¿Puede pensar una máquina? ~ Francisco A. González Redondo y Alfonso Hernando González. #AI

The readings shared in Mastodon on 21 November 2024 are

• Readings shared November 20, 2024. #ITP #Lean4 #Math #AI
• Lean4 and the Curry-Howard isomorphism. ~ Luis Wirth. #ITP #Lean4
• Repository for the conference "Lean For The Curious Mathematician 2024". #ITP #Lean4 #Math
• The denotational semantics of SSA. ~ Jad Elkhaleq Ghalayini, Neel Krishnaswami. #ITP #Lean4
• 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
• Scientific computing with confidence using typed dimensions. ~ Laurent P. René de Cotret. #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 36: Concurrency and the FFI. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• The Prolog Trinity ecosystem (Extracts from the current manuscripts). ~ Torbjörn Lager. #Prolog #LogicProgramming
• Apuntes de programación lógica (Hasta Prolog y más allá). ~ Joaquín Arias. #Prolog #LogicProgramming

The readings shared in Mastodon on 20 November 2024 are

• Readings shared November 19, 2024. #ITP #Lean4 #Math #Haskell #FunctionalProgramming
• Anatomy of a formal proof. ~ Jeremy Avigad, Johan Commelin, Heather Macbeth, Adam Topaz. #ITP #Lean4 #Math
• A course of Algebra (Part I). ~ Aleksandr Aleksandrovich Zykov. #Math
• El aprendizaje automático ayuda a atacar problemas matemáticos clásicos. ~ Juanjo Rué y Ágata A. Timón. #AI #Math

The readings shared in Mastodon on 19 November 2024 are

• Readings shared November 18, 2024. #LLMs #Math #Reasoning #Logic #TypeTheory
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #Lean4 #Math
• Competitive programming in Haskell: Union-Find, part II. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 18 November 2024 are

• Readings shared November 17, 2024. #ITP #Coq #Haskell #CommonLisp #FunctionalProgramming #Python #Programming #CategoryTheory
• Do Large Language Models truly grasp mathematics? An empirical exploration from cognitive psychology. ~ Wei Xie, Shuoyoucheng Ma, Zhenhua Wang, Enze Wang, Kai Chen, Xiaobing Sun, Baosheng Wang. #LLMs #Math #Reasoning
• Monoid theory in Alonzo: A little theories formalization in simple type theory. ~ William M. Farmer, Dennis Y. Zvigelsky. #Logic #Math #TypeTheory

The readings shared in Mastodon on 17 November 2024 are

• Readings shared November 16, 2024. #ITP #Lean4 #FunctionalProgramming #Math #AI #LLMs #Git #GitHub
• Designing proof deautomation for Coq. ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Andrew Head, Benjamin C. Pierce. #ITP #Coq
• Type-checking and type-inference. ~ René Thiemann. #Haskell #FunctionalProgramming
• Type-inference in Haskell, kinds and explicit foralls. ~ René Thiemann. #Haskell #FunctionalProgramming
• Functors, record syntax, case study: a simple parser. ~ René Thiemann. #Haskell #FunctionalProgramming
• Monads in general, state monads. ~ René Thiemann. #Haskell #FunctionalProgramming
• Evaluation of monadic code, example: Tseitin, error monads. ~ René Thiemann. #Haskell #FunctionalProgramming
• Parsing in general, Parsec. ~ René Thiemann. #Haskell #FunctionalProgramming
• Number of isomorphism classes of ternary trees. ~ Atabey Kaygun. #FunctionalProgramming #CommonLisp
• Sieves and sheaves. ~ Bartosz Milewski. #CategoryTheory
• Python is no more the king of data science (5 reasons why Python is losing its crown). ~ Abdur Rahman. #Python #Programming

The readings shared in Mastodon on 16 November 2024 are

• Readings shared November 15, 2024. #ITP #LeanProver #Math #SetTheory #Haskell #FunctionalProgramming #AI #LLMs
• Code with proofs: The Arena. #ITP #Lean4 #FunctionalProgramming
• The Turing Test and our shifting conceptions of intelligence. ~ Melanie Mitchell. #AI
• Debates on the nature of artificial general intelligence. ~ Melanie Mitchell. #AI
• Large Language Models. ~ Melanie Mitchell. #AI #LLMs
• GitHub for mathematicians. ~ Steven Clontz. #Git #GitHub
• Code4math: Consortium of Digital Ecosystems for Mathematics. #Math

The readings shared in Mastodon on 15 November 2024 are

• Readings shared November 14, 2024. #ITP #LeanProver #Coq #ATP #Logic #Math #Haskell #FunctionalProgramming #FormalMethods #CompSci #Education #RustLang #AI #LLMs
• Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
• The Haskell inlining and specialization FAQ. ~ Gabriella Gonzalez. #Haskell #FunctionalProgramming
• Axiomatic set theory (Version of 9 November 2024). ~ Tom Leinster. #Math #SetTheory
• The metaphors of artificial intelligence. ~ Melanie Mitchell. #AI #LLMs

The readings shared in Mastodon on 14 November 2024 are

• Readings shared November 13, 2024. #ITP #Lean4 #Math #Physics #ATP #SAT_Solvers
• VEL: A formally verified reasoner for ℰℒ++ description logic. ~ Atalay Mert Ileri1, Hande Küçük McGinty. #ITP #Coq #Logic
• La formalización automatizada de las matemática: Una historia de cómo la necesidad hizo la virtud. ~ David de Frutos Escrig. #ITP #LeanProver #Math
• Debugging Haskell type errors. ~ Tikhon Jelvis. #Haskell #FunctionalProgramming
• The role of formal methods in computer science education. ~ Maurice ter Beek, Manfred Broy, Brijesh Dongol. #FormalMethods #CompSci #Education
• Resolution prover in Rust. ~ Wanda Rosmus. #Logic #ATP #RustLang
• AI’s math problem: FrontierMath benchmark shows how far technology still has to go. ~ Michael Nuñez. #AI #Math
• A holistic and critical look at language agents. ~ Yu Su. #AI #LLMs

The readings shared in Mastodon on 13 November 2024 are

• Readings shared November 12, 2024. #ITP #LeanProver #LLMs #Emacs
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson, Riccardo Brasca, Nikolas Kuhn, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio, Adam Topaz. #ITP #Lean4 #Math
• Formalization of physics index notation in Lean 4. ~ Joseph Tooby-Smith. #ITP #Lean4 #Math #Physics
• How to discover short, shorter, and the shortest proofs of unsatisfiability: A branch-and-bound approach for resolution proof length minimization. ~ Konstantin Sidorov, Koos van der Linden, Gonçalo Homem de Almeida Correia, Mathijs de Weerdt, Emir Demirović. #ATP #SAT_Solvers

The readings shared in Mastodon on 12 November 2024 are

• Readings shared November 11, 2024. #ITP #LeanProver #Logic #Math #LLMs
• Benchmarking automated theorem proving with Large Language Models. ~ Vanessa Lama, Catherine Ma, Tirthankar Ghosal. #ITP #LeanProver #LLMs
• BC-Prover: Backward chaining prover for formal theorem proving. ~ Yuhang He et als. #ITP #LeanProver #LLMs
• Programación literaria en Emacs (1ª parte). ~ Nyan Max. #Emacs

The readings shared in Mastodon on 11 November 2024 are

• Readings shared November 10, 2024. #ITP #Lean4 #Logic #Math #TFM
• NL²PS: A natural language to Lean proofs system. ~ Yifan Luo, Kangping Xu.V#discussion #ITP #LeanProver #LLMs
• VCVio: A formally verified forking lemma and Fiat-Shamir transform, via a flexible and expressive oracle representation. ~ Devon Tuma, Nicholas Hopper. #ITP #LeanProver
• The art of proof (Basic training for deeper mathematics). ~ Matthias Beck, Ross Geoghegan. #Logic #Math

The readings shared in Mastodon on 10 November 2024 are

• Readings shared November 9, 2024. #ITP #Agda #Logic #Math #SetTheory #AI #MachineLearning
• #Calculemus: Proofs with Lean4 of "If u(n) tends to a, then 7u(n) tends to 7a". #ITP #Lean4 #Math
• An introduction to mathematical proof. ~ Seçkin Demirbaş, Andrew Rechnitzer, Hannah Kohut. #Logic #Math
• Los números metálicos. ~ Marta Macho Stadler. #Math
• Los números vistos como bosques. ~ Marta Macho Stadler. #Math
• Problemas de competición sobre combinatoria. ~ Araceli Arjona Muñoz. #TFM #Math
• Problemas de probabilidad de Olimpiada Matemática. ~ Eduardo Cebrián García. #TFM #Matemáticas
• Análisis y resolución de problemas sobre desigualdades numéricas en la preparación de la Olimpiada de Matemáticas. ~ Sara Amaro Serrano. #TFM #Matemáticas
• Análisis y resolución de problemas sobre teoría de juegos. ~ Celia García Ruiz. #TFM #Matemáticas
• Invariantes en la resolución de problemas. ~ José Félix Sánchez Martínez. #TFM #Matemáticas
• Estudio y discusión sobre problemas de Olimpíada: Aritmética. ~ Inmaculada Perálvarez Bermúdez. #TFM #Matemáticas
• Problemas de olimpiadas sobre números complejos. ~ Paola Posadas Prados. #TFM #Matemáticas
• Estudio y discusión sobre problemas de Olimpíada: Ecuaciones diofánticas. ~ Antonio Manuel Ortega Torres. #TFM #Matemáticas
• Estudio y discusión sobre problemas de Olimpíada: Desigualdades. ~ Iván Valero Terrón. #TFM #Matemáticas
• Problemas de Olimpíadas Matemáticas sobre Probabilidad. ~ Marta Fernández Rodríguez. #TFM #Matemáticas
• Problemas y aplicaciones de sucesiones recurrentes. ~ Carlos Cervera Zafra. #TFM #Matemáticas
• Estudio de problemas sobre ecuaciones funcionales en el nivel de Olimpiadas Matemáticas. ~ Luis Castro Castro. #TFM #Matemáticas
• Números curiosos. ~ Pascual Jara. #Matemáticas
• Paradojas. ~ Pascual Jara Martínez. #Lógica #Matemáticas
• Sucesiones recurrentes. ~ Pascual Jara Martínez. #Matemáticas

The readings shared in Mastodon on 9 November 2024 are

• Readings shared November 8, 2024. #Math #AI #LLMs #Math #Reasoning
• Formalising graph algorithms with coinduction. ~ Donnacha Oisín Kidney, Nicolas Wu. #ITP #Agda #Math
• Axiomatic set theory (Version of 3 November 2024). ~ Tom Leinster. #Math #SetTheory
• Introduction to mathematical proofs. ~ Shay Fuchs. #Logic #Math
• On the relevance of logic for AI, and the promise of neuro-symbolic learning. ~ Vaishak Belle. #Logic #AI #MachineLearning

The readings shared in Mastodon on 8 November 2024 are

• Readings shared November 7, 2024. #ITP #Coq #Lean4 #Agda #Logic #Math #Haskell #FunctionalProgramming #LLMs #ChatGPT #AI #Programming #Education
• Applications of graph theory. ~ Ashay Dharwadker, Shariefuddin Pirzada. #Math
• FrontierMath: A benchmark for evaluating advanced mathematical reasoning in AI. ~ Elliot Glazer et als. #AI #Math #Reasoning
• Benchmarking Large Language Models with integer sequence generation tasks. ~ Daniel O'Malley, Manish Bhattarai, Javier Santos. #AI #LLMs #Math

The readings shared in Mastodon on 7 November 2024 are

• Unification in matching logic — revisited. ~ Ádám Kurucz, Péter Bereczky, Dániel Horpácsi. #ITP #Coq
• Grupos en Lean. ~ Luis Turcio. #ITP #Lean4 #Math
• The Haskell Unfolder Episode 35: Distributive and representable functors. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• What can we mean? (on practices, norms and pluralisms). ~ Greg Restall. #ITP #Agda #Lean #Logic #Math
• Learning rules explaining interactive theorem proving tactic prediction. ~ Liao Zhang, David M. Cerna, Cezary Kaliszyk. #ILP #ITP #Coq
• Next-token prediction task assumes optimal data ordering for LLM training in proof generation. ~ Chenyang An et als. #LLMs #ITP #LeanProver
• ChatGPT as tutor? A case study on competitive programming. ~ Juuso Rytilahti, Erno Lokkila. #ChatGPT #AI #Programming #Education

The readings shared in Mastodon on 5 November 2024 are

• Readings shared November 4, 2024. #ITP #Lean4 #Math
• Functors to Monads: A story of shapes. ~ Justin Lê. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 4 November 2024 are

• Readings shared November 3, 2024. #Haskell #FunctionalProgramming
• Lean: First steps (14 - Disequality again)​ (Video). ~ Tariq Rashid. #ITP #Lean4 #Math

The readings shared in Mastodon on 3 November 2024 are

• Readings shared November 2, 2024. #ITP #LeanProver #IsabelleHOL #Coq #Math #SetTheory #CategoryTheory #AI #LLMs #Autoformalization
• Competitive programming in Haskell: Union-find. ~ Brent Yorgey. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 2 November 2024 are

• Readings shared November 1, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math #Haskell #FunctionalProgramming #Autoformalization #LLMs
• The future of Mathematics in a world of machines. ~ Simone Severini. #Math #ITP #LeanProver #AI #LLMs #Autoformalization
• AIPS: An Olympiad-level AI system for algebraic inequalities. #LLMs #ITP #Lean4 #Math
• Proving the existence of stable assignments in democratic forking using Isabelle/HOL. ~ Jan-Georg Smaus. #ITP #IsabelleHOL
• Verified parser- and printer-combinator bidefinition in the Isabelle proof assistant. ~ Matthias Sleurink. #ITP #IsabelleHOL
• The Boustrophedon transform, the Entringer numbers, and related sequences (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Completeness of asynchronous session tree subtyping in Coq. ~ Burak Ekici, Nobuko Yoshida. #ITP #Coq
• Axiomatic set theory (Version of 31 October 2024). ~ Tom Leinster. #Math #SetTheory
• Basic category theory. ~ Tom Leinster. #Math #CategoryTheory
• Computational thinking: The idea that lived. ~ Shuchi Grover. #Education #Programming

The readings shared in Mastodon on 1 November 2024 are

• Readings shared October 31, 2024. #ITP #IsabelleHOL #Lean4 #Coq #Math #GenerativeAI
• Intuitionistic propositional logic in Lean. ~ Dafina Trufaş. #ITP #Lean4 #Logic #Math
• Cobblestone: Iterative automation for formal verification. ~ Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First. #ITP #Coq #LLMs
• Going REPLing with Haskeline. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming
• Proving Olympiad algebraic inequalities without human demonstrations. ~ Chenrui Wei, Mengzhou Sun, Wei Wang. #LLMs #ITP #Math
• Autoformalize mathematical statements by symbolic equivalence and semantic consistency. ~ Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, Xiaoxing Ma. #Autoformalization #LLMs #IsabelleHOL #Math

The readings shared in Mastodon on 31 October 2024 are

• Readings shared October 30, 2024. #ITP #Lean4 #IsabelleHOL #Math #ITP #Prolog #ASP #LogicProgramming #LambdaCalculus #AI #LLMs
• Lean: First steps (14 - Disequality again)​. ~ Tariq Rashid. #ITP #Lean4 #Math
• Babai’s nearest plane algorithm (in Isabelle/HOL). ~ Eric Ren, Sage Binder, Katherine Kosaian. #ITP #IsabelleHOL #Math
• Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. ~ Julien Narboux, Viviane Durand-Guerrier. #ITP #Coq #Math #Education
• Generative AI as an icebreaker to help us accept other ways of thinking. ~ Berry Billingsley, Ted Selker. #GenerativeAI
• The secret of Ramsey numbers (A new order forms out of randomness). ~ Chris Edwards. #Math #CompSci
• Ética, pensamiento crítico y responsabilidad en el uso de la IA en trabajos académicos (presentación). ~ Lluís Codina. #GenerativeAI #Education

The readings shared in Mastodon on 30 October 2024 are

• Readings shared October 29, 2024. #AI #XAI #LLMs #Logic #Reasoning #ASP #LogicProgramming
• Lean 4 tactic cheatsheet (October 29, 2024). ~ Floris van Doorn. #ITP #Lean4
• AI and Mathematics. ~ Terence Tao. #AI #Math #ITP #Lean4
• A formal characterization of discrete condensed objects. ~ Dagur Asgeirsson. #ITP #Lean4 #Math
• Minimal, maximal, least, and greatest elements w.r.t. restricted ordering (in Isabelle/HOL). ~ Martin Desharnais. #ITP #IsabelleHOL
• Programming with Math: The lambda calculus. #LambdaCalculus
• Prolog, Datalog, languages, resources, and beyond! #Prolog #ASP #LogicProgramming
• Combining logic with Large Language Models for automatic debugging and repair of ASP programs. ~ Ricardo Brancas, Vasco Manquinho, Ruben Martins. #ASP #LogicProgramming #LLMs

The readings shared in Mastodon on 29 October 2024 are

• Readings shared October 28, 2024. #ITP #Lean4 #Coq #Math #LLMs
• Tools are all you need. ~ Henry Kautz. #AI #LLMs #Logic #Reasoning
• Logic in the age of AI. ~ Yuri Gurevich. #Logic #AI
• Rigorous language models for trustworthy AI. ~ Yanhong A. Liu. #AI #LLMs #Logic #Reasoning
• Harnessing ASP and its extensions: Recent applications and role in Trustworthy AI. ~ Giuseppe Mazzotta, Francesco Ricca. #AI #ASP #LogicProgramming
• Advancements in xASP, an XAI system for Answer Set Programming. ~ Mario Alviano, Ly Ly Trieu, Tran Son, Marcello Balduccini. #ASP #XAI
• Logic-based explainability: Past, present & future. ~ Joao Marques-Silva. #XAI #Logic
• A case study on TSP: What to optimize and how? ~ Martin Gebser. #ASP #LogicProgramming
• Integrating reasoning systems for trustworthy AI (Proceedings of the 4th Workshop on Logic and Practice of Programming (LPOP)). ~ Anil Nerode, Yanhong A. Liu (eds.) #Logic #LogicProgramming #AI
• Combining LLM code generation with formal specifications and reactive program synthesis. ~ William Murphy, Nikolaus Holzer, Feitong Qiao, Leyi Cui, Raven Rothkopf, Nathan Koenig, Mark Santolucito. #LLMs
• Keynote presentation by Hal Abelson and Gerald Sussman at the fourteenth RacketCon: "Teaching people thinking: programming and powerful ideas" and "From computational thinking to computational action". #CompSci
• Introduction to Git and GitHub for Python developers. ~ Jim Anderson. #Git

The readings shared in Mastodon on 28 October 2024 are

• Readings shared October 27, 2024. #ITP #Coq #Haskell #OCaml #Math #SetTheory #ChatGPT
• Lean: First steps (12 - Odd & Even). ~ Tariq Rashid #ITP #Lean4 #Math
• Lean: First steps (13 - Disequality). ~ Tariq Rashid #ITP #Lean4 #Math
• Prime number theorem and more. ~ Alex Kontorovich et als. #ITP #LeanProver #Math
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov, Anton Podkopaev. #ITP #Coq #LLMs

The readings shared in Mastodon on 27 October 2024 are

• Readings shared October 26, 2024. #ILP #LogicProgramming #AI #MachineLearning
• Double auctions: Formalization and automated checkers. ~ Mohit Garg, N. Raja, Suneel Sarswat, Abhishek Kr Singh. #ITP #Coq #Haskell #OCaml
• Axiomatic set theory (Version of 26 October 2024). ~ Tom Leinster. #Math #SetTheory
• ChatGPT’s performance in university admissions tests in mathematics. ~ Angel Udias et als. #ChatGPT #Math

The readings shared in Mastodon on 26 October 2024 are

• Readings shared October 25, 2024. #ITP #LeanProver #IsabelleHOL #Math #Prolog #ASP #CLP #LogicProgramming #LLMs #GenerativeAI #Rust #Verification
• Neuro-symbolic agent with ASP for robust exception learning in text-based games. ~ Kinjal Basu. #ILP #LogicProgramming #AI #MachineLearning
• An AI learning hierarchy. ~ Peter J. Denning, Ted G. Lewis. #AI

The readings shared in Mastodon on 25 October 2024 are

• A formal characterization of discrete condensed objects. ~ Dagur Asgeirsson. #ITP #LeanProver #Math
• Formalization of differential privacy in Isabelle/HOL. ~ Tetsuya Sato, Yasuhiko Minamide. #ITP #IsabelleHOL
• A formalization of Borel determinacy in Lean. ~ #ITP #LeanProver #Math
• Brownian motion in Isabelle/HOL. ~ Christian Pardillo Laursen, Simon Foster, Mark Post. #ITP #IsabelleHOL
• Teaching pure LP with Prolog and a fair search rule. ~ Manuel V. Hermenegildo, Jose F. Morales, Pedro Lopez-Garcia. #Prolog #LogicProgramming
• General game playing - Killer app for logic programming. ~ Michael Genesereth. #Prolog #LogicProgramming
• Teaching Prolog through grammars. ~ David S. Warren. #Prolog #LogicProgramming
• From logic programming to programming in Logica: A first-course in declarative data science & engineering. ~ Evgeny Skvortsov, Yilin Xia, Shawn Bowers & Bertram Ludäscher. #LogicProgramming #Logica
• Logica: language of Big Data. ~ Evgeny Skvortsov et als. #LogicProgramming #Logica
• Democratising access to logic programming: A Web application design tool for querying Prolog code. ~ Santiago Andrés Villarroel, Christian Nelson Gimenez, Jorge Pablo Rodríguez, Laura Andrea Cecchi. #Prolog #LogicProgramming
• Computational thinking with logic programming. ~ Gopal Gupta, Elmer Salazar, Joaquín Arias. #ASP #LogicProgramming
• Generative logic: Teaching Prolog as Generative AI in art and design. ~ Christian Jendreiko. #Prolog #LogicProgramming #GenerativeAI
• Controlled natural language models. ~ Jacinto A. Dávila Quintero. #LLMs #Prolog #LogicProgramming
• On teaching logic programming in the era of generative AI. ~ Paul Tarau. #Prolog #LogicProgramming #GenerativeAI
• Bringing logic programming to primary school: a teacher training course. ~ Laura Andrea Cecchi, Jorge Pablo Rodríguez. #Prolog #LogicProgramming #Education
• On teaching constraint-based modeling and algorithms for decision support in Prolog. ~ François Fages. #CLP #LogicProgramming
• Desarrollo de sistema de resolución de rompecabezas en ASP mediante el uso de LLM. ~ Pedro Pazos Curra. #ASP #LLMs
• Verifying the Rust Standard Library. ~ Rahul Kumar et als. #Rust #Verification

The readings shared in Mastodon on 22 October 2024 are

• Readings shared October 21, 2024. #ITP #LeanProver #Lean4 #Coq #Math #AI #AI4Mat #Emacs #Lisp
• Kripke-style semantics for strong functors. ~ Nachiappan Valliappan. #ITP #Agda
• Analysis on normed semirings and semimodules. ~ Matt Verhoeven. #ITP #Coq #Math
• An unexpected discovery: Automated reasoning often makes systems more efficient and easier to maintain. ~ Byron Cook. #ITP
• Neural approaches to theorem search & proof repair. ~ Thomas Reichel. #ITP #Coq #LLMs
• Towards Guaranteed Safe AI: A framework for ensuring robust and reliable AI systems. ~ David Dalrymple et als. #AI

The readings shared in Mastodon on 21 October 2024 are

• Readings shared October 20, 2024. #ITP # #LambdaCalculus #FunctionalProgramming #ALP #LogicProgramming #AI #LLMs #Math
• The Lean Language Reference. #ITP #LeanProver #Lean4
• Formalizing hyperspaces and operations on subsets of polish spaces over abstract exact real numbers. ~ Michal Konečný, Sewon Park, Holger Thies.][]]AI for Mathematics paper list. #AI #Math #AI4Mat #ITP #Coq #Math
• Safeguarded AI: this programme aims to develop the safety standards we need for transformational AI. #AI
• Mathematics for Safe AI. ~ David Dalrymple. #AI
• Safeguarded AI: constructing guaranteed safety (Programme thesis). ~ David Dalrymple. #AI
• ProvablySafe.AI: a collaborative landing page for the field and community at the intersection of AI safety and formal methods. #AI
• Curso de Emacs Lisp. ~ Andros Fenollosa. #Emacs #Lisp
• Curso de Emacs Lisp orientado a las interfaces de usuario. ~ Andros Fenollosa. #Emacs #Lisp

The readings shared in Mastodon on 20 October 2024 are

• Readings shared October 20, 2024. #ITP #LeanProver #Lean4 #Math #Math #SetTheory #AI
• Foreign function verification through metaprogramming. ~ Joomy Korkut. #ITP #Coq
• Lecture notes on overview and the lambda calculus. ~ Jan Hoffmann. #LambdaCalculus
• Course: Types and Programming Languages. ~ Jan Hoffmann. #FunctionalProgramming
• An efficient propositional system for Abductive Logic Programming. ~ M. Gavanelli, P. Julián-Iranzo, F. Sáenz-Pérez. #ALP #LogicProgramming
• The accepted papers for the MATH-AI workshop have been released on OpenReview. #ITP #AI #LLMs #Math

The readings shared in Mastodon on 19 October 2024 are

• Readings shared October 18, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #Logic #Math #FunctionalProgramming #Prolog #LogicProgramming #Autoformalization #Emacs #Lisp
• ENS-Lean-course: Plain structures in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: How to build hierarchy of algebraic structures in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• Axiomatic set theory (Version of 18 October 2024). ~ Tom Leinster. #Math #SetTheory
• Nobel prizes and AI: The promise, the peril, and the path forward. ~ Marc Rotenberg. #AI

The readings shared in Mastodon on 18 October 2024 are

• Readings shared October 17, 2024. #Haskell #FunctionalProgramming #Ollama #LLMs #Math #Emacs #OrgMode
• How the Lean language brings math to coding and coding to math. ~ Leo de Moura. #Lean4 #ITP #FunctionalProgramming #Math
• Basic probability in Mathlib. ~ Rémy Degenne. #ITP #LeanProver #Math
• A complete formalization of Fermat's Last Theorem for regular primes in Lean. ~ Riccardo Brasca, Christopher Birkbeck, Eric Rodriguez Boidi, Alex Best, Ruben van De Velde, Andrew Yang. #ITP #LeanProver #Math
• Agda proof of the Knaster-Tarski Fixpoint Theorem. ~ Reed Mullanix. #ITP #Agda #Math
• Deep dive: The profound connection between Prolog and Lean (A technical analysis). ~ Alireza Dehbazargi. #Prolog #LogicProgramming #LeanProver #ITP
• Wooley's discrete inequality (in Isabelle/HOL). ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math
• Formalizing hyperspaces and operations on subsets of polish spaces over abstract exact real numbers. ~ Michal Konečný, Sewon Park, Holger Thies. #ITP #Coq #Math
• FormalAlign: Automated alignment evaluation for autoformalization. ~ Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, Zhijiang Guo. #Autoformalization #ITP #Lean4
• Improving Isabelle/VSCode: Towards better prover IDE integration via language server. ~ Thomas Lindae. #ITP #IsabelleHOL
• Course: Logic & algorithms. ~ Bob Atkey. #Logic
• Write your own Emacs Lisp macros - a short introduction. ~ Marie K. Ekeberg. #Emacs #Lisp

The readings shared in Mastodon on 17 October 2024 are

• Readings shared October 16, 2024. #AI #Education #FunctionalProgramming #Haskell #ITP #Lean4 #MachineLearning #Math1
• The Haskell Unfolder Episode 34: You already understand monads. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• Ollama-haskell: Haskell bindings for Ollama. ~ Tushar Adhatrao. #Haskell #FunctionalProgramming #Ollama #LLMs
• Big advance on simple-sounding math problem was a century in the making. ~ Erica Klarreich. #Math
• Thinking about 12 aspects of personal information/knowledge management. ~ Sacha Chua. #Emacs #OrgMode
• Manual en español de GNU/Emacs 29.1. ~ Tano. #Emacs

The readings shared in Mastodon on 16 October 2024 are

• Readings shared October 15, 2024. #AI #ChatGPT #Emacs #FunctionalProgramming #GeoGebra #Haskell #ITP #LambdaCalculus #Lean4 #LeanProver #LogicProgramming #Math #OrgMode #Prolog
• Lean: First steps (13 - Disquality). ~ Tariq Rashid #ITP #Lean4 #Math
• Munihac WASM experiment: convert Haskell expressions to pointfree in your browser. ~ Sergey Vinokurov. #Haskell #FunctionalProgramming
• Por qué debemos enseñar Machine Learning en todos los títulos universitarios. ~ Manuel de León Rodríguez y Rodrigo Trujillo González. #Education #AI #MachineLearning

The readings shared in Mastodon on 15 October 2024 are

• Readings shared October 13, 2024. #AI #CategoryTheory #Coq #Education #FunctionalProgramming #Haskell #ITP #ITP
• On using GeoGebra and ChatGPT for geometric discovery. ~ Francisco Botana, Tomás Recio, María Pilar Vélez. #GeoGebra #ChatGPT #Math #AI
• Lean: First steps (12 - Odd & Even ). ~ Tariq Rashid #ITP #Lean4 #Math
• Tutorial videos for the course "Lean: First Steps". ~ Tariq Rashid. #ITP #Lean4 #Math
• The handshaking lemma. ~ Christoph Spiegel. #ITP #LeanProver #Lean4 #Math
• Water sort in Haskell. ~ Nicolas Audinet de Pieuchon. #Haskell #FunctionalProgramming
• The power of Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Programación lógica con restricciones. #Prolog #LogicProgramming
• Emacs para ciencias del dato. #Emacs #OrgMode
• The λ-calculus, 2: The Church-Rosser theorem. ~ Lawrence Paulson. #LambdaCalculus

The readings shared in Mastodon on 13 October 2024 are

• Readings shared October 12, 2024. #AI #ATP #IMO #ITP #LLMs #Lean4 #MachineLearning #Math #SetTheory
• Effects and coeffects in call-by-push-value. ~ Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich. #ITP #Coq
• Fully verified instruction scheduling. ~ Ziteng Yang, Jun Shirako, Vivek Sarkar. #ITP #Coq
• Iris-MSWasm: Elucidating and mechanising the security invariants of memory-safe WebAssembly. ~ Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal. #ITP #Coq
• Hazel: a live functional programming environment organized around typed holes. ~ Cyrus Omar et als. #ITP #FunctionalProgramming #Hazel
• Learner-centered design criteria for classroom proof assistants. ~ Matthew Keenan, Cyrus Omar. #ITP #Hazel
• Accessible bridge between category theory and functional programming. ~ Fethi Kadhi. #Haskell #FunctionalProgramming #CategoryTheory
• Refinement type refutations. ~ Robin Webbers, Klaus von Gleissenthall, Ranjit Jhala. #Haskell #FunctionalProgramming
• Intensional functions. ~ Zachary Palmer, Nathaniel Wesley Filardo, Ke Wu. #Haskell #FunctionalProgramming
• Semantics lifting for syntactic sugar. ~ Zhichao Guan, Yiyuan Cao, Tailai Yu, Ziheng Wang, Di Wang, Zhenjiang Hu. #Haskell #FunctionalProgramming
• The use of artificial intelligence in teaching students programming languages. ~ Svitlana Lytvynova, Natalya Rashevska and Svitlana Proskura. #AI #Education #Programming

The readings shared in Mastodon on 12 October 2024 are

• Readings shared October 11, 2024. #ITP #LeanProver #Coq #Deduce #IsabelleHOL #Math #LLMs #LogicProgramming
• ENS-Lean-course: Functions in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Taxicab number in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• IMOSLLean4: Formalization of IMO shortlist problems in Lean 4. ~ Gian Sanjaya. #ITP #Lean4 #Math #IMO
• AI for Mathematics. ~ Jeremy Avigad. #ITP #LeanProver #ATP #AI #MachineLearning #LLMs #Math
• Axiomatic set theory (Version of 9 October 2024). ~ Tom Leinster. #Math #SetTheory

The readings shared in Mastodon on 11 October 2024 are

• Readings shared October 10, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #Math #HoTT #LLMs
• ImProver: Agent-based automated proof optimization. ~ Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck. #ITP #LeanProver #LLMs
• Combining Waterproof and Mathematical Components (Utilising Mathematical Components in Waterproof to teach linear algebra proving). ~ Dick Arends. #ITP #Coq #Waterproof #Math
• Take-aways from using Deduce in the classroom. ~ Jeremy Siek. #ITP #Deduce
• The elementary theory of the category of sets (in Isabelle/HOL). ~ James Baxter & Dustin Bryant. #ITP #IsabelleHOL #Math
• Automated geometric theorem proving: Wu's method. ~ Joran Elias. #ATP #Math
• Can logic programming be liberated from predicates and backtracking? ~ Michael Hanus. #LogicProgramming

The readings shared in Mastodon on 10 October 2024 are

• Readings shared October 9, 2024. #Haskell #FunctionalProgramming
• #Exercitium: Número de ocurrencias de elementos. #Haskell
• M2Lyon2425: Group theory in Lean. ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #Math
• A complete formalization of Fermat's Last Theorem for regular primes in Lean. ~ Riccardo Brasca, Christopher Birkbeck, Eric Rodriguez Boidi, Alex Best, Ruben van De Velde, Andrew Yang. #ITP #LeanProver #Lean4 #Math
• Pointwise order of generalized Hofstadter functions G, H and beyond. ~ Pierre Letouzey, Shuo Li, Wolfgang Steiner. #ITP #Coq #Math
• Finite element method. Detailed proofs to be formalized in Coq. ~ François Clément, Vincent Martin. #ITP #Coq #Math
• Modelling and proving the monotonicity of processor pipelines in Coq. ~ Alban Gruin, Armelle Bonenfant, Thomas Carle, Christine Rochange. #ITP #Coq
• The Karatsuba square root algorithm (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Polynomial universes and dependent types. ~ C.B. Aberlé, David I. Spivak. #ITP #Agda
• Formalization of homotopy pushouts in homotopy type theory. ~ Vojtěch Štěpančík. #ITP #Agda #Math #HoTT
• AlphaIntegrator: Transformer action search for symbolic integration proofs. ~ Mert Ünsal, Timon Gehr, Martin Vechev. #LLMs #Math
• Demostraciones por inducción en Lean. ~ Luis Turcio. #ITP #Lean4

The readings shared in Mastodon on 9 October 2024 are

• Readings shared October 8, 2024. #ITP #IsabelleHOL #Lean4 #Mizar #Math #CompSci #Haskell #FunctionalProgramming #Emacs #OrgMode
• 18 months of the Haskell Unfolder. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming

The readings shared in Mastodon on 8 October 2024 are

• Readings shared October 7, 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Calculemus #LLMs
• Formalising the double-pushout approach to graph transformation. ~ Robert Söldner, Detlef Plump. #ITP #IsabelleHOL
• Formal BOOK (formalizing "Proofs from THE BOOK" by Martin Aigner and Günter M. Ziegler). ~ Moritz Firsching, Nick Kuhn, Ralf Stephan, Christopher Schmidt. #ITP #Lean4 #Math
• Bonn Lean Course WiSe 24/25. ~ Floris van Doorn. #ITP #Lean4
• BonnLeanCourse: 1 - Introduction to Lean 4. ~ Floris van Doorn. #ITP #Lean4
• Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. ~ Karol Pąk, Cezary Kaliszyk. #ITP #Mizar #Math
• What is theoretical computer science? ~ Moshe Y. Vardi. #CompSci #Math
• Literate Org Haskell. ~ F. Murillo. #Emacs #OrgMode #Haskell #FunctionalProgramming
• Using Org Mode to write and organize a book. ~ Ron Galloway. #Emacs #OrgMode

The readings shared in Mastodon on 7 October 2024 are

• Readings shared October 6, 2024. #ITP #LeanProver #Logic #Math #AI #Python
• Proofs of the pigeonhole principle in Lean4. #ITP #Lean4 #Math #Calculemus
• Formalizing MLTL formula progression in Isabelle/HOL. ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Rozier. #ITP #IsabelleHOL #Logic
• Repo for the first BerLean workshop. #ITP #Lean4 #Math
• Re-invention of group/ring algebra in Lean 4 for learning purposes. ~ Eugene Zolotarev. #ITP #Lean4 #Math
• Introduction to mathematical arguments (background handout for courses requiring proofs). ~ Michael Hutchings. #Logic #Math
• How to write proofs: a quick guide. ~ Eugenia Cheng. #Logic #Math
• Notes on math proof. ~ Bruce Ikenaga. #Logic #Math
• Proof writing and presentation tips. ~ Erika L.C. King. #Logic #Math
• How to write mathematics. ~ Martin Erickson. #Logic #Math
• Advice on mathematical writing. ~ Keith Conrad. #Math
• Examples of proofs by induction. ~ Keith Conrad. #Math
• An introduction to proofs and the mathematical vernacular. ~ Martin V. Day. #Math
• Conventions for writing mathematical proofs. ~ John M. Lee. #Math
• TheoremLlama: Transforming general-purpose LLMs into Lean4 experts. ~ Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang. #ITP #Lean4 #LLMs

The readings shared in Mastodon on 6 October 2024 are

• Readings shared October 5, 2024. #ITP #LeanProver #Lean4 #Agda #Logic #Math #FunctionalProgramming #AI
• Grelling–Nelson paradox. #Logic
• Formalization of the Grelling's paradox in the Lean theorem prover. ~ Juan Pablo Yamamoto. #ITP #LeanProver #Logic
• Proofs shown to be wrong after formalization with proof assistant. #ITP #Math
• We're entering uncharted territory for Math (Terence Tao, the world’s greatest living mathematician, has a vision for AI). ~ Matteo Wong. #Math #AI #ITP
• Curso Python para Matemáticas. ~ Javier García-Algarra. #Matemáticas #Python

The readings shared in Mastodon on 5 October 2024 are

• Readings shared October 4, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Python
• ENS-Lean-course: Taxicab number in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Sets in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean-course: Homework 3: Sets. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• PCC116-2021: Lógica aplicada à computação (2021/22). ~ Rodrigo Ribeiro. #ITP #Agda #Logic #Math #CompSci
• PCC116: Lógica aplicada à computação (2024). ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #CompSci
• PCC116: Aula 1: Lógica proposicional em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math
• PCC116: Aula 2: Predicate logic in Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math
• PCC116: Aula 3: Programação funcional em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 4: Programação funcional e recursividade em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 5: Listas encadeadas (tipo List na biblioteca) em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 6: Predicados indutivos em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 8: Programando com tipos dependentes em Lean. ~ Rodrigo Ribeiro. #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 9: Sobrecarga e classes de tipos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 10: Metaprogramação e automação de provas em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 11: Recursão geral em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 12: Representando semântica formal em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 13: λ-cálculo tipado simples em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 14: Formalizando em Lean compiladores / semântica de linguagens imperativas. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• PCC116: Aula 15: Modelagem de autômatos em Lean. ~ Rodrigo Ribeiro (@rodrigogeraldo). #ITP #Lean4 #Logic #Math #FunctionalProgramming
• Terence Tao’s vision of AI assistants in research mathematics. ~ David H Bailey. #Math #AI #ITP #LeanProver

The readings shared in Mastodon on 4 October 2024 are

• Readings shared October 3, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Haskell #FunctionalProgramming
• Proofs of "If f ∘ f is bijective, then f is bijective" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Abstract substitution (in Isabelle/HOL). ~ Martin Desharnais. #ITP #IsabelleHOL
• Discrete Math. ~ Mohamed Jamaloodeen, Kathy Pinzon, Daniel Pragel, Joshua Roberts & Sebastien Siva. #Math #Python

The readings shared in Mastodon on 1 October 2024 are

• Readings shared September 30, 2024. #ITP #LeanProver #Lean4 #Math #LambdaCalculus
• ENS-Lean_course: Homework 2 (Logic). ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• The geometry game. ~ Marc Masdeu.. #ITP #Lean3 #Math
• Parallel shear sort (in Isabelle/HOL). ~ Manuel Eberl & Peter Lammich. #ITP #IsabelleHOL #Algorithms
• Rule synthesis etudes for Tao's algebra problem. ~ Philip Zucker. #ATP #SMT #Z3
• Functional programming course for Telecom Nancy, using Haskell. ~ Clément Hurlin. #Haskell #FunctionalProgramming
• Integrando AI con mi herramienta de trabajo preferida: Google Gemini, Emacs Lisp y GNU/Linux!! ~ lksadj. #Emacs #AI #GoogleGemini

The readings shared in Mastodon on 30 September 2024 are

• Readings shared September 29, 2024. #ITP #LeanProver #Lean4 #Logic #Math #Haskell #FunctionalProgramming #Prolog #ASP #LogicProgramming #AI
• Introduction to the λ-calculus. ~ Lawrence C. Paulson. #LambdaCalculus
• How to read Lean. ~ Martin Dvořák. #ITP #LeanProver #Math
• Certifying rings of integers in number fields. ~ Anne Baanen, Alain Chavarri Villarello & Sander R. Dahmen. #ITP #Lean4 #Math

The readings shared in Mastodon on 29 September 2024 are

• Readings shared September 28, 2024. #ITP #LeanProver #IsabelleHOL #Coq #HOL_Light #Logic #Math
• M2Lyon2425: Sets and functions (Solutions). ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #Math
• M2Lyon2425: Sets and functions. ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Introduction to Lean. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Proofs by calculation. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Using theorems in Lean. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Lean style guidelines. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Homework 1 (Sep 21, 2024). ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• ENS-Lean_course: Logic in Lean4. ~ Roman Soletskyi. #ITP #LeanProver #Lean4 #Math
• Con(NF): A formal consistency proof of Quine's set theory New Foundations. ~ Sky Wilshaw et als. #ITP #Lean4 #Math
• Welcome to the parti(tioning) (Functional Pearl): Using rewrite rules and specialisation to partition Haskell programs. ~ Robert Krook & Samuel Hammersber. #Haskell #FunctionalProgramming
• The Marseille-Edinburgh connection. ~ Robert Kowalski. #Prolog #LogicProgramming
• PROLOG en son temps: hier, aujourd’hui, demain. Un point de vue industriel, économique et géopolitique. ~ Jean Rohmer. #Prolog #LogicProgramming
• L’IA symbolique et le dépassement de la logique classique. ~ Henri Prade. #AI #Logic #Prolog #LogicProgramming
• ASP: un devenir de Prolog. ~ Belaïd Benhamou, Vincent Risch & Éric Würbel. #LogicProgramming #Prolog #ASP
• Dimensions linguistiques de Prolog : le passé, le futur. ~ Verónica Dahl. #Prolog #AI

The readings shared in Mastodon on 28 September 28 2024 are

• Readings shared September 27, 2024. #ATP #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Math #CategoryTheory #SetTheory
• Hyperstability in the Erdős-Sós conjecture. ~ Alexey Pokrovskiy. #ITP #LeanProver #Math
• Formalized soundness and completeness of epistemic logic. ~ Asta Halkjær From, Alexander Birch Jensen & Jørgen Villadsen. #ITP #IsabelleHOL #Logic #Math
• Löb’s theorem and provability predicates in Coq. ~ Janis Bailitis. #ITP #Coq #Logic #Math
• Formalizing potential flows using the HOL Light theorem prover. ~ Elif Deniz & Sofiène Tahar. #ITP #HOL_Light
• Formal verification of coupled transmission lines using theorem proving. ~ Elif Deniz, Adnan Rashid & Sofiène Tahar. #ITP #HOL_Light