> ./whoami

Mathematician | AI & Formal Methods Student

I am a Mathematician (B.S. from UNICEN, Argentina) currently learning and experimenting in the intersection of Large Language Models (LLMs) and Automated Theorem Proving (ATP). My focus is on understanding how to bridge the gap between natural language mathematics and formal verification systems like Lean 4 and Coq.

Ayrton at Congress

> ./cv --display

Unable to display PDF file.

[DOWNLOAD CV_AYRTON_PORTO.PDF]

>> ./stack --list

Python Lean 4 Coq PyTorch TensorFlow Pandas Scikit-learn C++ MATLAB LaTeX Git

>> ./experiments --current

Currently exploring the 'reverse translation' problem: instead of formalizing math, I am experimenting with methods to translate formal theorems (Lean 4) back into natural language. The goal is to understand how explicit logical structures can be decoded into human-readable explanations.

>> ./mission --target

My long-term goal is to contribute to the development of an AI capable of formally proving almost any mathematical theorem.

[RETURN TO ROOT]