Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

Lean 4 is an open-source project maintained by the Lean FRO. External contributions are welcome, but the team has learned from experience that accepting every PR leads to hard-to-maintain code, performance regressions, and bugs. The guidelines below are designed to help contributions succeed on the first pass, protect the long-term quality of the codebase, and make the review process efficient for everyone involved.

​
Before You Open a Pull Request

​
Start with an issue

Always open an issue before writing code. This is the single most important rule. An issue lets you confirm that the team agrees the problem exists and that your proposed direction is sound, before you invest time in an implementation. For new features, prefix the issue title with RFC: (request for comments): 
RFC: add `omega` decision procedure for linear arithmetic
In your RFC, address:
  • User experience: How does this feature improve the day-to-day experience of Lean users?
  • Beneficiaries: Which users and downstream projects benefit most?
  • Community feedback: Have you discussed this on the Lean Zulip or in other issues?
  • Maintainability: Does this simplify the codebase or add significant long-term maintenance burden?
Take the time to summarize all discussion in the issue body. The triage team evaluates proposals from the issue, not from scrolling through a Zulip thread.

​
Help-wanted issues

If you are looking for a contribution that is already confirmed as desirable, browse the issues tagged help wanted. Post a comment on the issue before starting work to avoid duplicate effort and to get early guidance.

​
Understand the project

Read recent commits, open issues, and the development workflow documentation before starting. Make sure your proposed change aligns with the project’s current priorities. Regularly rebase or merge from master so your branch does not diverge.

​
Quality Standards

​
Focused changes

Each PR must address a single, clearly defined issue or feature. If your work touches multiple unrelated concerns, split it into multiple PRs. Reviewers should be able to understand the entire diff in one sitting.

​
Tests

Every bug fix must come with a regression test that would have caught the bug. Every new feature must come with tests covering the key behaviors. Place tests in the appropriate subdirectory under tests/ — see Development Workflow for the layout.

​
Documentation

Update inline comments, docstrings, and any relevant documentation to explain the reasoning behind your changes. If your PR adds a public API, add a docstring. If it changes behavior visible to users, update the relevant .md or .mdx files.

​
Code style

Follow the existing code style. Use Lean’s built-in standard library features; do not reinvent data structures that already exist. Run the test suite before opening a PR and make sure all checks pass — the maintainers will not review a PR with failing CI.

​
Submitting a Pull Request

​
PR title and description

The PR title becomes the squash-merge commit subject. It must follow the commit convention: 
feat: add simp lemmas for Nat.succ_le_iff
fix: prevent stack overflow in `whnf` for deeply nested let-bindings
doc: clarify `@[extern]` calling convention for borrowed arguments
The PR description becomes the commit body. It must:
  1. Explain what changed and why
  2. Start with "This PR " if a changelog-* label is present
  3. Reference related issues: Closes #1234
Links to Zulip threads are not acceptable as a PR description. You are responsible for summarizing the relevant discussion in the description itself.
Put questions, alternative approaches, and context that should not appear in the permanent commit history into a first comment on the PR (not the description).

​
AI contributions

Any assistance from Generative AI tools (GitHub Copilot, Claude, ChatGPT, etc.) that contributed to the final PR must be disclosed in the PR description. Authors are fully responsible for manually reviewing, testing, and understanding every line before opening the PR. PRs authored solely by AI — where the human author has not meaningfully reviewed the output — may be closed without further comment.

​
Stay responsive

Once your PR is open, respond to reviewer feedback promptly. The team will close any PR that has been inactive for more than a month (no response or updates from the author). If you need more time, leave a comment to keep the conversation open.

​
Continuous integration

All CI checks must pass before reviewers will look at a PR. Failed checks delay the process. Common CI failure modes:
  • Test failures: run make -C build/release test locally before pushing
  • Stage0 changes: if you need to update stage0, follow the process described in Development Workflow
  • Mathlib breakage: if your PR touches the parser, elaborator, or a heavily used API, consider testing against Mathlib by rebasing onto nightly-with-mathlib

​
The Triage Team and Review Process

The lean4 repository is managed by the Lean FRO’s triage team, which aims to provide initial feedback on all new bug reports, PRs, and RFCs weekly. Initial triage assigns one of the following priority labels:
LabelMeaning
P-highThe team will work on this issue / review this PR
P-mediumThe team may address this if time permits
P-lowThe team is not currently planning to work on this
(closed)Already fixed, not a real issue, or incompatible with the roadmap
For bug reports, the priority reflects the team’s commitment to fixing the bug. For PRs and RFCs, it reflects commitment to reviewing and guiding the contribution to an acceptable state. Accepted RFCs receive the label RFC accepted and are then assigned an implementation priority like a bug report.
A P-medium or P-low label on a bug does not mean an external PR fixing it will receive the same treatment. A well-crafted PR for a P-low bug can still be reviewed and merged quickly if the change is clean and the tests are solid.

​
What to expect

  • Be patient: the number of full-time maintainers is small relative to the volume of contributions.
  • Engage constructively: treat review comments as feedback about the code, not personal criticism.
  • Not all PRs are merged: even high-quality PRs may be declined if they do not align with the project’s direction. The triage priority on your RFC is the best signal of whether to invest in an implementation.

​
Commit Convention Reference

All PRs are squash merged. The commit message is taken from the PR title and body. Follow this format: 
<type>: <subject>

<body>

<footer>
Types: feat, fix, doc, style, refactor, test, chore, perf Subject: imperative present tense, lowercase first letter, no trailing period Body: imperative present tense; if changelog-* label is present, begin with "This PR " Footer (optional):
  • Breaking changes: describe the change, justification, and migration path
  • Closes #123, #456
Example: 
fix: prevent double-free when `lean_ctor_release` is called on a scalar

This PR guards `lean_ctor_release` with a scalar check so that calling
it on a tagged-pointer value (which should never happen but can occur
with incorrect FFI code) does not attempt to dereference the pointer.

Closes #5678

Build docs developers (and LLMs) love

Get started for freeTalk to us