Comment by chrisjj

> Autoformalization is the formalization of mathematics by AI.

I guess that came from a chatbot?

"There’s no such thing as auto-formalization" https://cutfree.net/notes/autoformalization.html