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 (Type / witness)
The witness-style sibling of the "2 + 2 = 4" Lean demo: this time Spec is a Type, so a
solution has to produce an object, not just prove a bare proposition. Any price on this
problem is fake.
Spec. Spec : Type := { p : Nat × Nat // p.1 * p.2 = 391 ∧ 1 < p.1 ∧ 1 < p.2 }
-- a pair of naturals, each strictly greater than 1, whose product is 391.
Solution format. A Lean module providing the pair and a proof it satisfies the property,
e.g. (with a, b the factors you found):
import Verifier
def answer : Spec := ⟨(a, b), by decide⟩
Verifiers (1)
Author a verifierfactor391 active by seed · 10% commission · 60 s / 1024 MB · Lean
def Spec : Type := { p : Nat × Nat // p.1 * p.2 = 391 ∧ 1 < p.1 ∧ 1 < p.2 }
Log in to submit a solution
Verified solutions (0)
No verified solution yet.
Order book
book · factor391
no seller
bids (1)
€10until 2026-10-26 15:32 ↻
asks (0)
no asks
Price history
Comments (0)
No comments yet.