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

The readings shared in Mastodon on September 27, 2024 are

• A pilot project in universal algebra to explore new ways to collaborate and use machine assistance? ~ Terence Tao. #ITP #LeanProver #Lean4 #Math
• Equational theory project. ~ Terence Tao et als. #ITP #ATP #Math
• Equational theories (Blueprint). ~ Terence Tao. #ITP #Lean4 #Math
• Knuckledragger solvers for Terence Tao's equational reasoning challenge. ~ Philip Zucker. #ITP #Math
• Linear algebra in "Mathematics in Lean". ~ Patrick Massot. #ITP #Lean4 #Math
• Lean: First steps (09 - "Or" goal). ~ Tariq Rashid. #ITP #Lean4 #Math
• Lean: First steps (11 - Existence). ~ Tariq Rashid #ITP #Lean4 #Math
• Post’s problem and the priority method in synthetic computability. ~ Haoyi Zeng. #ITP #Coq
• Secure smart contracts with Isabelle/Solidity. ~ Diego Marmsoler, Asad Ahmed & Achim D. Brucker. #ITP #IsabelleHOL
• Theoretical and practical approach to the soundness and completeness of operational semantics based on denotational semantics for MDESL. ~ Hongyan Zhao, Huibiao Zhu, Feng Sheng, Jifeng He & Jonathan Bowen. #ITP #Coq
• The universal presence of category theory. ~ Gabriel Field. #Math #CategoryTheory
• Axiomatic set theory (Version of 24 September 2024). ~ Tom Leinster. #Math #SetTheory

The readings shared in Mastodon on September 25, 2024 are

• Readings shared September 24, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Logic #Math #SetTheory #Haskell #FunctionalProgramming #AI #LLMs
• Proofs of the Brahmagupta-Fibonacci identity in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• M2Lyon2425: Sets and functions (1). ~ Filippo A. E. Nuccio. #ITP #LeanProver #Lean4 #Math
• Cambridge combinatorics in Lean (Formalisation of the Cambridge combinatorics courses). ~ Yaël Dillies. #ITP #LeanProver #Lean4 #Math
• The Matrix Cookbook, using Lean's mathlib. ~ Eric Wieser. #ITP #LeanProver #Lean4 #Mathlib #Math
• Math-Haskell Rosetta Stone - Part 1. ~ Daniel Brice. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 24, 2024 are

• Readings shared September 23, 2024. #ITP #LeanProver #Coq #IsabelleHOL #Math #ITP #Haskell #FunctionalProgramming #AI #LLMs
• Proofs of ∑k<n. 2ᵏ = 2ⁿ-1 in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Code examples from a Lean tutorial at the Copenhagen functional programming meetup (1/2). ~ David Thrane Christiansen. #ITP #Lean4 #FunctionalProgramming
• Code examples from a Lean tutorial at the Copenhagen functional programming meetup (2/2). ~ David Thrane Christiansen. #ITP #Lean4 #FunctionalProgramming
• Playing with a game. ~ Chris Smith. #Haskell #FunctionalProgramming
• Applicative logic. ~ Håkon Robbestad Gylterud. #Haskell #FunctionalProgramming #Logic
• Axiomatic set theory 1: Introduction. ~ Tom Leinster. #Math #SetTheory
• Axiomatic set theory (Version of 21 September 2024). ~ Tom Leinster. #Math #SetTheory
• On logic and generative AI. ~ Yuri Gurevich, Andreas Blass. #Logic #AI
• Proof automation with Large Language Models. ~ Minghai Lu, Benjamin Delaware, Tianyi Zhang. #ITP #Coq #LLMs
• ChatGPT as a solver and grader of programming exams written in spanish. ~ Pablo Fernández-Saborido, Marcos Fernández-Pichel, David E. Losada. #LLMs #ChatGPT #CompSci
• Is math the path to chatbots that don't make stuff up? ~ Cade Metz. #AI #ITP #Lean4 #Math
• Harmonic: We are forging the world's most advanced mathematical reasoning engine. #AI #ITP #Math

The readings shared in Mastodon on September 23, 2024 are

