Lean in Zulip 9.0 blog post

Stream: Zulip meta

[Alya Abbott]

In case folks didn't see it, we gave this community a shout-out in the 9.0 release announcement blog post:

• The Lean Prover community has kicked off a multi-year collaboration on Zulip to formalize a proof of Fermat’s Last Theorem. We wish them the best of luck!

  “The project will be run on the FLT channel on the Lean Zulip chat, a high-powered research forum where mathematicians and computer scientists can collaborate in real time, effortlessly posting code and mathematics using a thread and channel system which admirably handles the task of enabling many independent conversations to happen simultaneously.”

  — Kevin Buzzard, announcing The Fermat’s Last Theorem Project