Lean encourages long unsupervised play

  • Quanta article says: “So he powered through and finished the proof. But afterward, he wasn’t certain that what he had done was correct. The reason was more than the hazy circumstances in which he’d cleared the final hurdle. The proof was so complicated Scholze knew it was possible he had missed something.”

  • Shakey ground prevents “Mind like water” needed to be Absorbed in coding. Need a system to Close open loops;

  • Lean does not need to sleep, write grant proposals, spend time with family, or teach other students — so I can interact with it for as long as I want without worrying about overstaying my welcome.

  • A portable system of mathematical “elders”, to use Buzzard’s words.

  • Makes it easier to coordinate when you Lean together or Invite collaborators from developing places where there aren’t many mathematical elders. Personal computers for people with limited resources;

  • Buzzard says: “We can just state the things that the elders believe. I don’t care about proving them, that’s harder. We can just state them and then we’ve made a big database of our beliefs. We’re writing down our belief system. And that database doesn’t exist anywhere. This is a completely new kind of database. Then what we can do, we can start attaching things to the labels, saying this was proved by this person in this journal. And suddenly we can start searching it because you guys can do that stuff. And then we can start asking basic questions. I don’t know what we can do. That seems trivial, and that would be great. That will make mathematicians in the third world that don’t have – I have access to the elders, some of them work in the same building as me – but people that don’t have access to the elders, they can use the database…Instant feedback, that’s what they want. Two hundred and seventy students to me, I find it very very difficult to give them feedback. They write some stuff on paper, it goes into the machine, a week and a half later it comes back. And this gives them instant feedback. And then, ofcourse world domination. Then I can give up. That’s it. Thank you.”

  • Positive interactions to achieve the same end-result;

  • Lean gives me courage to play with math. It is in principle impossible to be wrong when doing math with Lean: You can define any structure you want, and whatever theory you develop around this structure is valid as long as it does not contain “sorries”.

  • Can you enhance the gameplay experience with a kind of Lean videogame?