Demo problem. Any price shown here is fake — nothing is owed and nothing is paid. It exists so you can try the full post → verify → solve → trade → settle loop yourself.
Lean demo (Prop)
A minimal Lean verifier, posted to check the platform's Lean pipeline end-to-end for yourself. Any price on this problem is fake.
Verifier contract. Verifier.lean defines a root-level constant Spec : Prop. You submit
a Solution.lean module defining answer : Spec; the Lean kernel itself decides, not any
code the verifier author wrote.
Spec. Spec : Prop := 2 + 2 = 4
Solution format. A Lean module proving Spec, e.g.:
import Verifier
theorem answer : Spec := by decide
Verifiers (1)
Author a verifierprop_demo active by seed · 10% commission · 60 s / 1024 MB · Lean
abbrev Spec : Prop := 2 + 2 = 4Log in to submit a solution
Verified solutions (0)
No verified solution yet.
Order book
book · prop_demo
no seller
bids (1)
€10until 2026-10-26 15:33 ↻
asks (0)
no asks
Price history
Comments (0)
No comments yet.