I am a computer scientist very interested in proof assistants and the Lean Proof Assistant in particular. I regularly contribute to Mathlib, the Lean mathematical library, currently having over 50 merged pull requests.
Industry
Since mid April 2026 I’m working for Marvell Technology, Inc..
From December 2025 to March 2026 I worked as freelancer for Cajal Technologies, Inc. using the Lean proof assistant.
Academy
- In 2025 I did a seven months internship at Max Planck Institute
for Security and Privacy with Gilles Barthe as my
supervisor.
- My second project was about verification of probabilistic cryptographic code in Jasmin and EasyCrypt.
- In my first project I worked on formalizing of the algebraic part of quantum computing in Lean.
Education
- Degree in Computer Science at the National University of Córdoba.
Competitive programming
- Participation in the ICPC South America South regional
programming contest:
- 2025: position 11 out of 201.
- 2024: position 16 out of 187.
- October 2023: position 26 out of 152.
- March 2023: position 49 out of 105.
- Participation in the ICPC Torneo Argentino de Programación (ICPC Argentine Programming Tournament):
- Participation in Training Camp Argentina in 2024.
- Teacher of competitive programming course at FAMAF in 2024.
- Participation in multiple competitive programming contests on Codeforces and AtCoder.
Courses and events
Assisted to Lean Together 2026.
Assisted to the 16th International Conference on Interactive Theorem Proving.
Formalizing Mathematics in Lean at Utrecht Summer School 2025.
RIO 2025 Summer School on Informatics:
- Program Verification with Isabelle/HOL.
- Introduction to Computability Theory.
- Programming Languages for Cybersecurity.
Participation in Cornell, Maryland, Max Planck Pre-doctoral Research School 2023.
Informatics Sciences School 2022 at University of Buenos Aires:
- Satellite imagery processing.
- Quantum natural computing: from simulation to algorithms.