Nat add zero
ShareProve that for every .
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
after your body — the file won't compile unless your answer matches.
Forbidden tokens (the static filter rejects 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, …).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