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.
Talia Ringer /
npub1vk…vace4
2024-02-07 18:54:05
in reply to nevent1q…3mlt
Author Public Key
npub1vku3fe6ehffwyphmz04977g4h9v73ppgkzem3tnanp6pp4fkennqyvace4Seen on
wss://relay.noswhere.comPublished at
2024-02-07 18:54:05Event JSON
{
"id": "5a4700944511e9e0aa1c86ea5058cad6c83ef5c9b1a88de0509207b19c972135",
"pubkey": "65b914e759ba52e206fb13ea5f7915b959e88428b0b3b8ae7d987410d536cce6",
"created_at": 1707328445,
"kind": 1,
"tags": [
[
"e",
"0f36bf70c002bd33b59061e2eb7524e436a8591a5b959a4832c99a650cc166fd",
"wss://relay.mostr.pub",
"reply"
],
[
"proxy",
"https://mathstodon.xyz/users/TaliaRinger/statuses/111891477006601057",
"activitypub"
]
],
"content": "I've noticed newer proof engineers quickly get distracted by one of two things:\n\n1. trying to set up the perfect definitions, lemmas, and theorems from the start, or\n2. trying to game the proof of the top-level theorem that's already there without thinking much about what is needed to get there.\n\nIt 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.",
"sig": "01a4e9e91669c2cf576bb0c9acebd2179e7caa9b065bd47452bd8b1bfd1c98c341cd4040da97706bdb307d7807cf9e25a03b3789c6ec6b9cd0c3c9cc986583d1"
}