Where we can sort proofs into categories based on the proof techniques we think are well-equipped to solve them.
As we develop our algorithm, we can test it out on these proofs.
Some proof techniques include:
- Conflict-driven: Proofs where oscillating between counterexamples, lemmas-learnt-from-failure, and the proof helps proof discovery.
- Backward-Reasoning from Hypothesis: Proofs where backward-reasoning from the hypothesis (finding conditions that imply the hypothesis) helps proof discovery.
- Forward-Reasoning from Target: Proofs where forward-reasoning from the target (finding necessary conditions) helps proof discovery.
- Generalization - Specialization: Proofs where applying generalization & specialization helps proof discovery.
- Induction: Proofs where applying mathematical induction (or, thought of slightly differently, an algorithm) genuinely helps progress the proof.
- Library Search: Proofs where a sophisticated library search has to be used.
Of course some proofs may fall in multiple categories, at which point it might make sense for the full proof to be stored in a folder belonging to a particular category, and for the high-level summary of why it is relevant to each category to still be written down in every relevant category.