[Lean] Will someone solve square_even_of_even by 2026-10-31?
Source: Manifold price history
This market has resolved. The final Manifold price was 59.0%.
- Final market price
- 59.0%
- Event deadline
- October 31, 2026 at 7:59 PM ET
- Venue status
- resolved
ProbCast Reliability Summary
[Lean] Will someone solve square_even_of_even by 2026-10-31? The final Manifold price was 59.0%. This market has resolved. The final Manifold price was 59.0%.
- Market data as of
- October 31, 2026 at 5:35 AM ET
- ProbCast assessment generated
- October 31, 2026 at 5:37 AM ET
- Source
- Manifold
- Event deadline
- October 31, 2026 at 7:59 PM ET
- Market status
- Resolved
- Data updated
- 2m ago
What this market actually measures
A Lean challenge by @harfe: Lean files with missing proofs. Will someone fill them in?
This summary shows the opening of the venue's official rules. ProbCast has not yet generated an independent plain-English interpretation for this contract — review the full rules before relying on it.
View full official resolution rules
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.