• Readings shared September 22, 2024. #ITP #LeanProver #Lean3 #Lean4 #Logic #Math
• Introduction to Lean. ~ Markus Himmel. #ITP #LeanProver #Math
• Scientific computing in Lean. ~ Tomáš Skřivan. #ITP #LeanProver #Math
• Tips and tricks for beginners using Mathlib/Lean. ~ Moritz Firsching. #ITP #LeanProver
• Lean Tutorial in Vienna. ~ Pietro Monticone et als. #ITP #LeanProver #Math
• Turning the Coq proof assistant into a pocket calculator. ~ Guillaume Melquiond. #ITP #Coq
• A case for first-class environments. ~ Jinhao Tan & Bruno C. D. S. Oliveira. #ITP #Coq
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov & Anton Podkopaev. #ITP #Coq #AI #LLMs
• Rabin's closest pair of points algorithm (in Isabelle/HOL). ~ Emin Karayel & Zixuan Fan. #ITP #IsabelleHOL
• Wlog – Without loss of generality (in Isabelle/HOL). ~ Dominique Unruh. #ITP #IsabelleHOL
• Haskell tutorial and cookbook. ~ Mark Watson. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 22, 2024 are

• Readings shared September 21, 2024. #ITP #IsabelleHOL #LeanProver #Lean3 #Lean4 #Mathlib #Logic #Math #AI #LLMs #DeepLearning
• Lean: First steps (08 - "And" hypothesis). ~ Tariq Rashid. #ITP #Lean4 #Math
• Using Lean theorem prover to teach formal mathematics: Lean-Intro-Topology library. ~ Rafael Grenier. #ITP #LeanProver #Lean4 #Math
• Lean-Intro-Topology: Introduction to topology with Lean. ~ Rafael Grenier. #ITP #LeanProver #Lean4 #Math
• "A concise introduction to mathematical logic" in Lean4. ~ Enrico Borba. #ITP #LeanProver #Lean4 #Logic #Math
• Lean proofs of (some) problems from the book "102 combinatorial problems". ~ Musab Guma'a et als. #ITP #LeanProver #Lean4 #Math
• The Topology Game (Learn topology with Lean!). ~ Barcelona Lean Seminar. #ITP #LeanProver #Math
• Source of the "The Topology Game". ~ Marc Masdeu et als. #ITP #LeanProver #Lean3 #Math
• Formalization of Riemann-Stieltjes integral in Lean4. ~ Marc Masdeu et als. #ITP #LeanProver #Lean4 #Math
• A Lean 4 proof of unique prime factorization in well-ordered rings, starting from ring axioms. ~ Mattchen. #ITP #LeanProver #Lean4 #Math
• Formalisation of mathematics and dependent-type programming (A tutorial introduction using the Lean4 theorem prover). ~ Frédéric Peschanski. #ITP #LeanProver #Lean4 #Math
• A tutorial introduction of dependently-typed programming (and the Lean4 theorem prover). ~ Frédéric Peschanski. #ITP #LeanProver #Lean4 #Math

The readings shared in Mastodon on September 21, 2024 are

• Readings shared September 20, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #ATP #Prover9 #Mace4
• Course: Theorem proving with Lean. ~ Damiano Testa. #ITP #LeanProver #Math
• Finding lemmas in Mathlib. ~ Damiano Testa. #ITP #LeanProver #Mathlib
• Course: Repository for the Lean master program in Lyon for 2024-25. ~ Filippo A. E. Nuccio et als. #ITP #LeanProver #Math
• Weekly-Lean: The Lean weekly challenge. ~ Kyle Thompson, Saketh Kasibatla & Nico Lehmann. #ITP #LeanProver
• Mini-curso de Lean. ~ Luis Turcio. #ITP #LeanProver #Logic #Math
• Lean - Tácticas y proposiciones. ~ Luis Turcio. #ITP #LeanProver
• Lean - Proposiciones y primer orden. ~ Luis Turcio. #ITP #LeanProver #Logic
• Lean - Conjuntos 1. ~ Luis Turcio. #ITP #LeanProver #Logic #Math
• Lean - Funciones. ~ Luis Turcio. #ITP #LeanProver #Logic #Math
• Topología general en Lean3. ~ Miguel Marco. #ITP #LeanProver #Lean3 #Math
• Juego LEAN de topología general. ~ Miguel Marco. #ITP #LeanProver #Lean4 #Math
• Stone duality in Lean. ~ Dagur Ásgeirsson, Sam van Gool, Tomáš Jakl & Filippo A.E. Nuccio. #ITP #LeanProver #Lean4 #Math
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving. ~ Kangfeng Ye, Jim Woodcock & Simon Foster. #ITP #IsabelleHOL
• No generalization without understanding and explanation (Why AI needs symbolic and logical reasoning). ~ Walid Saba. #AI #LLMs #DeepLearning #Logic
• Qwen2.5-Math: The world's leading open-sourced mathematical LLMs. #LLMs #Math
• Qwen2.5-Coder Technical Report. ~ Binyuan Hui et als. #LLMs #Programming

