The speaker says models are becoming expressive enough that correctness can be verified without requiring every output to be in Lean code.

“Lean can tell you which ones those are. Uh, at the same time, right, the expressive power of the models is getting so much better that you don't need everything to be outputted in Lean code to verify its correctness.”