Check the domain and edge cases
Write down what happens for empty structures, zero, negative values, duplicate elements, non-finite cases and degenerate parameters. If the informal theorem silently excludes a case, make that exclusion an explicit hypothesis.
Make every assumption explicit
- ✓Do not hide a mathematical assumption in a notation expansion.
- ✓Do not rely on a local instance unless it is listed in the review.
- ✓State decidability, finiteness and non-emptiness requirements.
- ✓Match the assumptions used in the source paper or specification.
Compare strength, not just syntax
A theorem can compile while proving a weaker claim. Check whether an equality should be an iff, whether an existence result should include uniqueness, and whether a bound is tight enough for the downstream argument.
-- Ask: is this the intended strength?
theorem exists_bound (f : Nat → Nat) :
∃ n, ∀ k, f k ≤ n := by
sorry
-- Stronger, but only if justified:
-- theorem exists_bound_unique ... : ∃! n, ...Freeze the statement before proof work
Once the statement is approved, record it and treat later changes as specification changes. This keeps proof effort auditable and prevents a difficult proof from silently becoming a different, easier theorem.
Frequently asked questions
Can I use `sorry` while drafting a statement?
Yes, for statement review. The handoff must clearly label placeholders so nobody mistakes a draft for a completed proof.
Who decides whether a statement matches the intended mathematics?
The author or domain reviewer owns that decision. A proof-engineering pass can surface ambiguities and verification gaps, but it should not silently redefine the claim.