Function run_proof_sketch 

pub fn run_proof_sketch(
    premises: &[ProofExpr],
    premise_names: &[Option<String>],
    goal: &ProofExpr,
    script: &str,
    rule_name: Option<&str>,
) -> (VerifiedProof, usize)

The vernacular Proof: line is an English proof SKETCH, not a Lean tactic block.

It names the METHOD; the routine obligations the method leaves are discharged by the same certified automation Proof: Auto. uses, and the count comes back so the answer can SAY how much the author left to the machine (see discharged_note). Nothing about the trust door moves: every step, sketched or swept, is assembled into one derivation and certified through qed → check_derivation → the kernel. The engine-level script API (ProofState::run_script + qed) keeps Lean’s strict “close every goal” discipline untouched — the sketch reading belongs to the vernacular surface, not to the engine.

A step that ERRORS is never swept: the sweep runs only after the sketch itself ran clean, so a misspelt tactic, a missing hypothesis or an inapplicable rule still fails loudly instead of being proved around.

rule_name is Some for a ProofStrategy::ByRule line — a one-word proof. It changes only the DIAGNOSTIC: a word the tactic namespace does not carry is reported as what it is (a kernel inference-rule name) rather than leaving the author to read “unknown tactic” and guess.