The speaker says that autoformalization is occurring and that an LLM can convert a mathematics paper into Lean code in a fraction of the time required by a human team.

“What's been interesting since the book came out, it came out in the States in June of this year. It's gonna come out in Europe later this month. What's been interesting is autoformalization is now happening.”

“You can now give, uh, an LLM a math paper and it can spit out the Lean code version of it in, you know, a fraction of the time it would've taken a team of humans to do the same thing.”