Talia Ringer on Nostr: I've noticed newer proof engineers quickly get distracted by one of two things: 1. ...
I've noticed newer proof engineers quickly get distracted by one of two things:
1. trying to set up the perfect definitions, lemmas, and theorems from the start, or
2. trying to game the proof of the top-level theorem that's already there without thinking much about what is needed to get there.
It occurs to me that both of these are problems in the balance of bottom-up versus top-down proving. Experienced proof engineers are more likely to smoothly move between these when it will give them the most information to make progress.
1. trying to set up the perfect definitions, lemmas, and theorems from the start, or
2. trying to game the proof of the top-level theorem that's already there without thinking much about what is needed to get there.
It occurs to me that both of these are problems in the balance of bottom-up versus top-down proving. Experienced proof engineers are more likely to smoothly move between these when it will give them the most information to make progress.