Submission Status

Below is a brief explanation of possible submission statuses. For details, see the checker source code.

Pending

The submission has not been judged yet. You may need to refresh the page to see if the status has been updated.

System error

Something went wrong on the system side. Please, contact the admin via Discord.

Compilation Error

Submission compilation has failed. Make sure your Mathlib version matches the one used by the checker. It is normally the latest stable (currently, v4.28.0). You can check the version in your Lean editor with #eval Lean.versionString.

Time out

Submission compilation took more time than the predefined limit. This might be caused by heavy imports (e.g., whole Mathlib). The #min_imports macro can be helpful in this case.

Out of memory

Submission compilation took more memory than the predefined limit.

Bad answer

The provided answer does not match one set for this problem. Make sure you are using one from the Answer Bank.

Template mismatch

Some declarations in the template are missing or do not match those in the submission. Extra declarations are allowed.

Rejected

The submission has not passed extra verification. Make sure that propext, Classical.choice, and Quot.sound are the only axioms used. This can be checked with #print axioms solution. Note that some tactics, such as native_decide, may rely on extra axioms. The status can also be caused by attempts to trick the checker (e.g., by tampering the environment via metaprogramming). If that is your intention, there is a special problem for that.

Passed

The submission has passed. Hooray!