The speaker says agentic coding can let mathematicians use Lean without learning its detailed syntax, which is a barrier to entry.

“It's in two ways. A, right, I mentioned the kind of writing the fiddly Lean syntax is a real barrier to entry for mathematicians. Obviously, with, like, agentic coding, you don't need to, like, learn all that Lean.”