I kind of agree, "math" can be a "language". Same as "images" can be a language. You can use anything as tokens.

In this context, we're not even talking about "math" (as a broad, abstract concept). We're strictly talking about converting English to Lean. Both are just languages. Lean isn't just something that can be a language. It's a language.

There is no reason or framing where you can say Aristotle isn't a language model.

That's true, and a good fundamental point. But here it's much simpler than that: math is a language the same way code is, and if there's one thing LLMs excel at, it's reading and writing code and translating back and forth between code and natural language.