Greg Burnham on Lemmata

I broadly agree, though I will say that evaluating "is this an interesting intermediate result" is related to what the so-called prover model + MCTS is supposed to provide. I think it's analogous to judging whether a move in a game will take you in a winning direction, even if you can't see all the way to the end of the game. LLMs' generative abilities make them seem like better brainstorming partners, but I'm not sure less-linguistic systems like AlphaProof can't also get good statistical intuitions for which direction to take a proof. The space of possibly-good technical directions seems wide open to me!