Lean Theory Repository Profile¶

The lean-theory-repository profile applies accountable surface rules to Lean theory repositories.

Scope¶

This profile covers repositories that contain Lean theorem development, reference TOML encodings, generated contracts, validation commands, and release automation.

Required self-protection¶

A repository using this profile MUST declare .accountability/surfaces.toml as an authority manifest surface.

AI authority over the authority manifest MUST be prohibited.

The required role terms are defined by accountable-surface-vocabulary. The manifest structure and self-protection rule are defined by accountable-surface-spec.

Profile-specific expectations¶

A Lean theory repository using this profile SHOULD declare protected surfaces for:

• Lean build and toolchain configuration;
• Lean public modules;
• reference TOML artifacts;
• generated contract artifacts;
• validation commands;
• release-affecting workflows;
• repository identity metadata.

Changes to Lean public surfaces SHOULD require theory review.

Changes to generated contracts SHOULD require evidence that generation, validation, export, and catalog checks passed.

Concrete examples are provided in examples/lean-theory-repository/surfaces.toml.

Required review¶

Changes to Lean public surfaces SHOULD require theory review.

Changes to generated contracts SHOULD require human review and evidence that the generation and validation commands passed.

Changes to release workflows SHOULD require release review.

Typical evidence¶

Typical evidence includes:

• Lean build result;
• test result;
• schema validation result;
• export check result;
• catalog check result;
• manifest validation result;
• decision note;
• human review record.

Boundary rule¶

Lean theory repositories may contain both formal theorem surfaces and operational reference artifacts. The manifest must keep these roles inspectable rather than collapsing them into a single generic source-code category.