Readings shared April 9, 2026
The readings shared in Bluesky on 9 April 2026 are:
- ABC implies that Ramanujan's tau function misses almost all primes. ~ David Kurniadi Angdinata et als. #LeanProver #ITP #Math
- Do we need frontier models to verify mathematical proofs?. ~ Aaditya Naik, Guruprerana Shabadi, Rajeev Alur, Mayur Naik. #AI4Math #LeanProver #ITP
- Automatic textbook formalization. ~ Fabian Gloeckle, Ahmad Rammal, Charles Arnal, Remi Munos, Vivien Cabannes, Gabriel Synnaeve, Amaury Hayat. #AI4Math #LeanProver #ITP
- Making written theorems explorable by grounding them in formal representations. ~ Hita Kambhamettu, Will Crichton, Sean Welleck, Harrison Goldstein, Andrew Head. #AI4Math #LeanProver #ITP
- Automated conjecture resolution with formal verification. ~ Haocheng Ju et als. #AI4Math #ITP #LeanProver
- Formalizing CHSH rigidity in Lean 4. ~ Tianrun Zhao, Nengkun Yu. #LeanProver #ITP
- A prime-generated formalization of Nagata's factoriality theorem in Lean 4. ~ Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. #LeanProver #ITP #Math
- A taste of LeanLang. ~ Siddhartha Gadgil. #LeanProver #ITP #FunctionalProgramming
- SAT is not solvable in constant time (in Isabelle/HOL). ~ Daniel Shea. #IsabelleHOL #Math
- Theory X cannot exist: Machine-verified impossibility theorems in population ethics. ~ Julian L. Voigt. #IsabelleHOL #ITP
- Abstract consistency properties (in Isabelle/HOL). ~ Asta Halkjær From, Anders Schlichtkrull. #IsabelleHOL #ITP
- A graded modal dependent type theory with erasure, formalized. ~ Andreas Abel, Nils Anders Danielsson, Oskar Eriksson. #Agda #ITP
- An optimal 14-symbol hybrid basis for BCH-algebras. ~ Mahesh Ramani, Shlok Kumar. #Prover9 #ATP #Math
- QED-Nano: Teaching a tiny model to prove hard theorems. ~ LM-Provers, Yuxiao Qu, Amrith Setlur, Jasper Dekoninck, Edward Beeching, Jia Li, Ian Wu, Lewis Tunstall, Aviral Kumar. #AI4Math
- Artificial intelligence and the structure of mathematics. ~ Maissam Barkeshli, Michael R. Douglas, Michael H. Freedman. #AI4Math
- Short proofs in combinatorics, probability and number theory II. ~ Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant. #AI4Math
- Mathematical methods and human thought in the age of AI. ~ Terence Tao, Tanya Klowden. #AI #Math