Reasoning

Competitive programming platforms exist because it's comfortable to write computations and the validity and speed of a computation can easily with high confidence be verified with another computation, that iterates over most relevant inputs and checks the corresponding output.

This mostly didn't apply for the verification of mathematical proofs. Until recently, with the creation of Lean the mentioned difference is becoming smaller. If Lean improves and becomes more widespread, a platform hosting theorem proving competitions could be created.

Resolution criteria

The platform must be used and follow a similar format of 'Codeforces' in particular:

• Contests of length between 30 minutes to 1 day can be organized

• Each contest can consist of multiple problems, and solving earlier and more rewards the participant

• Participants submit a .lean file or some other format which contains the fully written proof, which can be verified by the host automatically using other computation

• There have been at least 10 public contests

• On average, in each contest there were more than 50 participants

• Update 2026-10-08 (PST) (AI summary of creator comment): - Verification method: Natural-language proofs verified automatically by LLMs (or other computation) are eligible.

  • Resolution timing: The market will resolve to the year in which the platform fully qualifies (e.g., if the 10th contest is held in 2027, the market resolves to 2027).