emsenn

SKILL

3 min read

Write Formal Proof

Before writing any code

  1. Read the specification section that the proof corresponds to. Know what you are proving and why the spec claims it is true.

  2. Identify the proof strategy from the spec’s sketch or from mathematical reasoning. Do not start writing tactics until you know the argument.

  3. Check what already exists. Read the formalization directory’s existing files. Do not duplicate definitions. Import what you need.

Writing the proof

  1. State the theorem with a complete type signature. The type must precisely match the mathematical claim. If you cannot state the type without stubs or placeholders, you are missing prerequisites — write those first.

  2. Write the proof body. In Lean, prefer tactic mode for multi-step proofs, term mode for one-liners. In Agda, proofs are always terms — use equational reasoning chains for clarity.

  3. No placeholders. Every field of every record/class must have a real implementation, not True, trivial, or a type that does not match the mathematical content. If a condition cannot be stated yet, document WHY and mark it with sorry (Lean) or a postulate (Agda) with an explicit comment explaining the gap.

Anti-slop checklist

Before marking a proof as complete, verify ALL of the following:

  • No sorry in the proof (Lean) or unexplained postulate (Agda)
  • No True placeholders standing in for real conditions
  • No placeholder types (e.g., Nat standing in for DefOp)
  • Every axiom/field is mathematically meaningful — it states what the spec says, not a vacuous condition
  • Proof compiles. Run lake build (Lean) or agda --check (Agda). If you cannot compile, say so explicitly rather than claiming the proof is done.
  • At least one concrete test instance exercises the new definitions (in Test/Trivial.lean or a test module)
  • Worked examples demonstrate that the definitions match mathematical intuition
  • Doc comments connect each definition to its spec section

After writing

  1. Run the build. Do not commit unverified proofs. If the build environment is not available, state this explicitly and flag the proof as unverified.

  2. Add test instances. Every new typeclass/record needs at least one concrete instance in the test file, with examples exercising derived lemmas on that instance.

  3. Update the module root (SemioticUniverse.lean or Everything.agda) to import the new file.

Common failure modes

  • Writing type signatures that look right but contain stubs. Fix: Read the signature aloud as a mathematical statement. Does it say what the spec says?

  • Proving things about Prop (where everything is trivial) and assuming they generalize. Fix: Also test on a nontrivial instance (e.g., a 3-element Heyting algebra).

  • Writing comments that describe what the proof WILL do rather than what it DOES. Fix: Comments describe the current state. Future work goes in a roadmap, not in proof comments.

Graph View