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.
Formalized 3 International Math Olympiad problems using Lean 4’s proof assistant and created machine-readable problem statements to serve as competition benchmarks.