The readings shared in Mastodon on September 20, 2024 are

• Readings shared September 19, 2024. #ITP #Coq #Math #Haskell #FunctionalProgramming #Logic #AI
• Proofs of "∑i<n. i = n(n-1)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #CaWlculemus
• Extending Isabelle/HOL's code generator with support for the Go programming language. ~ Terru Stübinger & Lars Hupel. #ITP #IsabelleHOL #GoLang
• Mapping probability with logic: First order models in puzzle solving. ~ Adrian Groza. #ATP #Prover9 #Mace4

The readings shared in Mastodon on September 19, 2024 are

• Readings shared September 18, 2024. #ITP #IsabelleHOL
• An imperative language for verified exact real-number computation. ~ Andrej Bauer, Sewon Park & Alex Simpson. #ITP #Coq #Math
• The Haskell Unfolder Episode 32: Solving tic-tac-toe. ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• What is logic-based/logicist AI? (Its history). ~ Selmer Bringsjord. #Logic #AI
• The failure of Deep Learning (GPT-4o bites the dust). ~ Selmer Bringsjord. #Logic #AI
• AI should challenge, not obey (Let’s transform our robot secretaries into Socratic gadflies). ~ Advait Sarkar. #AI #CriticalThinking
• La mecánica cuántica explicada de otra forma fácil de entender y en su contexto histórico. ~ @Alvy. #Física

The readings shared in Mastodon on September 18, 2024 are

• Readings shared September 17, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Autoformalization #Emacs
• Combining classical and probabilistic independence reasoning to verify the security of oblivious algorithms. #ITP #IsabelleHOL
• Efficient formally verified maximal end component decomposition for MDPs. ~ Arnd Hartmanns, Bram Kohlen & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on September 17, 2024 are

