Difference between revisions of "Spaced proof review"

Latest revision as of 00:01, 2 August 2021

Spaced proof review is the general idea of trying to memorize/deeply understand a theorem using spaced repetition. This is currently one of my main interests with spaced repetition and with learning in general.

I also want to use this term to mean that particular method of proof review I've settled on? which involves adding the theorem statement on front, then proof solution on back (plus a whole bunch of subtleties about deck options, how to grade yourself, how to split things by deck, etc).

Rationale

Four steps of insights leading to my current workflow of proof cards:

It's a good idea to store big cards in the first place, rather than just smaller cards -- this lets you actually test your knowledge. I have found that if I have only small cards, I will know some of the pieces of knowledge that I intend to know, but there might be "gaps", and when I actually sit down to write a proof, I may be unable to do so. That's a problem.
Separating big cards into their own deck is a good idea, because it prevents breaking your workflow/rhythm while reviewing small cards (see also this tweet). I found that if I have to sit down and do a proof in the middle of my "normal cards" review session, it makes me more scared to do the normal reviews. I need some extra energy or be in a special mood to want to review proofs, so maintaining a strict separation is good.
But Anki doesn't "know about" proof cards, so its default deck options are optimized for small cards. Thus, changing the deck settings to make review of big cards not as onerous is important for keeping the habit. Otherwise you will be asked to do the same problem (that you just got done solving correctly) in 1 day, then in 4 days, then in 7 days -- that's way too frequent!
When you get stuck on big cards, make life easy on yourself by isolating the difficulty and making smaller cards that help you navigate those difficult points (e.g. difficult steps/insights in proofs). Make new cards when you get stuck. So there is some connection between proof cards and normal cards after all: the proof cards are the "real test", and the normal cards are there to help you for this test. And conversely, the proof cards are a check on your normal cards: they are testing if your normal cards are good enough and plenty enough to help you tackle the proof cards.

Analysis

The main problem with "state this theorem" and "prove this theorem" cards is that if your theorems are actually non-trivial, then it will take some time to write them down and so forth — so if you mix them in with your typical anki cards, then it will break the flow of review. So my current idea is to have a separate deck that's really slowly moving (only 1 card per day (edit: a better idea is to do a fake "review" as soon as you add a card, and to add cards on the day you first do an exercise)) and with a long time interval (i'm thinking something like 1 month, 1.5 months, 2.5 months, etc. (edit: this turned out to be horrible)) that just contains some important theorems and their statements. Previously my idea was to do this separately from anki — maybe in an orgmode file or setting up an email reminder — because i had made this theorems deck in anki many months ago but felt ugh-y about actually using it. Then i realized that the reason i felt this way was that the 5 cards per day or whatever, plus the shorter intervals meant i would be proving many things many times, which i didn't want. The idea is to make things fun! and one way to make them fun is to make the intervals longer, reduce your work load, and add only fun theorems.

These days i'm thinking more of my proofs/problems deck as the "main deal" and the smaller cards as things i should make to help me with the main deal. This is possible with math, but i'm not sure how to do this with AI safety (it's not like there's problems i can solve).

i start to notice a bunch of subtleties about a proof once i put it in the deck. There are a couple of reasons for this: (1) i'm forced to actually do the proof now, instead of just reading, so by doing the proof and comparing with the one in the book, i notice the differences, in particular the places where my proof is lacking. (2) because i forget some of the details of the proof, i start coming up with some alternative ways to do some things. This is like how andrew wiles says that having a bad memory is important for doing math, so that you forget how you got stuck so that you can do things a little differently next time. To give an example of this that i just experienced: i was proving the "length of linearly independent list <= length of spanning list" in axler. i didn't notice until now how subtle the use of the linear dependence lemma was. in particular, you need both parts (a) and (b) of the lemma, and it totally matters that the j is the same in both (a) and (b). until now, it wasn't clear to me why the j had to be the same, and also (b) seemed like an immediate corollary of (a) so i didn't see why it mattered that axler stated both. But now i see how all the parts of that lemma are used in this proof, which motivates things.

the spacing part matters for two reasons. first, you want to be able to prove these things at any point in the future, so the only solution to that is to just keep reviewing it over the course of your life. second, it's important that you forget some things in the proof. you might never forget the main idea, but there might be a small trick somewhere, and you can appreciate it way more if you forget it once and then reinvent it yourself later.

when does a problem deck not work? e.g. i'm worried that this style only works for things like real analysis where there are relatively simple theorems you can prove. what about something like belief propagation, where the "meat" of the content is in a long derivation of the algorithm/formula? and also i'm still not sure about things like godel's first incompleteness theorem: you can put in the diagonalization lemma, but what about all the tedious arithmetization work, which is different in every single textbook? do i just pick one and really internalize it? or should i just forget about internalizing it? Related: The mathematics community has no clear standards for what a mathematician should know.

