A Lean challenge by @harfe: Lean files with missing proofs. Will someone fill them in? A bot checks solutions with an external verifier (lake comparator) and resolves this market.

Deadline and close: 2026-10-31 23:59:59 UTC

Resolution

• YES as soon as a solution posted before the deadline passes verification. Verification may finish after the deadline.

• NO if none does, even if the challenge turns out to be broken.

Challenge

File list

• Challenge.lean

• config.json

Challenge info

version: v4.36.0-rc1
file: Challenge.lean cdac9e11f2eb7a845ff24dbda55c4e640286d9e55e77ccb37e0d939b19d5e0c5 4 lines 91 bytes
file: config.json 9fe7f8dee1890cf7129cd657a3566fb0ad496511d598eb681f014890092c1504 6 lines 188 bytes

Original submission

name: square_even_of_even
by: 2026-10-31
file: Challenge.lean https://pastebin.com/raw/QWA0RNZ6
file: config.json https://pastebin.com/raw/GYxVV1DX

Comparator config

{
  "challenge_module": "Challenge",
  "solution_module": "Solution",
  "theorem_names": ["square_even_of_even"],
  "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]
}

Submitting a solution

Post a top-level comment that starts with Solution and has one file: <path> <url> [sha256] line per file:

Solution
file: Solution.lean https://example.org/Solution.lean

• Include the config's solution_module (module A.B is the file A/B.lean). Only .lean files.

• URLs start with https:// and serve the raw file. The sha256 is optional and may be shortened. The files are downloaded when the bot sees the comment.

• The bot checks the comment as it first sees it, later edits are ignored.

• The bot replies to the comment when the check is done. In some cases it can take hours.

• The comparator run is subject to a memory limit of 10 GiB and a time limit of at least 1 hour.

Note: this bot is in beta and details may change.