FormalMarket

Writing verifiers and solutions

A verifier decides, by machine, whether a solution is correct. Pick the language you want to work in.

The verifier

A verifier is one Python module that defines

def verify(solution: str, rng: numpy.random.Generator) -> bool:

It gets the candidate solution as a string and must return the literal True if and only if it is correct. Anything else -- False, an exception, a timeout, 1, printing "ACCEPTED" -- is a rejection. Put the solution format you expect in the module docstring so solvers know what to submit.

  • Parse defensively: strip whitespace, reject wrong arity, empty or malformed input, trivial answers. Never let bad input raise -- return False.
  • Check the whole claim, not a heuristic. No prints, no side effects, no global state.
  • Need randomness (random test cases)? Draw from rng only, so every verdict is reproducible from its seed.

What a verifier can use

Python 3.12, the standard library, and numpy, scipy, sympy, mpmath -- nothing else can be imported. It runs in a sandbox with no network, a read-only filesystem and no writable directory: do not read or write files or spawn processes. It must finish, imports included, within the time and memory budget the author declares when publishing; design for a small one (10 s / 256 MB is typical).

The solution

Plain text, in whatever format the verifier's docstring asks for (at most 64 KB). Paste it or upload a file on the problem page, pick the verifier, and the verdict arrives within that verifier's time budget. Only an ACCEPTED solution can be listed for sale.

Try it: the Python demo problems

Nothing on a demo problem involves money: every bid, ask and trade on it is fake, and a practice bot already holds a standing bid on each one. Post a solution, get your verdict, list an ask and watch it trade -- the whole loop, with no stakes.

The verifier

In Lean the verifier is a type, and the checker is the Lean kernel -- there is no function to write. A verifier is a module named Verifier defining one root-level constant:

abbrev Spec : Prop := 2 + 2 = 4          -- a statement to prove, or
def Spec : Type := { p : Nat × Nat // p.1 * p.2 = 391 ∧ 1 < p.1 ∧ 1 < p.2 }   -- an object to produce
  • Spec : Prop asks for a proof; Spec : Type (typically a subtype) asks for a witness together with the proof it qualifies.
  • Write Spec with abbrev when tactics such as decide or norm_num must see through it; a plain def leaves the goal opaque to them.
  • Helper definitions and lemmas can live in the same file, above Spec. The verifier is held to the same axiom rules as solutions: a sorry in a helper lemma fails the build.

The solution

A module named Solution defining a root-level constant answer : Spec:

import Verifier

theorem answer : Spec := by decide        -- Prop
def answer : Spec := ⟨(17, 23), by decide⟩  -- Type

import Verifier brings Spec into scope (you may also restate the type verbatim; the kernel compares types, not text). Accepted iff the module elaborates, the kernel accepts answer : Spec, and the proof's axioms are within the allowlist -- propext, Classical.choice, Quot.sound. So sorry, your own axioms and native_decide are all rejected (a verifier may widen the list with a first-line comment such as -- judge: allow Lean.ofReduceBool). Every elaboration-time trick -- run_cmd, debug.skipKernelTC, redefining Spec -- is caught by an independent kernel replay.

What is available

Core Lean, and Mathlib: import Mathlib.Tactic.NormNum.Prime (or any other Mathlib module) works in both the verifier and the solution, from a pinned Mathlib build inside the sandbox. Importing Mathlib costs real time and memory, so a verifier that needs it should be published with a larger budget (a few minutes, a few GB) than a core-only one. No network, no files, no randomness: a verdict depends only on the two modules and the pinned image. Solutions are at most 64 KB.

Try it: the Lean demo problems

Nothing on a demo problem involves money: every bid, ask and trade on it is fake, and a practice bot already holds a standing bid on each one. Post a solution, get your verdict, list an ask and watch it trade -- the whole loop, with no stakes.