one of the mistakes i made earlier is to add theorems from books that i hadn't fully processed. this meant that when it came up in the deck, i had more work to do then. but now i think it's better to do all the work when first making the card. then you know that everything in the deck is something you've deeply processed. there is a kind of relief, rather than a slight panic/dread of "oh boy, is this the day when i'll get that horrible card?"

thought about henkin proof: i entered in some cards related to it a long time ago, but after i did that i lost interest in the proof, and i've never returned to it. as a result, the cards are kind of in a dangling state now. if i were doing this again, i would put the sections of the proof as exercises in the problems deck, and only make the smaller cards if i need them.

What links here

@@ Line 2: / Line 2: @@
 I also want to use this term to mean that particular method of proof review I've settled on? which involves adding the theorem statement on front, then proof solution on back (plus a whole bunch of subtleties about deck options, how to grade yourself, [[Anki deck philosophy|how to split things by deck]], etc).
+==Rationale==
+Four steps of insights leading to my current workflow of proof cards:
+# It's a good idea to store [[big card]]s in the first place, rather than just smaller cards -- this lets you actually test your knowledge. I have found that if I have only [[small card]]s, I will know some of the pieces of knowledge that I intend to know, but there might be "gaps", and when I actually sit down to write a proof, I may be unable to do so. That's a problem.
+# Separating big cards into their own deck is a good idea, because it prevents breaking your workflow/rhythm while reviewing small cards (see also [https://twitter.com/michael_nielsen/status/1204079374888128513 this tweet]). I found that if I have to sit down and do a proof in the middle of my "normal cards" review session, it makes me more scared to do the normal reviews. I need some extra energy or be in a special mood to want to review proofs, so maintaining a strict separation is good.
+# But Anki doesn't "know about" proof cards, so its default deck options are optimized for [[small card]]s. Thus, changing the deck settings to make review of [[big card]]s not as onerous is important for keeping the habit. Otherwise you will be asked to do the same problem (that you just got done solving correctly) in 1 day, then in 4 days, then in 7 days -- that's way too frequent!
+# When you get stuck on big cards, make life easy on yourself by isolating the difficulty and making smaller cards that help you navigate those difficult points (e.g. difficult steps/insights in proofs). [[Make new cards when you get stuck]]. So there is some connection between proof cards and normal cards after all: the proof cards are the "real test", and the normal cards are there to help you for this test. And conversely, the proof cards are a check on your normal cards: they are testing if your normal cards are good enough and plenty enough to help you tackle the proof cards.
 ==Analysis==