• Readings shared September 16, 2024. #ITP #LeanProver #Lean4 #Math #Haskell #FunctionalProgramming
• Scientific computing in Lean. ~ Tomáš Skřivan. #ITP #LeanProver #Lean4 #Math
• Towards verified polynomial factorisation. ~ James H. Davenport. #ITP #LeanProver #Math
• First steps towards computational polynomials in Lean. ~ James H. Davenport. #ITP #LeanProver #Math
• miniCodeProps: A minimal benchmark for proving properties of code. ~ Evan Lohn & Sean Welleck. #ITP #LeanProver #Lean4 #LLMs
• Leveraging large language models for autoformalizing theorems: A case study. ~ Michail Karatarakis. #ITP #LeanProver #Lean4 #Autoformalization #Math
• Concrete bounds for Chebyshev’s prime counting functions (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Why Emacs is the best: 10 key advantages. ~ Tristan de Cacqueray. #Emacs

The readings shared in Mastodon on September 16, 2024 are

• Readings shared September 15, 2024. #ITP #LeanProver #Lean4 #LLMs
• Duality theory in linear optimization and its extensions (formally verified). ~ Martin Dvorak & Vladimir Kolmogorov. #ITP #LeanProver #Lean4 #Math
• The Haskell playground. ~ Tom Smeding. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 15, 2024 are

• Readings shared September 14, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Agda #HOL_Light #Math #Haskell #FunctionalProgramming #LambdaCalculus #LLMs
• LLMlean integrates LLMs and Lean for tactic suggestions, proof completion, and more. ~ Sean Welleck et als. #ITP #LeanProver #Lean4 #LLMs
• LeanDojo: Theorem Proving in Lean using Language Models. ~ Kaiyu Yang et als. #ITP #LeanProver #Lean4 #LLMs
• llmstep: [L]LM proofstep suggestions in Lean 4. ~ Sean Welleck et als. #ITP #LeanProver #Lean4 #LLMs

The readings shared in Mastodon on September 14, 2024 are

• Readings shared September 13, 2024. #Haskell #FunctionalProgramming #LiquidHaskell #Emacs #OrgMode
• AI for Mathematics: Mathematical formalized problem solving and theorem proving in different fields in Lean 4. ~ Xichen Tang. #ITP #LeanProver #Lean4 #Math
• Better-performing “25519” elliptic-curve cryptography (Automated reasoning and optimizations specific to CPU microarchitectures improve both performance and assurance of correct implementation). ~ Torben Hansen, John Harrison. #ITP #HOL_Light
• A simple proof that π is irrational (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Decidable equality for indexed data types. ~ Brent Yorgey. #ITP #Agda #FunctionalProgramming
• Why Haskell? ~ Gideon Farrell. #Haskell #FunctionalProgramming
• Type-theoretic considerations in functional language software development. ~ David Michael Roberts. #Haskell #FunctionalProgramming #ITP #IsabelleHOL
• Simulation of lambda terms in lambda calculus. ~ Helmut Brandl. #LambdaCalculus
• Estrenando el nuevo modelo de OpenAI: o1-preview. Resolviendo con ChatGPT un problema de Matemáticas II de la Prueba de Acceso a la Universidad EBAU. ~ Luis M. Iglesias. #LLMs #Matemáticas

The readings shared in Mastodon on September 13, 2024 are

• Readings shared September 12, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #LLMs
• Reflecting away from definitions in Liquid Haskell. ~ Jonathan Arnoult. #Haskell #FunctionalProgramming #LiquidHaskell
• Why and how I use "Org Mode" for my writing and more. ~ Aditya Athalye. #Emacs #OrgMode

The readings shared in Mastodon on September 12, 2024 are

• Readings shared September 11, 2024. #ITP #IsabelleHOL #LeanProver #Coq #NaprocheZF #Natty #AlphaGeometry #AlphaProof #FunctionalProgramming #OCaml #Logic #Math #IMO #AI #MachineLearning #LLMs
• Proofs of "If p > -1, then (1+p)ⁿ ≥ 1+np" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• The undecidability of contextual equivalence on PCF2 (Towards a mechanisation in Coq). ~ Fabian Andreas Brenner. #ITP #Coq
• 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 September 11, 2024 are

• Readings shared September 10, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #Python #Math
• Mathematical Olympiad (To the geometry and beyond…). ~ Mirek Olšák. #Math #ITP #AI #IMO #AlphaGeometry #AlphaProof #LeanProver
• Isabelle/RL project proposal: Reinforcement learning on the Isabelle proof assistant. ~ Jonathan Julián Huerta y Munive. #ITP #IsabelleHOL #MachineLearning
• CoqPilot, a plugin for LLM-based generation of proofs. ~ Andrei Kozyrev, Gleb Solovev, Nikita Khramov & Anton Podkopaev. #ITP #Coq #LLMs
• ATPs as universal AIs: What do AGI architectures suggest for ATP research? ~ Zarathustra Goertzel. #ATP #AI
• The formal theory of monads, univalently. ~ Niels van der Weide. #ITP #Coq
• 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 #AI #LLMs
• Naproche-ZF: Lessons learned from implementing a new natural-language-oriented theorem prover. ~ Adrian De Lon. #ITP #NaprocheZF #Math
• Natural-language proof assistant for higher-order logic. ~ Adam Dingle. #ITP #Natty #Math
• Natty: a natural-language proof assistant with an embedded automatic prover for higher-order logic. ~ Adam Dingle. #ITP #Natty #Math #OCaml
• A few open problems in neural theorem proving (in Lean). ~ Sean Welleck. #ITP #LeanProver #LLMs
• Project description: Experiments with language models for Isabelle autoformalization. ~ David Valente, Manuel Eberl, Cezary Kaliszyk & Josef Urban. #ITP #IsabelleHOL #Autoformalization
• Provably safe systems: Prospects and approaches. ~ Mario Carneiro. #ITP #AI
• With fifth busy beaver, researchers approach computation’s limits. ~ Ben Brubaker. #ITP #Coq #Math #CompSci
• Kids should be taught to think logically. ~ Vinay K. Chaudhri. #Logic

The readings shared in Mastodon on September 10, 2024 are

• Readings shared September 9, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Prolog #LogicProgramming #Python
• Proofs of 0³+1³+2³+3³+···+n³ = (n(n+1)/2)² in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• #Exercitium: Sumas de dos abundantes. #Haskell #Python #Matemáticas
• Types as interfaces. ~ Chris. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 9, 2024 are

• Readings shared September 8, 2024. #ITP #Agda #Math #Haskell #FunctionalProgramming
• Proofs of "a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Describing a knight's tour with Prolog. ~ Markus Triska. #Prolog #FunctionalProgramming
• String Knuth Bendix. ~ Philip Zucker. #Math #Python

The readings shared in Mastodon on September 8, 2024 are

• Readings shared September 7, 2024. #ITP #Lean4 #IsabelleHOL #Maude #ATP #Prover9 #Math #Calculemus
• Formalization of the structure sheaf of a ring spectrum. ~ Maša Žaucer. #ITP #Agda #Math
• Automatic test-case generation for Haskell based on dependent types. ~ Pablo Castellanos García. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 7, 2024 are

• Readings shared September 6, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Agda #PVS #Logic #HOL4 #Lisa #Mizar #ACL2 #Math #AI #MachineLearning
• Proofs of "a+(a+d)+(a+2d)+···+(a+nd) = (n+1)(2a+nd)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Metaprogramming in Lean. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Examples using MetaProgramming for writing tactics. ~ Siddhartha Gadgil. #ITP #LeanProver #Lean4
• Formalisation of Hall’s theorem for countable infinite graphs. ~ Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón & Thaynara Arielly de Lima. #ITP #IsabelleHOL #Math
• First-order theorem proving with power maps in semigroups. ~ Yi Lin1, Ranganathan Padmanabhan & Yang Zhang. #ATP #Prover9 #Math
• Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. #ITP #Maude #LeanProver #Lean3

The readings shared in Mastodon on September 6, 2024 are

• Readings shared September 5, 2024. #ITP #LeanProver #Lean4 #IsabelleHO #Agda #Logic #Math #Calculemus #Haskell #OCaml #FunctionalProgramming #AI
• Towards solid abelian groups: A formal proof of Nöbeling’s theorem. ~ Dagur Asgeirsson. #ITP #LeanProver #Math
• The directed Van Kampen theorem in Lean. ~ Henning Basold, Peter Bruin & Dominique Lawson. #ITP #LeanProver #Lean4 #Math
• Verifying peephole rewriting in SSA compiler IRs. ~ Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens & Tobias Grosser. #ITP #LeanProver
• Duper: A proof-producing superposition theorem prover for dependent type theory. ~ Joshua Clune, Yicheng Qian, Alexander Bentkamp & Jeremy Avigad. #ITP #LeanProver #Lean4
• Teaching mathematics using Lean and controlled natural language. ~ Patrick Massot. #ITP #LeanProver #Lean4 #Math
• Lean formalization of completeness proof for Coalition Logic with Common Knowledge. ~ Kai Obendrauf, Anne Baanen, Patrick Koopmann & Vera Stebletsova. #ITP #LeanProver #Lean4
• Formal verification of the empty hexagon number. ~ Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro & Marijn J. H. Heule. #ITP #LeanProver #Lean4
• Integrals within integrals: A formalization of the Gagliardo-Nirenberg-Sobolev inequality. ~ Floris van Doorn & Heather Macbeth. #ITP #LeanProver #Lean4 #Math
• Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4. ~ Sam Ezeh. #ITP #LeanProver #Lean4 #Math
• Formalising half of a graduate textbook on number theory. ~ Manuel Eberl, Anthony Bordg, Lawrence C. Paulson & Wenda Li. #ITP #IsabelleHOL #Math
• A formalization of the Lévy-Prokhorov metric in Isabelle/HOL. ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• Alpha-beta pruning verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
• A formal analysis of capacity scaling algorithms for minimum cost flows. ~ Mohammad Abdulaziz & Thomas Ammer. #ITP #IsabelleHOL
• An operational semantics in Isabelle/HOL-CSP. ~ Benoît Ballenghien & Burkhart Wolff. #ITP #IsabelleHOL
• A verified earley parser. ~ Martin Rau & Tobias Nipkow. #ITP #IsabelleHOL
• A modular formalization of superposition in Isabelle/HOL. ~ Martin Desharnais, Balazs Toth, Uwe Waldmann, Jasmin Blanchette & Sophie Tourret. #ITP #IsabelleHOL
• Distributed parallel build for the Isabelle Archive of Formal Proofs. ~ Fabian Huch & Makarius Wenzel. #ITP #IsabelleHOL
• A generalised union of rely–guarantee and separation logic using permission algebras. ~ Vincent Jackson, Toby Murray & Christine Rizkallah. #ITP #IsabelleHOL
• An Isabelle/HOL formalization of narrowing and multiset narrowing for E-unifiability, reachability and infeasibility. ~ Dohan Kim. #ITP #IsabelleHOL
• A Coq formalization of Taylor models and power series for solving ordinary differential equations. ~ Sewon Park & Holger Thies. #ITP #Coq #Math
• A comprehensive overview of the Lebesgue differentiation theorem in Coq. ~ Reynald Affeldt & Zachary Stone. #ITP #Coq #Math
• Taming differentiable logics with Coq formalisation. ~ Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz & Kathrin Stark. #ITP #Coq #Logic #MachineLearning
• Completeness of asynchronous session tree subtyping in Coq. ~ Burak Ekici & Nobuko Yoshida. #ITP #Coq
• End-to-end formal verification of a fast and accurate floating-point approximation. ~ Florian Faissole, Paul Geneau de Lamarlière & Guillaume Melquiond. #ITP #Coq
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue & Takafumi Saikawa. #ITP #Coq
• Verifying software emulation of an unsupported hardware instruction. ~ Samuel Gruetter, Thomas Bourgeat & Adam Chlipala. #ITP #Coq
• Modular verification of intrusive list and tree data structures in separation logic. ~ Marc Hermes & Robbert Krebbers. #ITP #Coq
• Formalizing the algebraic small object argument in UniMath. ~ Dennis Hilhorst & Paige Randall North. #ITP #Coq #Math
• The Rewster: Type preserving rewrite rules for the Coq proof assistant. ~ Yann Leray, Gaëtan Gilbert, Nicolas Tabareau & Théo Winterhalter. #ITP #Coq
• Correctly compiling proofs about programs without proving compilers correct. ~ Audrey Seo, Christopher Lam, Dan Grossman & Talia Ringer. #ITP #Coq
• Redex2Coq: Towards a theory of decidability of redex’s reduction semantics. ~ Mallku Soldevila, Rodrigo Ribeiro & Beta Ziliani. #ITP #Coq
• Defining and preserving more C behaviors: Verified compilation using a concrete memory model. ~ Andrew Tolmach, Chris Chhak & Sean Anderson. #ITP #Coq
• Robust mean estimation by all means. ~ Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa & Carsten Schürmann. #ITP #Coq
• Abstractions for multi-sorted substitutions. ~ Hannes Saffrich. #ITP #Agda
• The functor of points approach to schemes in Cubical Agda. ~ Max Zeuner & Matthias Hutzler. #ITP #Agda
• A formalization of the general theory of quaternions. ~ Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro & Mauricio Ayala-Rincón. #ITP #PVS #Math
• Formalizing the Cholesky factorization theorem. ~ Carl Kwan & Warren A. Hunt Jr. #ITP #ACL2 #Math
• A formal proof of R(4,5)=25. ~ Thibault Gauthier & Chad E. Brown. #ITP #HOL4 #Math
• Mechanized HOL reasoning in set theory. ~ Simon Guilloud, Sankalp Gambhir, Andrea Gilot & Viktor Kunčak. #ITP #Lisa #Math
• Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. ~ Karol Pąk & Cezary Kaliszyk. #ITP #Mizar #Math
• 15th International Conference on Interactive Theorem Proving (ITP 2024,). #ITP
• The code of Mathematics: Proof and truth ~ Stefan Müller-Stach. #Math
• Neuro-symbolic theorem proving with Lean. ~ Peiyang Song. #ITP #LeanProver #AI #MachineLearning

The readings shared in Mastodon on September 5, 2024 are

• Readings shared September 4, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Haskell #FunctionalProgramming
• Proofs of "0+1+2+3+···+n=n(n + 1)/2" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Lean: First steps (07 - Proof by cases). ~ Tariq Rashid. #ITP #Lean4 #Math
• Logic and proof. ~ Jeremy Avigad, Robert Y. Lewis & Floris van Doorn. #ITP #LeanProver #Lean4 #Logic #Math
• Formalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch & Axel Ljungström.3# #ITP #Agda
• Sized types and coinduction in Safe Agda. ~ Isaac Elliott. #Agda #FunctionalProgramming
• OCaml scientific computing. #OCaml #FunctionalProgramming #AI
• LSP: the good, the bad, and the ugly. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming
• Parsers are relative bimonads. ~ Artemis. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 4, 2024 are

• Readings shared September 3, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Proofs of "If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a)" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Seven levels of type safety in Haskell: Lists. ~ Justin Lê. #Haskell #FunctionalProgramming

The readings shared in Mastodon on September 3, 2024 are

• Readings shared September 2, 2024. #ITP #Lean4 #LeanProver #IsabelleHOL #Coq #Maude #Math #Calculemus #FunctionalProgramming
• Proofs of "If x is the limit of u and y is an upper bound of u, then x ≤ y" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• An exponential improvement for diagonal Ramsey (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Extension of stateful intransitive noninterference with inputs, outputs, and nondeterminism in language IMP. ~ Pasquale Noce. #ITP #IsabelleHOL
• Definitive set semantics for LTL3 (in Isabelle/HOL). ~ Rayhana Amjad, Rob van Glabbeek & Liam O’Connor. #ITP #IsabelleHOL

The readings shared in Mastodon on September 2, 2024 are

• Readings shared September 1, 2024. #ITP #Agda
• Proofs of "If (∀ ε > 0, y ≤ x + ε), then y ≤ x" in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Maude2Lean: Theorem proving for Maude specifications using Lean. ~ Rubén Rubio & Adrián Riesco. #ITP #LeanProver #Maude
• Scaling the evolution of verified software. ~ Kiran Gopinathan. #PhDThesis #ITP #Coq
• Ramsey number bounds (in Isabelle/HOL). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Lean 4.11.0. ~ David Thrane Christiansen. #ITP #Lean4 #FunctionalProgramming

The readings shared in Mastodon on September 1, 2024 are

• Readings shared August 31, 2024. #ITP #Lean4 #IsabelleHOL #Theorema #Coq #Agda #Math #HoTT #Calculemus #PhDThesis
• Modal μ-calculus for free in Agda. ~ Ivan Todorov & Casper Bach Poulsen. #ITP #Agda

The readings shared in Mastodon on August 31, 2024 are

• Readings shared August 30, 2024. #ITP #IsabelleHOL #Agda #Logic #Math #Nix #Haskell #FunctionalProgramming #LogicProgramming
• Proofs of "If x is the supremum of set A, then (∀ y, y < x → ∃ a ∈ A, y < a) in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Unifying model execution and deductive verification with interaction trees in Isabelle/HOL. ~ Simon Foster, Chung-Kil Hur & Jim Woodcock.7# #ITP #IsabelleHOL
• Certification of sorting algorithms using Theorema and Coq. ~ Isabela Drămnesc, Tudor Jebelean & Sorin Stratulat. #ITP #Theorema #Coq
• Investigations in graph-theoretical constructions in Homotopy Type Theory. ~ Jonathan Prieto-Cubides. #PhDThesis #ITP #Agda #HoTT

The readings shared in Mastodon on August 30, 2024 are

• Readings shared August 29, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #Calculemus
• Compactness theorem for propositional logic and combinatorial applications. ~ Fabián Fernando Serran Suárez, Thaynara Arielly de Lima & Mauricio Ayala-Rincón. #ITP #IsabelleHOL #Logic #Math
• Law and order for typestate with borrowing. ~ Hannes Saffrich, Yuki Nishida & Peter Thiemann.1# #ITP #Agda
• Getting started with Nix for Haskell. ~ Abhinav Sarkar. #Nix #Haskell #FunctionalProgramming
• Logic programming with extensible types. ~ Ivan Perez & Angel Herranz. #Haskell #FunctionalProgramming #LogicProgramming

The readings shared in Mastodon on August 29, 2024 are

• Readings shared August 28, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Math #Calculemus #AI
• Proofs of the equivalence of two definitions of the Fibonacci function in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A residual service curve computable in quadratic time for network calculus. ~ Marc Boyer & Pierre Roux. #ITP #Coq
• Modular verification of intrusive list and tree data structures in separation logic. ~ Marc Hermes & Robbert Krebbers. #ITP #Coq

The readings shared in Mastodon on August 28, 2024 are

• Readings shared August 27, 2024. #ITP #IsabelleHOL #Math
• Proofs of "flatten (mirror a) = reverse (flatten a)" in Lean4 and Isabelle/HOL. ~ José A. Alonso. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Formalizing Mason-Stothers theorem and its corollaries in Lean 4. ~ Jineon Baek & Seewoo Lee. #ITP #LeanProver #Lean4 #Math
• On the maximum weighted irredundant set problem. ~ Ricardo D. Katz & Daniel Severín. #ITP #Coq #Math
• Compositional verification of composite byzantine protocols. ~ Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey. #ITP #Coq
• The top 100 gen AI consumer apps. ~ Olivia Moore. #AI
• Conocimientos de sentido común: el obstáculo de la IA en el camino hacia la inteligencia artificial general. ~ Ramón López de Mántaras. #IA
• Las herramientas de IA que están captando la atención de la gente. ~ @Alvy #IA
• L’intelligence artificielle : Hier, aujourd’hui … et demain. ~ Jean-Paul Haton. #AI

The readings shared in Mastodon on August 27, 2024 are

• Readings shared August 26, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Prolog #LogicProgramming
• Topological groups (in Isabelle/HOL). ~ Niklas Krofta. #ITP #IsabelleHOL #Math
• Difference bound matrices (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 26, 2024 are

• Proofs that the mirror function of binary trees is involutive in Lean4 and Isabelle/HOL. ~ José A. Alonso. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalized programming language with speculative execution. ~ Jamie Wright & Andrei Popescu. #ITP #IsabelleHOL
• Game programming in Prolog (Part 1). ~ Youngjin Kang. #Prolog #LogicProgramming

The readings shared in Mastodon on August 24, 2024 are

• Readings shared August 23, 2024. #ITP #IsabelleHOL #LeanProver #Lean4 #AI #DeepLearning #Haskell #FunctionalProgramming #LogicProgramming #Python
• Logic and computation intertwined. ~ Prabhakar Ragde. #Logic #Racket #ITP #Coq #Agda
• Tipos dependientes: λP. ~ Juan Pablo Yamamoto Zazueta. #TypeTheory #CurryHoward

The readings shared in Mastodon on August 23, 2024 are

• Readings shared August 22, 2024. #ITP #Agda #HoTT #Haskell #FunctionalProgramming
• Lean: First steps (06 - Intermediate results). ~ Tariq Rashid. #ITP #Lean4 #Math
• How to make mathematicians into programmers (and vice versa). ~ Will Crichton. #ITP #LeanProver #Math
• Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. ~ Lawrence C Paulson. #ITP #HOL
• Coproduct measure (in Isabelle/HOL). ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang & Xujie Si. #AI #DeepLearning #ITP
• Property-based testing for the people. ~ Harrison Goldstein. #PhDThesis #Haskell #FunctionalProgramming
• Boolean matrix logic programming. ~ Lun Ai & Stephen H. Muggleton. #LogicProgramming
• Ordinals aren't much worse than Quaternions. ~ Philip Zucker. #Python #Math

The readings shared in Mastodon on August 22, 2024 are

• Readings shared August 21, 2024. #ITP #IsabelleHOL #Lean4 #Math #FunctionalProgramming
• Terminal coalgebras and non-wellfounded sets in Homotopy Type Theory. ~ Håkon Robbestad Gylterud, Elisabeth Stenholm & Niccolò Veltri. #ITP #Agda #HoTT
• Prettier. Happier. More Imperative. (Understanding "A prettier printer" by porting it). ~ Benjamin Hodgson. #Haskell #FunctionalProgramming

The readings shared in Mastodon on August 21, 2024 are

• Readings shared August 20, 2024. #ITP #Lean4 #Coq #ACL2 #AlphaProof #Math #Haskell #FunctionalProgramming #Logic #Math #CategoryTheory #TypeTheory
• Probabilistic reasoning and formal proof. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto. #Lean4 #FunctionalProgramming
• Worklist algorithms (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL
• Trustworthy verification of realtime systems. ~ Simon Wimmer. #ITP #IsabelleHOL
• Verified model checking of timed automata. ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 20, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Calculemus
• Improving on AlphaProof: IMO 2024 problem 2 in Lean 4. ~ David Renshaw. #ITP #Lean4 #Math #AlphaProof
• Verification and attack synthesis for network protocols. ~ Max von Hippel. #ITP #ACL2
• A two-phase infinite/finite low-level memory model (Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction). ~ Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski & Steve Zdancewic. #ITP #Coq
• Snapshoble stores. ~ Clément Allain, Basile Clément, Alexandre Moine & Gabriel Scherer. #ITP #Coq
• Refinement composition logic. ~ Youngju Song & Dongjae Lee. #ITP #Coq
• Beyond trees: Calculating graph-based compilers (Functional pearl). ~ Patrick Bahr & Graham Hutton. #Haskell #FunctionalProgramming
• An introduction to categorical proof theory. ~ Amirhossein Akbar Tabatabai. #Logic #Math #CategoryTheory #TypeTheory

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #FunctionalProgramming #Math #Prolog #LogicProgramming
• Proofs of the equivalence of reverse definitions in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalisation of the Mathieu-24 group. ~ Edward van de Meent. #ITP #LeanProver #Lean4 #Math

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 17, 2024. #ITP #LeanProver #Lean4 #Math #AI
• How the Lean language brings math to coding and coding to math. ~ Leo de Moura. #ITP #LeanProver #Math
• Lean again. ~ Adolfo Neto. #ITP #Lean4 #FunctionalProgramming
• The semantics of metapropramming in Prolog. ~ David S. Warren. #Prolog #LogicProgramming

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 15, 2024. #ITP #IsabelleHOL #Coq #SSReflect #Math #Haskell #Elm #FunctionalProgramming
• Machine-checked proofs and the rise of formal methods in mathematics. ~ Leonardo de Moura. #ITP #LeanProver #Math
• DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. ~ Huajian Xin et als. #ITP #Lean4
• The AI scientist: Towards fully automated open-ended scientific discovery. ~ Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune & David Ha. #AI