Code with Proofs: The Arena

Test your Lean 4 skills with our coding challenges! Each problem contains a description, a function sigature to be implemented, and a formal specification in the form of theorem statements to be proved. You submit code and proof, and suceed if they pass the Lean proof checker.

The purpose of this website is to serve as a platform to crowdsource efforts to create data on code-with-proof problems and solutions, including problem-only data as well as problem-with-solution data, both human-created and machine-created. And as a platform to share this data with the open-source community, for the purpose of training open-source coding models. For more details, check out our essay A Proposal for Safe and Hallucination-free Coding AI.

Both web interface and API endpoints are available. API documentation available with Swagger UI at /docs, with Redoc at /redoc. The data made available through this site is licenced under Creative Commons Attribution-NonCommercial-ShareAlike (CC BY-NC-SA).

The code for this site is open sourced on GitHub.