#Exercitium: Producto cartesiano de una familia de conjuntos. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

AWS scientist: Your AI strategy needs mathematical logic. ~ Byron Cook. fortune.com/2025/09/20/a... #AI #LLMs #Logic #Math #ATP #ITP

Feeling cranky about AI and CS education. ~ Valerie Barr. cacm.acm.org/blogcacm/fee... #AI #CompSci #Education

Lean-auto: An interface between Lean 4 and automated theorem provers (video). ~ Yicheng Qian, Joshua Clune, Clark Barrett, Jeremy Avigad. youtu.be/_ExTLAXDTSQ #ITP #LeanProver #ATP #SMT

Determination of the fifth Busy Beaver value. ~ Justin Blanchard et als. arxiv.org/abs/2509.123... #ITP #CoqProver #Rocq

Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin et als. arxiv.org/abs/2509.131... #ITP #LeanProver

Discovering new theorems via LLMs with in-context proof learning in Lean. ~ Kazumi Kasaura et als. arxiv.org/abs/2509.142... #ITP #LeanProver #Math #LLMs

Refinement-types driven development: A study. ~ Facundo Domínguez, Arnaud Spiwack. arxiv.org/abs/2509.150... #FunctionalProgramming #Liquid #Haskell #SMT

Computationally-sound symbolic cryptography in Lean. ~ Stefan Dziembowski et als. eprint.iacr.org/2025/1700.pdf #ITP #LeanProver

Formal verification of the Euler Sieve via Lean. ~ Isaac (Rucheng) Li. pimr.pitt.edu/pimr/article... #ITP #LeanProver #Math

"Si hay algo en nosotros verdaderamente divino, es la voluntad. Por ella afirmamos la personalidad, templamos el carácter, desafiamos la adversidad, reconstruimos el cerebro y nos superamos diariamente." ~ Santiago Ramón y Cajal (1952-1934).

"Una de las desdichas de nuestro país consiste, como se ha dicho hartas veces, en que el interés individual ignora el interés colectivo." ~ Santiago Ramón y Cajal (1952-1934).

Readings shared September 20, 2025. jaalonso.github.io/vestigium/po... #AI #ATP #FormalVerification #FunctionalProgramming #ITP #LeanProver #Logic #LogicProgramming #Math

Everything you know is wrong. ~ Lawrence Paulson. lawrencecpaulson.github.io/2025/09/20/W... #AI #Logic #ATP #ITP #FunctionalProgramming #LogicProgramming #FormalVerification

An introduction to formal real analysis (Lecture 5: Doubling a convergent sequence). ~ Alex Kontorovich. youtu.be/MSp48lKUOGY #ITP #LeanProver #Math

An introduction to formal real analysis (Lecture 4: Non-convergence of (-1)^n, triangle inequality). ~ Alex Kontorovich. youtu.be/p2Q4Vgn0QB0 #ITP #LeanProver #Math

"Urge volver a creer en el mundo, en la humanidad." ~ Stefan Zweig (1881-1942).

Readings shared September 19, 2025. jaalonso.github.io/vestigium/po... #Agda #CoqProver #ITP #Idris2 #LeanProver #Rocq

Mechanizing the meta-theory of session types in Rocq: A tutorial. ~ Marco Carbone, Alberto Momigliano. momigliano.di.unimi.it/papers/stuto... #ITP #Rocq

The conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. szumixie.github.io/docs/papers/... #ITP #Agda

Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir. Alex Kontorovich, Heather MacBeth. leanprover-community.github.io/blog/posts/s... #ITP #LeanProver

The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction. ~ Arnaud Mayeux, Jujian Zhang. arxiv.org/abs/2509.15116 #ITP #LeanProver

Theorem provers: One size fits all? ~ Harrison Oates, Hyeonggeun Yun, Nikhila Gurusinghe. arxiv.org/abs/2509.15015 #ITP #CoqProver #Idris2

The groupoid-syntax of type theory is a set. ~ Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie. arxiv.org/abs/2509.14988 #ITP #Agda

"Todo está perdido cuando los malos sirven de ejemplo y los buenos de mofa." ~ Demócrito (-460, -370).

Readings shared September 18, 2025. jaalonso.github.io/vestigium/po... #AI #ATP #Dedukti #FunctionalProgramming #Haskell #ITP #LLMs #Vampire

#Exercitium: Código Morse. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional

Gemini AI solves coding problem that stumped 139 human teams at ICPC World Finals (Gemini shows off at another high-level academic competition). ~ Ryan Whitwam. arstechnica.com/google/2025/... #AI #LLMs #Gemini #Programming

