Definition
Plain language
A keyword in proof languages that lets you mark a step as 'I'll prove this later' and keep going.
As stated in the literature
A Rocq keyword that introduces an unproven axiomatic placeholder for a proof obligation, allowing the rest of the development to type-check while tracking outstanding goals.
Why it matters: It lets large formal developments make progress without getting blocked by a single hard step, as long as the unfinished obligations are tracked.
For example, you might write 'Admitted' under a difficult lemma so the rest of your proof script still compiles while you focus on other parts.
Heard on the show
“The feature is a keyword called "Admitted.”Episode 075 — Growing Code and Proof Together: Verified Systems in Ten Hours Instead of a Year