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

Introduction

We start with the most important rule: Every commit/pull request must comply with the standards listed on this website. This might seem like a lot of work at first, but experience has shown that a consistent commitment to such rules results in:

  1. High quality of theories due to uniform conventions and documentation
  2. Easy collaboration due to point 1.; in particular, it improves searchability and uniformity of theories and offers a flexible as well as transparent contribution model
  3. Quicker development in the mid-term and long-term due points 1. and 2.

Table of Contents

The guidelines cover the following topics: