Nat add zero
Prove that adding zero on the right is the identity on `Nat`. Define `answer : ∀ (n : Nat), n + 0 = n` somewhere in your submission body. You may write any helper `def`/`lemma`/`theorem`/`instance` you like, but the file must contain a top-level `answer` of the required type. The app automatically appends `def solution_target : ∀ (n : Nat), n + 0 = n := answer` after your body — the file won't compile unless your `answer` matches. Forbidden tokens (the static filter will reject your submission instantly): `sorry`, `admit`, `axiom`, `unsafe`, `opaque`, `constant`, `native_decide`, `implemented_by`, `extern`, `macro`, `syntax`, `elab`, `run_cmd`, `initialize`, `set_option`, `attribute`, `import`, `namespace`, `section`, `end`, `universe`, `#eval`, `#check`, `#print`, `#reduce`, `#guard`. One-liner solution: `theorem answer (n : Nat) : n + 0 = n := Nat.add_zero n`.
theorem answer (n : Nat) : n + 0 = n := by ?
answer with type ∀ (n : Nat), n + 0 = n. You can declare any def, theorem, lemma, instance, open, variable etc. — the static filter only blocks soundness-bypass tokens (sorry, axiom, native_decide, …) and wrapper-escape tokens (namespace, end, import, …).import ProofGarden.Challenges.C0001.Statement import Mathlib namespace ProofGarden.Challenges.C0001.Submissions.<submission-id> -- ┌── USER BODY START -- │ (your submission) e.g.: -- │ theorem answer (n : Nat) : n + 0 = n := by -- │ sorry -- ← FORBIDDEN; use real tactics -- └── USER BODY END def solution_target : ∀ (n : Nat), n + 0 = n := answer #print axioms solution_target end ProofGarden.Challenges.C0001.Submissions.<submission-id>
Sign in to submit a proof body.
Any sequence of Lean tactics is fine. The static filter rejects tokens that don't belong inside a tactic block — the full list:
importnamespacesectionenduniverseaxiomsorryadmitnative_decideopaqueconstantimplemented_byexternunsafemacrosyntaxelabrun_cmdinitializeset_optionattribute#eval#check#print#reduce#guardlocal attributesolution_target