This repository contains a comprehensive set of guidelines to follow while formalizing problem statements and solutions for Project Numina on our internal platform https://app.projectnumina.ai/.
The guideline document can be found in the file Guidelines.md. Additionaly, for extra clarity, we provide a set of examples following the guidelines under the folder /AnnotationExamples
To learn new tricks or read about common pitfalls about formalizing Olympiad problems in Lean, checkout the /FormalizationResources folder. Contributions very much encouraged!