Pietro Monticone
@pietromonticone.bsky.social
Informal Mathematics @UniTrento || Formal Mathematics @Harmonic || Formalising in #Lean || Developing #FOSS in #Python and #Julia || Forecasting @Metaculus.
• GitHub: https://github.com/pitmonticone
• YouTube: https://www.youtube.com/@PietroMonticone
• GitHub: https://github.com/pitmonticone
• YouTube: https://www.youtube.com/@PietroMonticone
Pinned
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
📍 University of Bologna
🗓 9–12 December 2025
Proudly supported by #Harmonic.
#LeanLang #FormalMath #AI4Math
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
📍 University of Bologna
🗓 9–12 December 2025
Proudly supported by #Harmonic.
#LeanLang #FormalMath #AI4Math
October 14, 2025 at 7:44 AM
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
📍 University of Bologna
🗓 9–12 December 2025
Proudly supported by #Harmonic.
#LeanLang #FormalMath #AI4Math
Reposted by Pietro Monticone
I have never seen a better conference name
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/
ItaLean 2025
pitmonticone.github.io
October 9, 2025 at 3:23 PM
I have never seen a better conference name
Reposted by Pietro Monticone
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/
ItaLean 2025
pitmonticone.github.io
October 9, 2025 at 12:31 PM
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/
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
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.
shorturl.at
May 12, 2025 at 10:29 PM
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