The speaker says OpenAI and Anthropic are doing mathematics and translating it into Lean without necessarily considering whether the work uses the correct level of generality.

“Uh, we could just bash something out and formalize a paper that came out last week. You know, and indeed this is what's happening. You know, companies like OpenAI and Anthropic are doing mathematics and then just translating it into Lean and not really thinking about whether this is all done in the correct generality.”