The readings shared in Bluesky on 13 June 2025 are

• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• Formal verification of relational algebra transformations in Fiat2 using Coq. ~ Christian Teshome. #ITP #CoqProver #Rocq
• Growing a modular framework for modal systems - HOLMS: a HOL Light library. ~ Antonella Bilotta. #ITP #HOL_Light #Logic #Math
• Trinity: an autoformalization system for verified superintelligence. #Autoformalization #AIforMath #ITP #LeanProver
• The abc conjecture almost always — autoformalized. ~ Jesse Michael Han et als. #Autoformalization #AIforMath #ITP #LeanProver
• MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems? ~ Zhitao He et als. #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath
• Mathesis: Towards formal theorem proving from natural languages. ~ Yu Xuejun et als. #AI #LLMs #Math #ITP #LeanProver #AIforMath
• StepProof: Step-by-step verification of natural language mathematical proofs. ~ Xiaolin Hu, Qinghua Zhou, Bogdan Grechuk, Ivan Y. Tyukin. #LLMs #ITP #IsabelleHOL #Math #AIforMath
• 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