Case study: Verified Vampire proofs in the lambdapi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suda. arxiv.org/abs/2503.15541 #ATP #Vampire #ITP #Dedukti

"La felicidad reside en los gustos y no en las cosas; somos felices cuando tenemos lo que nos gusta y no cuando tenemos lo que los demás encuentran agradable." ~ François de La Rochefoucauld (1613-1680).

Readings shared September 17, 2025. jaalonso.github.io/vestigium/po... #AI #Autoformalization #CAS #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Macaulay2 #Math #Mathlib #Physics #Rocq #SMT

🎉 Lean 4.23.0 is here! Includes many usability improvements, including: 🎯 Enhanced 'Go to Definition' supporting type class instances 🔧 Interactive error hints for faster debugging Release notes: lean-lang.org/doc/referenc... #LeanLang #LeanProver #OpenSource #Mathematics #FormalVerification

Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin, Colin Jones, John Velkey, Tyler R. Josephson. arxiv.org/abs/2509.13142 #ITP #LeanProver

Claude can (sometimes) prove it. ~ Mike Dodds. www.galois.com/articles/cla... #ITP #LeanProver #Math #AI #LLMs #Claude

An AI-focused tactic for language learning. ~ Robert Y. Lewis. www.renaissancephilanthropy.org/an-ai-focuse... #AI #Math #ITP #LeanProver

A dataset of modern formalized theorem statements. ~ Kevin Buzzard. www.renaissancephilanthropy.org/a-dataset-of... #ITP #LeanProver #Math

A structured representation of tactics for machine-assisted theorem proving. ~ Jade Master, Vincent Wang-Maścianica, Zanzi Mihejevs, Bruno Gavranović, Andre Videla, Dylan Braithwaite. www.renaissancephilanthropy.org/a-structured... #AI #Math #ITP #LeanProver

Bridging proof and computation (For a verified Lean–Macaulay2 interface). ~ Matthew Ballard, Anton Leykin, Damiano Testa, Michael Stillman. www.renaissancephilanthropy.org/bridging-pro... #AI #Math #ITP #LeanProver #CAS #Macaulay2

Constraining LLMs for theorem proving (A neurosymbolic approach to guaranteed autoformalization). ~ Eleonora Giunchiglia, Sam Adam-Day, Joshua Ong, Mihaela Cătălina Stoian, Luca Andolfi. www.renaissancephilanthropy.org/constraining... #AI #Math #LLMs #ITP #LeanProver #Autoformalization

Databases of structured motivated proofs. ~ Timothy Gowers, Anand Rao, Anshula Gandhi, Jacob Loader, Jovan Gerbscheid, Jonas Bayer. www.renaissancephilanthropy.org/databases-of... #AI #Math #ITP #LeanProver

Document-level autoformalization. ~ Antoine Bosselut, Viktor Kunčak, Maryna Viazovska. www.renaissancephilanthropy.org/document-lev... #AI #Math #ITP #LeanProver #Autoformalization

Domain specific (Documentation for Mathlib). ~ John Talbot, Richard M. Hill. www.renaissancephilanthropy.org/domain-speci... #ITP #LeanProver #Mathlib

Game over or QED? (For taking the Lean Game Server to the next level). ~ Marcus Zibrowius. www.renaissancephilanthropy.org/game-over-or... #ITP #LeanProver

GNN-SMT: A consortium based proof automation for Lean 4. ~ Clark Barrett, Leni Aniva, Abdalrhman Mohamed, Harun Khan. www.renaissancephilanthropy.org/gnn-smt-cons... #ITP #LeanProver #SMT

Learning to do math with vampires and spiders. ~ Andrei Voronkov, Michael Rawson. www.renaissancephilanthropy.org/learning-to-... #ITP #LeanProver #Rocq

Scalable theorem proving via mathematical databases. ~ Christopher Birkbeck, David Roe, Andrew Sutherland. www.renaissancephilanthropy.org/scalable-the... #AI #Math #ITP #LeanProver

Sketchpad: A high-precision and easy-to-use system for automatic formal sketch generation. ~ Wenda Li, Luo Mai, Larry Paulson, Huajian Xin. www.renaissancephilanthropy.org/sketchpad-a-... #AI #Math #ITP #IsabelleHOL #LeanProver

Towards automated mathematical discovery. ~ Aaron Courville, Navin Goyal. www.renaissancephilanthropy.org/towards-auto... #AI #Math #LLMs #ITP #LeanProver

The meta-principle: A tautological foundation for physics. ~ Jonathan Washburn. recognitionphysics.org/meta-princip... #ITP #LeanProver #Physics

Formalization of the internal language of a topos. ~ Johannes Folttmann. florisvandoorn.com/theses/Johan... #ITP #LeanProver #Math