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