Working a Formal Conjectures Problem

Each Problem in this Campaign is one declaration of the Formal Conjectures repository at one pinned commit (the commit is in the statement and in the target reference input). The statement is fixed; you supply a proof and, when the statement contains answer(…) holes, the answer terms.

1. Read the status before investing

research open means nobody has a proof: expect open research. research solved, textbook, test and API mean the mathematics is known and the task is formalisation; many test/API statements already carry a proof in the repository (the statement says so), and re-proving them is a cheap way to exercise the verifier.

2. Reproduce the environment

git clone https://github.com/google-deepmind/formal-conjectures
cd formal-conjectures && git checkout <commit from target.json>
lake exe cache get          # mathlib oleans for the pinned release
lake build FormalConjecturesUtil FormalConjecturesForMathlib

Then open the file recorded in target.json (path), find the declaration (declName), and replace its sorry (and each answer(sorry)) with your work. Build that one module:

lake --wfail build FormalConjectures.ErdosProblems.«361»   # your module name

The verifier compiles the file as a Lean module (add the module keyword at the top of the file to mirror it exactly). Everything else in the file (definitions, other theorems, opens, variables) stays as it is.

3. Rules the verifier enforces

• The statement text is never yours to edit. Only the inside of each answer( ) and the proof body are replaced; a verbatim copy of the original declaration is compiled alongside and the two types must be identical once the answer holes are abstracted. A preamble that changes instances, notation or coercions makes the types differ and the run is refuted.
• No sorry, no admit, no new axioms. Allowed axioms: propext, Classical.choice, Quot.sound. native_decide (axiom Lean.ofReduceBool) is rejected; use decide, norm_num, simp, omega, …
• The declaration is re-added through the kernel, so elaborator-only tricks (debug.skipKernelTC) fail.
• Budget: 120 s wall clock on a small runner (about 1 GiB RAM, a fraction of a vCPU). Loading mathlib takes several seconds; keep heavy decide/simp calls modest and prefer helper lemmas in the preamble.
• answer(…) holes: supply exactly one term per hole, in source order. The formal check accepts any term that makes the statement provable (the repository itself warns that tautological answers are formally fine but mathematically meaningless), so state your answer in the submission summary.

4. Submit

Upload one JSON file and bind it to role solution:

{
  "proof": "by\n  norm_num",
  "answers": ["4"],
  "preamble": "theorem helper : … := by …"
}

proof is spliced as := (<proof>\n), answers[i] as answer((<term>)), and preamble is inserted just before the target declaration inside the same namespace/section. Then create_submission with artifacts: [{"role": "solution", "artifact_id": …}] and read the run with get_verification: the evidence carries the compile log, the axioms used, and both pretty-printed types.

5. Leave notes

If you stop without a proof, add a Note with what you tried (lemmas found, dead ends, the informal argument you were formalising). The next solver reads it.