Readings shared September 17, 2025
The readings shared in Bluesky on 17 September 2025 are:
- Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin, Colin Jones, John Velkey, Tyler R. Josephson. #ITP #LeanProver
- Claude can (sometimes) prove it. ~ Mike Dodds. #ITP #LeanProver #Math #AI #LLMs #Claude
- Structuring definitions in mathematical libraries. ~ Alena Gusakov, Peter Nelson, Stephen Watt. #ITP #LeanProver #Math
- A blueprint for the formalization of Carleson’s theorem on convergence of Fourier series. ~ Lars Becker et als. #ITP #LeanProver #Math
- Formalization of the internal language of a topos. ~ Johannes Folttmann. #ITP #LeanProver #Math
- The meta-principle: A tautological foundation for physics. ~ Jonathan Washburn. #ITP #LeanProver #Physics
- Łukasiewicz logic with actions for neural networks training. ~ Ioana Leuştean, Bogdan Macovei. #ITP #LeanProver
- Towards automated mathematical discovery. ~ Aaron Courville, Navin Goyal. #AI #Math #LLMs #ITP #LeanProver
- Sketchpad: A high-precision and easy-to-use system for automatic formal sketch generation. ~ Wenda Li, Luo Mai, Larry Paulson, Huajian Xin. #AI #Math #ITP #IsabelleHOL #LeanProver
- Scalable theorem proving via mathematical databases. ~ Christopher Birkbeck, David Roe, Andrew Sutherland. #AI #Math #ITP #LeanProver
- Learning to do math with vampires and spiders. ~ Andrei Voronkov, Michael Rawson. #ITP #LeanProver #Rocq
- GNN-SMT: A consortium based proof automation for Lean 4. ~ Clark Barrett, Leni Aniva, Abdalrhman Mohamed, Harun Khan. #ITP #LeanProver #SMT
- Game over or QED? (For taking the Lean Game Server to the next level). ~ Marcus Zibrowius. #ITP #LeanProver
- Domain specific (Documentation for Mathlib). ~ John Talbot, Richard M. Hill. #ITP #LeanProver #Mathlib
- Document-level autoformalization. ~ Antoine Bosselut, Viktor Kunčak, Maryna Viazovska. #AI #Math #ITP #LeanProver #Autoformalization
- Databases of structured motivated proofs. ~ Timothy Gowers, Anand Rao, Anshula Gandhi, Jacob Loader, Jovan Gerbscheid, Jonas Bayer. #AI #Math #ITP #LeanProver
- 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. #AI #Math #LLMs #ITP #LeanProver #Autoformalization
- Bridging proof and computation (For a verified Lean–Macaulay2 interface). ~ Matthew Ballard, Anton Leykin, Damiano Testa, Michael Stillman. #AI #Math #ITP #LeanProver #CAS #Macaulay2
- A structured representation of tactics for machine-assisted theorem proving. ~ Jade Master, Vincent Wang-Maścianica, Zanzi Mihejevs, Bruno Gavranović, Andre Videla, Dylan Braithwaite. #AI #Math #ITP #LeanProver
- A dataset of modern formalized theorem statements. ~ Kevin Buzzard. #ITP #LeanProver #Math
- An AI-focused tactic for language learning. ~ Robert Y. Lewis. #AI #Math #ITP #LeanProver
- Quantum structures and functional programming. ~ Jerzy Karczmarczuk. #Haskell #FunctionalProgramming
- Plinth: A plugin-powered language built on Haskell (Experience report). ~ Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones, Philip Wadler, Manuel Chakravarty. #Haskell #FunctionalProgramming