> I guess [the term “autoformalization”] came from a chatbot?

The term dates back at least to 2020, years before the release of ChatGPT.

https://research.google/pubs/a-promising-path-towards-autofo...