Lorenzo Luccioli

PhD Student in Mathematics at the University of Bologna since 2024, I conduct research in artificial intelligence applied to automated reasoning and the formalization of mathematics, with a particular focus on the use of the theorem prover Lean 4, under the supervision of Prof. Giovanni Paolini.

I have collaborated on various formalization projects in Lean, including Testing Lower Bounds, PFR, and Equational Theories, and contributed to the mathematical library Mathlib.

Since 2025, I have been collaborating with Harmonic as a Part-time Lean Expert.