diff --git a/good_ideas.myco b/good_ideas.myco
index a67be1c..09ad133 100644
--- a/good_ideas.myco
+++ b/good_ideas.myco
@@ -6,6 +6,7 @@
 * {
 Similarly, contrastive RL for computer algebra (specifically, proving that expressions equal other expressions via making substitutions repeatedly). Try and contrastively learn a "how close is this expression to this other one" function (I think with an action input?). Bootstrap to progressively harder problems.
 * 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.
 }
 * {
 Startup ideas: