Skip to main content


This is the Lean prover community blog. There is no predefined list of authors. Everybody can submit a pull-request with a post in this folder. If you are unsure whether your post will be welcome then don't hesitate to first discuss the topic of your post on Zulip before investing too much time writing it. The kind of posts we expect include:

  • posts highlighting some new contributions to mathlib
  • news about ongoing project such as the Liquid tensor experiment or the sphere eversion project
  • news about exciting developments in other proofs assistants
  • announcement of conferences and talks
  • some explanations of specific topics in a less formal context than the documentations
  • speculations about future developments or somewhat philosophical discussions