CS student at the University of Naples Federico II and AI researcher at Project Numina, where I work on automating mathematics and autoformalization with Numina Fuse. I worked on Numina's public Lean 4 formalization of the three-dimensional Kakeya conjecture. I also work on automated theorem proving, model checking, and formal logic.
Open to internship and research opportunities.
I contribute to automated reasoning tools:
- Vampire, the first-order theorem prover: 8 merged PRs, including fixes for a wrong answer from
-newcnfon two Boolean$lets (#894), a parser crash on Boolean$let(#885) and proof output in the wrong TPTP fragment (#884), plus a staged refactor that names the hash function of every container explicitly (#899, #904, #905, #906). - LiquidHaskell, the refinement type checker for Haskell: 3 merged PRs fixing the autosize measure for recursive datatypes (#2738, #2742) and rejecting
pleannotations in modules that leave PLE off (#2739). - Apalache, the symbolic model checker for TLA+: 8 merged PRs across the type checker, expression simplifier, and module importer.
- Logic Evaluator: propositional logic parser and Boolean minimizer (Quine-McCluskey, Petrick's method, Karnaugh maps).
Python - ATL Model Checker: strategic verification of multi-agent systems with Alternating-time Temporal Logic.
Python - DietiEstates25: full-stack real estate platform with geospatial search.
Spring Boot · React · PostGIS - Labyrinth Game: multiplayer TCP client-server maze game.
C · UNIX sockets
More on my portfolio.
Reasoning
Engineering
