iiinova — where your digital self keeps evolving

Pietro Monticone

@pietromonticone.bsky.social

AI for Mathematics @HarmonicMath || Formalising Mathematics and Software in @LeanProver || Developing Free Open Source Software in #Lean, #Python and #Julia.

Posts Replies Media

Pietro Monticone @pietromonticone.bsky.social · 07/04/2026

AI is increasingly changing how we do mathematics. Erdős Problem #650, open for over 60 years, was solved a few weeks ago through a collaboration between human mathematicians, an informal reasoning model (GPT 5.4 Pro @OpenAI) and a formal one (Aristotle @harmonic.fun). 🧵

221

Pietro Monticone @pietromonticone.bsky.social · 11/12/2025

Day 3 at #ItaLean2025 here in Bologna! Great talks this morning and now the project work session is buzzing: so many new ideas everywhere and exciting collaborative projects taking shape. What a fantastic atmosphere! @lean-lang.org #FormalMath #AI4Math

020

Pietro Monticone @pietromonticone.bsky.social · 14/10/2025

We’re pleased to announce #ItaLean2025: Bridging Formal Mathematics and AI, an international conference dedicated to @lean-lang.org, Formal Mathematics, and AI4Math. 📍 University of Bologna 🗓 9–12 December 2025 Proudly supported by #Harmonic. #LeanLang #FormalMath #AI4Math

143

Reposted by Pietro Monticone

Adam Marblestone @adammarblestone.bsky.social · 09/10/2025

I have never seen a better conference name

1121

Reposted by Pietro Monticone

xenaproject.bsky.social @xenaproject.bsky.social · 09/10/2025

ItaLean : formal maths and AI in Italy (Bologna), Dec 2025. Lectures, hands-on tutorials, research talks from academia and industry etc. Register here pitmonticone.github.io/ItaLean2025/

pitmonticone.github.io

ItaLean 2025

083

Pietro Monticone @pietromonticone.bsky.social · 12/05/2025

A very nice article in @quantamagazine.bsky.social mentions our #EquationalTheories project, led by @teorth.bsky.social, which aims to advance collaborative mathematical research through the synergy of human researchers, interactive proof assistants and automated theorem provers. shorturl.at/RCgCq

shorturl.at

Mathematical Beauty, Truth and Proof in the Age of AI | Quanta Magazine

Mathematicians have started to prepare for a profound shift in what it means to do mathematics.

011