Lean 4

Declaration uses 'sorry' (Lean 4)

Lean accepted the file, but this declaration still contains sorry — a placeholder that skips a step — so the theorem is not actually proved.

What it looks like

Main.lean:3:8: warning: declaration uses `sorry`

What does "Declaration uses 'sorry' (Lean 4)" mean?

Lean prints this warning (not an error) when it adds a theorem or definition whose proof still contains sorry. Behind the scenes sorry is the axiom sorryAx, which can produce a proof of any statement, so a theorem that relies on it proves nothing. Since Lean 4.28 the message reads declaration uses `sorry` with backticks; Lean 4.27 and earlier print declaration uses 'sorry'. It is only shown on the declaration that contains the sorry, and only when the file has no errors: when a step fails, Lean fills it with a sorry of its own and shows you the error instead.

What causes "Declaration uses 'sorry' (Lean 4)"?

You wrote sorry as a placeholder for a step or a whole proof and have not replaced it yet.
The admit tactic was used; it is the same as sorry.
A proof copied from a tutorial or produced by an AI tool left a step unfinished.

How do I confirm the cause?

Search the file for sorry and admit; the warning is reported on the declaration that contains one.
Add #print axioms yourTheorem after the theorem. A finished proof lists only propext, Classical.choice and Quot.sound, or says it does not depend on any axioms; sorryAx means a sorry is still in it or in a lemma it uses.
A theorem can show no warning yet still depend on sorry through a lemma it calls — #print axioms catches that, the warning does not.

How do I fix "Declaration uses 'sorry' (Lean 4)"?

Replace each sorry with a real proof term or tactic block.
Put exact? or apply? where the sorry was to search for a lemma that closes that goal.
Run #print axioms yourTheorem: if sorryAx is listed, this theorem or something it uses is still incomplete.
A finished proof lists only propext, Classical.choice and Quot.sound (or no axioms at all).

How do I stop it happening again?

Treat any warning as a failure in CI: a lake build that finishes with no errors and no warnings is the everyday standard for a complete proof.
For proofs you did not write, including AI-generated ones, check #print axioms and replay the build with lean4checker before trusting a "verified" claim.