The readings shared in Bluesky on 4 April 2026 are:

• Why Lean?. ~ Leonardo de Moura. #LeanProver #ITP
• A formalization of the Gelfond-Schneider theorem. ~ Michail Karatarakis, Freek Wiedijk. #LeanProver #ITP #Math
• Formalizing Pick's theorem, efficiently. ~ Michael Eisermann. #LeanProver #ITP #Math
• Lean on Vampire proofs (short paper). ~ Jonas Bodingbauer, Márton Hajdu, Laura Kovács, Axel Polaczek, Michael Rawson. #LeanProver #ITP #Vampire #ATP
• La IA acaba de hacerle una pregunta incómoda a la física teórica. Qué pasa si algunos de sus resultados más citados nunca fueron tan sólidos como parecían. ~ Martín Nicolás Parolari. #LeanProver
• Type-checked compliance: Deterministic guardrails for agentic financial systems using Lean 4 theorem proving. ~ Devakh Rashie, Veda Rashi. #LeanProver #ITP #LLMs
• Physics as code: From scans to theorems with ITP APIs in SU(5) model building. ~ Sven Krippendorf, Joseph Tooby-Smith. #LeanProver #ITP #Physics
• Pairwise independence of representation, classification, and composition in finite extensional magmas. ~ Stefano Palmieri. #ITP #LeanProver
• Optimal bounds for an Erdős problem on matching integers to distinct multiples. ~ Wouter van Doorn, Yanyang Li, Quanyu Tang. #AI4Math #LeanProver #ITP #LLMs
• Coherence for asynchronous buffered MPST: A mechanized metatheory. ~ Sam Hart Berman. #LeanProver #ITP #Physics
• Computable dynamics for asynchronous MPST: Lyapunov descent, critical capacity, and decision procedures. ~ Sam Hart Berman. #LeanProver #ITP #Physics
• Harmony from coherence in asynchronous MPST: A minimal erasure invariant for classical dynamics. ~ Sam Hart Berman. #LeanProver #ITP #Physics
• On the formalization of network topology matrices in HOL. ~ Kubra Aksoy, Adnan Rashid, Osman Hasan, Sofiene Tahar. #ISabelleHOL #ITP #Math
• Putnam 2025 problems in Rocq using Opus 4.6 and Rocq-MCP. ~ Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot. #RocqProver #AI4Math
• Representing graphs in Prolog. ~ Markus Triska. #Prolog #LogicProgramming
• Encodings into the λ-calculus. ~ Kristopher Micinski. #LambdaCalculus #Racket #FunctionalProgramming
• What Gödel discovered. ~ Stepan Parunashvili. #Logic #Math #Lisp #Programming
• This startup wants to change how mathematicians do math. ~ Will Douglas Heaven. #AI4Math
• Short proofs in combinatorics and number theory. ~ Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, Gregory Valiant. #AI4Math
• How effective are current AI models on mathematical research problems?. ~ David H Bailey. #AI4Math
• Mathematical methods and human thought in the age of AI. ~ Tanya Klowden, Terence Tao. #AI #Math
• Category theory illustrated: Types. ~ Jencel Panic. #CategoryTheory #Math
• Reseña de 'LeanTutor: A formally-verified AI tutor for mathematical proofs'. #ITP #LeanProver #Math #AIforMath #Teaching
• Reseña de «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?». #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath
• Reseña de «Mathesis: Towards formal theorem proving from natural languages». #AI #LLMs #Math #ITP #LeanProver #AIforMath
• Reseña de «Hardest problems in mathematics, physics & the future of AI». #ITP #LeanProver #AI #Math #AIforMath
• Reseña de «Hablemos de Lisp». #Lisp #FunctionalProgramming
• Reseña de «Diophantine equations over Z: Universal bounds and parallel formalization». #ITP #IsabelleHOL #Math
• Reseña de «Solving formal math problems by decomposition and iterative reflection». #AI4Math #LLMs #ProofAssistants #LeanProver #Math
• Reseña de «The Infinity Project (How to use AI and mathematics to prove and improve science and security)». #AI #Math #ITP #LeanProver
• Reseña de «Olympiad-level formal mathematical reasoning with reinforcement learning». #AI #Math #ITP #LeanProver #AlphaProof
• Reseña de «DeepMind’s latest: An AI for handling mathematical proofs». #AI #Math #ITP #LeanProver #AlphaProof
• Reseña de «Formalization of Erdős problems». #ITP #LeanProver #Math #Autoformalization
• Reseña de «Machine assistance and the future of research mathematics». #AI4Math
• Reseña de «Machine assistance and the future of research mathematics». #AI4Math
• Reseña de «AI that can prove it’s right: Verification as the missing layer in AI». #AI4Math #LeanProver
• Reseña de «Completing the formal proof of higher-dimensional sphere packing». #AI4Math
• Reseña de «Shaping the future of mathematics in the age of AI». #AI4Math
• Reseña de «AI for mathematical and scientific discovery». #AI4Math
• Reseña de «Mathematicians in the age of AI». #AI4Math
• Reseña de «Coding after coders: The end of computer programming as we know it». #AI #Programming
• Reseña de «Eval awareness in Claude Opus 4.6’s BrowseComp performance». #AI
• Reseña de «Formal verification and AI are reshaping mathematical research». #AI4Math #ITP #LeanProver
• Reseña de «In math, rigor is vital. But are digitized proofs taking it too far?». #AI4Math #LeanProver #ITP
• Reseña de «Can machines do mathematics?». #AI4Math #LeanProver #ITP
• Reseña de «Advancing mathematics by guiding human intuition with AI». #AI4Math
• Reseña de «Shaping the future of mathematics in the age of AI». #AI4Math #LeanProver #ITP
• Reseña de «What happens when AI starts checking mathematicians’ work». #AI4Math #ITP #LeanProver
• Reseña de «As AI keeps improving, mathematicians struggle to foretell their own future». #AI4Math
• Reseña de «Mathematics in the library of Babel». #AI4Math
• Reseña de «Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools». #AI4Math
• Reseña de «This startup wants to change how mathematicians do math». #AI4Math
• Reseña de «La IA acaba de hacerle una pregunta incómoda a la física teórica. Qué pasa si algunos de sus resultados más citados nunca fueron tan sólidos como parecían». #LeanProver #ITP
• Reseña de «Short proofs in combinatorics and number theory». #AI4Math
• Reseña de «Mathematical methods and human thought in the age of AI». #AI4Math
• Reseña de «Mathematicians in the age of AI». #AI4Math
• Reseña de «AI for mathematical and scientific discovery». #AI4Math
• Reseña de «Accelerating mathematics». #AI4Math #LeanProver
• Reseña de «AI that can prove it’s right: Verification as the missing layer in AI». #AI4Math #LeanProver
• Reseña de «Type-checked compliance: Deterministic guardrails for agentic financial systems using Lean 4 theorem proving». #LeanProver
• Reseña de «What Gödel discovered». #Logic #Math #Lisp #Programming
• Reseña de «Why Lean?». #LeanProver #ITP #FunctionalProgramming
• Reseña de «DeepSeek-Prover-V2-7B bridges the gap between mathematical thought and formal code». #AI4Math #LeanProver
• Reseña de «Recent advances in LLMs for mathematics». #AI4Math
• Reseña de «Aristotle, an AI theorem prover using Lean». #AI4Math #LeanProver
• Reseña de «Sobre la resolución de problemas de Erdös usando inteligencia artificial generativa». #AI4Math
• Reseña de «The story of Erdős problem #1026». #AI4Math
• Reseña de «50 years of proof assistants». #ITP #IsabelleHOL #LeanProver #CoqProver
• Reseña de «Teaching real analysis as a game»". #LeanProver #ITP #Math
• Reseña de «How we achieved an IMO medal, one year before any other AI system». #AI #Math #ITP #LeanProver #AlphaProof
• Reseña de «A new paradigm for mathematical proof?». #Math #ITP #LeanProver #Agda