Link to current text
MATH.19:3 - Forces
| Force | Tension |
|---|
| A conclusion guides search | A sufficient intermediate claim can itself be harder than the original target. |
| Available constructions guide inference | Many consequences of the premises do no work in the desired argument. |
| Stronger lemmas support more uses | Extra hypotheses or conclusions can make the lemma unavailable or unnecessarily difficult. |
| Local reasoning supports collaboration | A lemma can be assigned separately only when its inputs, premises and required consequence are clear. |
| Automation can complete steps | The obtained proof still has to establish the mathematical statement the work requires. |