Max Martínez
Computer Science student at UNAM focused on formal methods, theorem proving, and the construction of provably correct software.
IMO Grand Challenge: Problem Formalization
Formalized 3 International Math Olympiad problems using Lean 4’s proof assistant and created machine-readable problem statements to serve as competition benchmarks.