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