Diff of Good Ideas at ebf4887

@@ -8,2 +8,3 @@ Similarly, contrastive RL for computer algebra (specifically, proving that expre
 * What does Gyges mean by "anyone who wants it: you should be able to train contrastive models way faster if you use lsh to determine pairs to contrast"? This might contain alpha.
+* Maybe this should be a "theorem prover" and not an "expression rewriter". I think they're fairly similar anyway.
 }