Isabelle Community Conventions

This repository contains style guidelines for the development of projects with the Isabelle proof assistant. Many of these guidelines have been adapted from the very successful Lean mathlib contribution guidelines.


We start with the most important rule: Every commit/pull request must comply with the standards listed in this document.

This might seem like a lot of work at first, but experience has shown that a consistent commitment to such rules means:

  1. High quality of theories due to uniform conventions and documentation
  2. Easy collaboration due to (1) (searchability, uniformity) and a flexible as well as transparent contribution model
  3. Quicker development in the mid-term and long-term due (1) and (2)


The guidelines cover the following topics:

Get Help and Join The Community

This Zulip chat is where some of the Isabelle community, in particular the creators of these guidelines, hang out. We are always happy to help you and try to answer your questions, no matter if they are basic or advanced.