Lean demo (Mathlib)

The Mathlib-using sibling of the other two Lean demos: this verifier's Spec is stated using a real Mathlib definition (Nat.Prime), not just core Lean. Any price on this problem is fake.

Spec. Spec : Prop := Nat.Prime 7

Why abbrev, not def. abbrev is reducible, so tactics like norm_num and decide can see straight through it to Nat.Prime 7; a plain def would leave the goal stated as the opaque Spec and most Mathlib tactics won't unfold it on their own. Same reason the other two demos use abbrev.

Solution format. A Lean module importing Verifier and proving Spec, e.g.:

import Verifier

theorem answer : Spec := by norm_num

Budget. Importing Mathlib's norm_num extension costs real time and memory on its own -- this verifier is published with a larger budget (120 s / 6144 MB) than the other two demos for exactly that reason.