A fork of openai/miniF2F adapted to Lean 4, with corrections to formalizations and informal descriptions. for human readers. - View it on GitHub