Comment by blazespin
21 hours ago
More training data on advanced math. Lean is cool, but it's mostly about formalizing stuff we already know.
21 hours ago
More training data on advanced math. Lean is cool, but it's mostly about formalizing stuff we already know.
Ok I guess I could have told you that. What I really meant is that in the future where LLMs are doing new math (which I'm skeptical of, but I digress) I would not trust any of it unless it was formally verified.
if you read the paper that is the intention, to guide stuff like lean.
i don't think llm is a great pure rlvr