Overview

This project’s own library is, in effect, a small extension of Mathlib and Lean’s own core library — the table below also links to every external declaration it refers to directly.

Module Definitions Abbreviations Lemmas Theorems Difficulty
Ontology 0 0 0 0
Mathlib 153 (external)
Lean core 238 (external)