Lean together

• If you Lean together then theory development is a software engineering group project.

  • Theory development company;

• Inclusive like the Lean-prover community: On Zulip or Discord we can gather. Quanta article says:

  • “Last October, Quanta wrote that the collective effort to write mathematics in Lean has the “air of a barn raising.” This project was no different. Commelin would identify discrete parts of the proof and post them to Zulip, a discussion board that serves as a hub for the Lean community. When mathematicians saw a part of the proof that fit their expertise, they’d volunteer to formalize it.”

  • “It’s one big collaboration with a lot of people doing what they’re good at to make a singular monolith.”

  • Work with the garage door up;

    • The Cathedral and the Bazaar;

  • Invite collaborators from developing places;

• Lean encourages long unsupervised play when participants can Start from others evergreen notes;

• Nielsen’s Ted talk: “as driving is to pushing a car”.