Leo felt that responding to user-support questions and mathematicians' queries left him unable to find time to move Lean toward his intended vision.

“We're currently on Lean 4, but for years, you know, we were at Lean 2. And J- uh, Leo saw where he wanted it to go, and he felt inhibited in his ability to actually find the time to do it because he was answering all these essentially, like, user support questions and, uh, queries from mathematicians.”