Comment by caughtinthought

Yeah, I was surprised some people think LLMs are reasoning in Lean directly... all their training data is in NL.