Skip to content


Michael Kohlhase edited this page Jun 1, 2018 · 3 revisions

MathHub Libraries

The top level of organization in consists of libraries (described here) and user spaces.

A MathHub library is a public resource of flexiformal documents (e.g. a theorem prover library, a mathematical terminology base, or a logic atlas). MathHub libraries are usually developed and maintained by a community, either directly on, or imported from an external library for archiving.

A MathHub library is established by the MathHub library committee and consists of a set of MathHub math archives that contain the contents of the resource, metadata, and documentation about the resource.

Technically, a MathHub library corresponds to a GitLab group with a MathHub-specific layout:

  1. The metadata repository meta-inf for library-level metadata and documentation
  2. a set of math archives that contain the flexiformal content.

The set of libraries in MathHub can be found here.

You can’t perform that action at this time.