Spaced proof review as a way to understand key insights in a proof
I think a key difficulty of mathematics is "combinatorial explosion" or the problem of alternatives. e.g. if a proof uses ≤ in one place instead of < or some other inequality (e.g. reversed direction) then you, as the reader of the proof, must be prepared to explain why. With each piece of the proof, you have to be able to say why the author did one thing instead of the other. The end result is that you're not just memorizing the short string representing the proof — rather, you're internalizing this much larger space of "why the author did this thing instead of this other thing which doesn't work", which can guide you when you write the proof yourself. Why is this relevant to Anki? Well, i feel like one really good way to actually experience all these alternatives in proof-writing is to attempt the proof yourself at spaced intervals. As you start to forget pieces of the proof, your mind goes like "wait, so here, should i do this or this other thing?" and so you check both, and then you get this feeling of like "oh! so that's why the book does it like that".
One time I completely forgot the trick for how to even get started proving Löb's theorem. (That's sort of a good thing because I wasn't just relying on a memorized trick!) Eventually I remembered that Löb's theorem had something to do with the Santa Claus sentence, which I wrote down as "If this sentence is true, then Santa Claus exists". So then I realized I wanted something like [math]T \vdash L \leftrightarrow (L \to \varphi)[/math]. But then I remembered that actually it's not just the bare sentence, but there was a provability predicate somewhere. And that's when I remembered that we are supposed to diagonalize [math]\mathrm{Bew}(x) \to \varphi[/math]. So, [math]T \vdash L \leftrightarrow (\Box L \to \varphi)[/math]. Previously, I think it was somewhat mysterious to me why I should diagonalize that particular formula (like, where that formula even comes from).
