Legend
- Boxes (□)
- definitions
- Ellipses (○)
- theorems and lemmas
- Diamonds (◇)
- axioms — unformalized external results
- ■ Draft
- AI-generated, not yet reviewed
- ■ Reviewed
- human confirmed NL content
- ■ Bound
- has
\lean{{}}binding to Lean declaration - Aligned
- human confirmed NL↔Lean semantic match
- Proved
- Lean proof compiled (theorems only)