Developers

Package Registration Guide

How to register new Lean mathematical packages and audit certificates to the NPA registry.

To maintain the integrity of our verified math registry, new packages must supply cryptographic signatures and verify configuration rules. Follow this guide to prepare your package for registration.

1. Set Up Package Manifest

Every mathematical repository must contain an npa-package.toml file at its root. This defines the package version, dependencies, license, and module pathways.

schema = "0.1.0"
package = "my-math-library"
version = "0.1.0"
license = "Apache-2.0"
description = "Verified theorems for group actions and rings."

2. Generate Certificates (.npcert)

Use the NPA CLI compiler tool to build your Lean files and compile the verification certificates. Place the .npcert signatures in your generated build folder.

npa package compile --manifest npa-package.toml

3. Verify Locally

Run the verify-certs commands on your local environment to ensure all signatures and hashes match the files perfectly before submission.

npa package verify-certs --root . --checker reference

4. Submit a Pull Request

Add your package configuration to repositories.yaml on this website's repository, and submit a Pull Request. Our CI gates will automatically audit your certificates before merging.