Lean Online Judge

---

How to use it?

Some knowledge of Lean is necessary to solve problems on the platform. You can find installation instructions and resources to learn Lean on the official website. Going through the first few chapters of Mathematics in Lean should be enough to get started.

How to submit a solution to a problem?

If you played with Lean for a bit, this should be relatively straight-forward.

• Problems that ask for a proof.
  Replace sorry in the problem template with your proof and submit the resulting code.

• Problems that ask for an answer.
  Some problems ask to provide an answer and prove that it's correct. Formally defining what an acceptable answer should be is difficult. Instead, valid answers are predefined and added to the Answer Bank. Replace the answer declaration in the problem template with one from the Answer Bank, then prove its correctness as usual.

• xyzzy.
  This is a special problem that doesn't have a real template and can be used to submit a solution to any custom problem. It can also be used to test the checker against potential exploits (please, create an issue on GitHub if you find one). Submissions are not visible to other participants but still visible to the admin.

You can import Mathlib modules not present in the template but try to keep imports light to avoid timeout. The checker is using the latest stable version of Mathlib (currently, v4.28.0).

How to participate in a contest?

Simply go to an ongoing contest and start solving problems! Contest problems are still available for upsolving after contest is over.