Keep the pull request precise
For a correction, API improvement, or documentation update that does not alter the architecture, make the smallest coherent change and explain its purpose clearly in the pull request.
StatsMLlib contributor guide
How to Contribute
This guide explains how complete, reusable Lean developments in probability, statistics, and learning theory move from proposal to integration in StatsMLlib.
You are warmly welcome to contribute to StatsMLlib. Contributors whose work is integrated into the library will be acknowledged in our contributor list, ensuring that their contributions are properly recognized.
01 · Discuss
Before You Begin
Coordinate early when a contribution changes the mathematical scope or architecture. Focused corrections can remain narrow; large developments need agreement on ownership and dependencies before coding begins.
Open an issue first
Before a large formalization or architectural change, identify the mathematical result and source, propose the subject-owned module, and describe the dependencies or API questions that need agreement.
02 · Develop
Build in the Owning Layer
StatsMLlib is organized by mathematical subject, with an acyclic import direction. Search StatsMLlib first and Mathlib second, then extend the module that owns the relevant definitions.
{MeasureTheory · Topology · LinearAlgebra}→Analysis→Probability→LearningTheory→Statistics
Ground before proving
Reuse existing declarations and infrastructure. New files are reserved for mathematically distinct material or import boundaries that cannot be handled cleanly in an owning module.
No proof placeholders
Do not introduce sorry, axiom, admit, or native_decide. New code must elaborate without warning or info messages.
Document the mathematics
New modules need the established copyright and author header, ordered imports, and a module docstring describing the main definitions and results.
Preserve attribution. Existing copyright and author notices remain authoritative when code is moved, renamed, or reused. Add significant authors to the relevant source-file
Authors header; for co-written work, also add one Co-authored-by trailer per additional author.03 · Verify
Check the Whole Library
Use the Lean and Mathlib versions pinned by lean-toolchain and lakefile.lean. From the repository root, run the full verification before submitting.
LEAN_NUM_THREADS=$(nproc) \
lake build- Every proof is complete.
- The whole-library build succeeds.
- No warning or info messages remain.
- Imports respect the layer order.
- File headers preserve attribution.
- New modules include a module docstring.
04 · Submit
Open a Focused Pull Request
A reviewer should be able to understand both the mathematics and the API decision without reconstructing the development from the diff.
Record the essential decisions
- State the mathematical result and its source.
- Name the subject-owned module.
- Explain important declaration, naming, and API choices.
- Report the whole-library verification.
- Call out any preserved or newly added attribution.
Add a Git trailer
Use an email associated with the co-author’s GitHub account when the credit should appear on GitHub.
Co-authored-by: Full Name <email@example.com>Community and terms
Contribute Respectfully
Participation is governed by the project’s Code of Conduct. Unless explicitly stated otherwise, intentionally submitted contributions are provided under the Apache License 2.0 contribution terms.