Lmst

Accelerating mathematics. ~ Kevin Buzzard. https://xenaproject.wordpress.com/2026/02/09/accelerating-mathematics/ #AI4Math #ITP #LeanProver

Evaluating Large Language Models on solved and unsolved problems in graph theory: Implications for computing education. ~ Adithya Kulkarni, Mohna Chakraborty, Jay Bagga. https://arxiv.org/abs/2602.05059v1 #AI4Math

Semi-autonomous mathematics discovery with Gemini: A case study on the Erdős problems. ~ Tony Feng et als. https://arxiv.org/abs/2601.22401v1 #AI4Math #ITP #LeanProver

Recent advances in LLMs for mathematics. ~ Sebastien Bubeck. https://youtu.be/MH3lG7V7SuU #AI4Math

LeanArchitect: Automating blueprint generation for humans and AI. ~ Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck. https://arxiv.org/abs/2601.22554v1 #AI4Math #ITP #LeanProver

Irrationality of rapidly converging series: a problem of Erdős and Graham. ~ Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovač, Shengtong Zhang. https://arxiv.org/abs/2601.21442 #AI4Math

Flow-based extremal mathematical structure discovery. ~ Gergely Bérczi, Baran Hashemi, Jonas Klüver. https://arxiv.org/abs/2601.18005v1 #AI4Math

Construction-verification: A benchmark for applied mathematics in Lean 4. ~ Bowen Yang et als. https://arxiv.org/abs/2602.01291v1 #AI4Math #ITP #LeanProver

Readings shared January 29, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/30-readings_shared_01-29-26 #AI #AI4Math #FunctionalProgramming #Hakell #ITP #IsabelleHOL #LLMs #LeanProver #Math

Aristotle, an AI theorem prover using Lean. ~ Alex Best. https://youtu.be/XmD-Vl2iiqM #AI #Math #AI4Math #ITP #LeanProver #Aristotle

Thinking machines: Mathematical reasoning in the age of LLMs. ~ Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen. https://arxiv.org/abs/2508.00459 #AI #Math #AI4Math #LLMs

LeanTutor: Towards a verified AI mathematical proof tutor. ~ Manooshree Patel, Rayna Bhattacharyya, Thomas Lu, Arnav Mehta, Niels Voss, Narges Norouzi, Gireeja Ranade. https://arxiv.org/abs/2601.17473v1 #AI #Math #AI4Math #ITP #LeanProver #LLMs

Readings shared January 24, 2026. https://jaalonso.github.io/vestigium/posts/2026/01/25-readings_shared_01-24-26 #AI #AI4Math #ATP #CoqProver #HOL_Light #ITP #IsabelleHOL #LeanProver #Logic #Math #Prover9 #RocqProver

AI for mathematics: Progress, challenges, and prospects. ~ Haocheng Ju, Bin Dong. https://arxiv.org/abs/2601.13209v2 #AI #Math #AI4Math #ITP #IsabelleHOL #CoqProver #LeanProver

We’re pleased to announce #ItaLean2025: Bridging Formal Mathematics and AI, an international conference dedicated to @leanprover, Formal Mathematics, and AI4Math.

📍 University of Bologna
🗓 9–12 December 2025

#ItaLean2025 brings together researchers and practitioners advancing the formalization of mathematics in Lean and exploring the interplay between machine learning and formal methods.

The program includes lectures, tutorials, research talks, product demos, and a concluding panel.

Applications to participate are now open.
Participation is free of charge.

A limited amount of travel support may be available.
Priority deadline: 31 October 2025.

A preliminary schedule will be released in the coming weeks, with regular updates to follow.

Official website (applications, program, logistics): https://pitmonticone.github.io/ItaLean2025/

#LeanLang #FormalMath #AI4Math