Tag attribute marking a declaration as intentionally unproved.
Use this when the book does not provide a proof for a statement (e.g. "proof
omitted", references another source, or states without proof). The dependency
graph metaprogram detects this tag and surfaces it as is_unproved so that
evaluation judges can distinguish justified gaps from failures.
Convenience macro: unproved theorem foo : P expands to
@[unproved] axiom foo : P.