Lean and Mathematical - Is It a Means of Building Intuitions?

"I've had some experiences with lean where, because lean is so much like a video game. I'm no longer actually thinking bout mathematics. I'm just playing the video game," he says. "It's like, you know, thiss the joy stake, and you have to jump up at the right time."...