Lorenzo Luccioli

Dottorando in Matematica presso l’Università di Bologna dal 2024, svolgo la mia ricerca nell’ambito dell’intelligenza artificiale applicata al ragionamento automatico e alla formalizzazione della matematica, con particolare focus sull’uso del theorem prover Lean 4, sotto la supervisione del prof. Giovanni Paolini.

Ho collaborato a diversi progetti di formalizzazione in Lean, tra cui Testing Lower Bounds, PFR ed Equational Theories, oltre ad aver contribuito alla libreria matematica Mathlib.

Dal 2025 collaboro con Harmonic come Part-time Lean Expert.