-i start to notice a bunch of subtleties about a proof once i put it in the deck. There are a couple of reasons for this: (1) i'm forced to actually do the proof now, instead of just reading, so by doing the proof and comparing with the one in the book, i notice the differences, in particular the places where my proof is lacking. (2) because i forget some of the details of the proof, i start coming up with some alternative ways to do some things. This is like how andrew wiles says that having a bad memory is important for doing math, so that you forget how you got stuck so that you can do things a little differently next time. To give an example of this that i just experienced: i was proving the "length of linearly independent list <= length of spanning list" in axler. i didn't notice until now how subtle to use of the linear dependence lemma was. in particular, you need ''both'' parts (a) and (b) of the lemma, and it totally matters that the j is the same in both (a) and (b). until now, it wasn't clear to me why the j had to be the same, and also (b) seemed like an immediate corollary of (a) so i didn't see why it mattered that axler stated both. But now i see how all the parts of that lemma are used in this proof, which motivates things.
+The main problem with "state this theorem" and "prove this theorem" cards is that if your theorems are actually non-trivial, then it will take some time to write them down and so forth — so if you mix them in with your typical anki cards, then it will break the flow of review. So my current idea is to have a separate deck that's really slowly moving (only 1 card per day (edit: a better idea is to do a [[Do an empty review of proof cards immediately after adding to prevent backlog|fake "review" as soon as you add a card]], and to add cards on the day you first do an exercise)) and with a long time interval (i'm thinking something like 1 month, 1.5 months, 2.5 months, etc. (edit: this turned out to be [https://gist.github.com/riceissa/9616621772754a94e4254e1590a44afd horrible])) that just contains some important theorems and their statements. Previously my idea was to do this separately from anki — maybe in an orgmode file or setting up an email reminder — because i had made this theorems deck in anki many months ago but felt ugh-y about actually using it. Then i realized that the reason i felt this way was that the 5 cards per day or whatever, plus the shorter intervals meant i would be proving many things many times, which i didn't want. The idea is to make things fun! and one way to make them fun is to make the intervals longer, reduce your work load, and add only fun theorems.
-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".
+These days i'm thinking more of my proofs/problems deck as the "main deal" and the smaller cards as things i should make to help me with the main deal. This is possible with math, but i'm not sure how to do this with [[AI safety]] (it's not like there's problems i can solve).
+i start to notice a bunch of subtleties about a proof once i put it in the deck. There are a couple of reasons for this: (1) i'm forced to actually do the proof now, instead of just reading, so by doing the proof and comparing with the one in the book, i notice the differences, in particular the places where my proof is lacking. (2) because i forget some of the details of the proof, i start coming up with some alternative ways to do some things. This is like how andrew wiles says that having a bad memory is important for doing math, so that you forget how you got stuck so that you can do things a little differently next time. To give an example of this that i just experienced: i was proving the "length of linearly independent list <= length of spanning list" in axler. i didn't notice until now how subtle the use of the linear dependence lemma was. in particular, you need ''both'' parts (a) and (b) of the lemma, and it totally matters that the j is the same in both (a) and (b). until now, it wasn't clear to me why the j had to be the same, and also (b) seemed like an immediate corollary of (a) so i didn't see why it mattered that axler stated both. But now i see how all the parts of that lemma are used in this proof, which motivates things.
 the spacing part matters for two reasons. first, you want to be able to prove these things at any point in the future, so the only solution to that is to just keep reviewing it over the course of your life. second, it's important that you forget some things in the proof. you might never forget the main idea, but there might be a small trick somewhere, and you can appreciate it way more if you forget it once and then reinvent it yourself later.
-when does a problem deck not work? e.g. i'm worried that this style only works for things like real analysis where there are relatively simple theorems you can prove. what about something like belief propagation, where the "meat" of the content is in a long derivation of the algorithm/formula? and also i'm still not sure about things like godel's first incompleteness theorem: you can put in the diagonalization lemma, but what about all the tedious arithmetization work, which is different in every single textbook? do i just pick one and really internalize it? or should i just forget about internalizing it?
+when does a problem deck not work? e.g. i'm worried that this style only works for things like real analysis where there are relatively simple theorems you can prove. what about something like belief propagation, where the "meat" of the content is in a long derivation of the algorithm/formula? and also i'm still not sure about things like godel's first incompleteness theorem: you can put in the diagonalization lemma, but what about all the tedious arithmetization work, which is different in every single textbook? do i just pick one and really internalize it? or should i just forget about internalizing it? Related: [[The mathematics community has no clear standards for what a mathematician should know]].
-one of the mistakes i made earlier is to add theorems from books that i hadn't fully processed. this meant that when it came up in the deck, i had more work to do then. but now i think it's better to do all the work when first making the card. then you know that everything in the deck is something you've deeply processed. there is a kind of relief, rather than a slight panic/dread of "oh boy, is this the day when i'll get that horrible card?" i also now think that putting the full solution on the card, rather than just a reference to a textbook or web page, is better. it keeps everything self-contained, so when you're reviewing there is less work to do. in general, the idea to make reviewing fun.
+one of the mistakes i made earlier is to add theorems from books that i hadn't fully processed. this meant that when it came up in the deck, i had more work to do then. but now i think it's better to do all the work when first making the card. then you know that everything in the deck is something you've deeply processed. there is a kind of relief, rather than a slight panic/dread of "oh boy, is this the day when i'll get that horrible card?"
+thought about henkin proof: i entered in some cards related to it a long time ago, but after i did that i lost interest in the proof, and i've never returned to it. as a result, the cards are kind of in a dangling state now. if i were doing this again, i would put the sections of the proof as exercises in the problems deck, and only make the smaller cards if i need them.
 ==See also==
+* [[Deck options for proof cards]]
+* [[Do an empty review of proof cards immediately after adding to prevent backlog]]
+* [[Spaced proof review routine]]
+* [[Spaced proof review is not about memorizing proofs]]
+* [[Choosing problems for spaced proof review]]
+* [[Dealing with bad problems in spaced proof review]]
 * [[Spaced proof review as a way to invent novel proofs]]
 * [[Spaced proof review as a way to understand key insights in a proof]]
-* [[Linked list proof card]] -- this is sort of the opposite of the "spaced proof review" method
+* For my spaced proof review, I make sure to [[Use paper during spaced repetition reviews|use paper]]
+* Alternatives to spaced proof review:
+** [[Linked list proof card]] -- this is sort of the opposite of the "spaced proof review" method
+** Cloze deletion for proofs
+** Adding lots of simple front-back cards, as described by [[Michael Nielsen]] http://cognitivemedium.com/srs-mathematics
+==What links here==
+{{Special:WhatLinksHere/{{FULLPAGENAME}} | hideredirs=1}}
 [[Category:Spaced repetition]]

Difference between revisions of "Spaced proof review"

Latest revision as of 00:01, 2 August 2021

Contents

Rationale

Analysis

See also

What links here

Navigation menu

Personal tools

Namespaces

Variants

Views

More

Search

Navigation

Tools