The speaker says AI tools can translate book mathematics into Lean without considering whether the resulting formalization is easy to work with.

“And what seems to be happening now is you can have an AI tool which just sees something in a book, doesn't think about it at all, just blindly translates that human-written, uh, mathematics into, you know, into Lean, the language, you know, the, the language that the software uses, and, uh, doesn't really care about making things easy.”