Recommendation: A first mathlib pull request works best as one docstring fix or one missing lemma inside an existing theory, built locally with lake build and opened from a fork against leanprover-community/mathlib4. Any AI assistance has to be disclosed in the PR description, and the contributor must be able to explain every line without it.

A good first contribution

The mathlib contribution overview says that small fixes, such as docstring corrections, and single-lemma additions to existing theories are almost always welcome. A new theory is different. It needs to fit the maintainers' interests and usually starts as a discussion in the #mathlib channel on the Lean Zulip. Work outside that scope can live in a separate repository that depends on mathlib.

Two kinds of first PR are easy to scope:

A docstring correction: an existing declaration whose documentation omits a hypothesis, for example a nonzero condition that the type requires. The fix changes text only, but still needs the mathematical understanding to describe the hypothesis correctly.
A single lemma: a small fact that a proof elsewhere needs and that belongs next to related lemmas. Searching the library first, with exact? in the editor or the mathlib documentation search, confirms that it is actually missing.

The whole process, from the change to review, fits on one map:

Mind map of a first mathlib pull request, from one scoped change through fork and branch, local checks and library fit to a PR against leanprover-community/mathlib4 and CI review

Fork, clone and branch

Mathlib's contribution workflow starts with a fork of leanprover-community/mathlib4 on GitHub, then these commands:

git clone https://github.com/<username>/mathlib4.git
cd mathlib4
lake exe cache get
git switch -c my-first-lemma

git clone .../<username>/mathlib4.git: copies the fork, so origin points to the contributor's own repository. Branches are pushed there, and the PR is opened from the fork.
lake exe cache get: downloads precompiled .olean files for the current commit. Without it, the first build compiles the whole library, which takes hours.
git switch -c my-first-lemma: creates and checks out a new branch for this one change. Each PR gets its own branch.

The lean-toolchain file in the repository names the exact Lean version. elan, the Lean version manager, reads it and installs that version automatically. The Git guide for mathlib contributors covers the one-time setup in more detail.

Local checks before pushing

After editing, the change has to compile:

lake build Mathlib.Algebra.Group.Basic
lake build
lake exe mk_all

lake build Mathlib.Algebra.Group.Basic: builds one module and the files it imports. This is fast and catches errors in the edited file.
lake build: builds the whole library, including every file that imports the edited one. Files low in the import hierarchy can take a long time. Pushing and letting CI run the full build is also accepted.
lake exe mk_all: needed only when the PR adds a new file. It updates Mathlib.lean so the new file is imported.

The branch must compile without sorry. A PR that still has gaps can be marked work in progress, covered in the labels section below.

Names, style and documentation

A PR that compiles can still need revision if it does not match the library's conventions. Three guides set them:

Naming conventions: a lemma's name describes its statement, so other contributors can guess it. mul_inv_cancel states that a * a⁻¹ = 1, read left to right.
Style guide: line length, indentation and declaration layout. Style fixes that follow the guide are welcome. Other style-only changes need agreement on Zulip first.
Documentation guide: module docstrings and declaration docstrings. A useful docstring adds context, such as why a hypothesis is needed, instead of repeating the type in words.

New lemmas go next to the related results, in the same namespace and section. Reading the surrounding file shows which variables and implicit arguments are already in scope.

The PR description and labels

The PR is opened against leanprover-community/mathlib4, not against the fork's master branch. The title follows mathlib's commit conventions:

feat(Algebra/Group/Basic): add lemma about <statement>

feat: the change type, here a new lemma. The angle brackets mark a placeholder for the short description of the statement. fix, doc, chore and refactor are other common types. A docstring correction uses doc.
(Algebra/Group/Basic): the scope, usually the edited file's path under Mathlib/.
The subject describes the change in the imperative mood, as mathlib's commit convention requires.

The description explains the gap, why nearby lemmas did not already cover it, and which checks ran. Moved or deleted declarations are listed at the bottom of the description under Moves: and Deletions:, above the --- line. Notes for reviewers go below that line.

Anyone can add or remove labels by posting a comment with the label name on its own line:

Comment	Meaning
`WIP`	Work in progress, for example with `sorry` still in the branch
`easy`	Trivial change, typically under 25 lines with no changed definitions or statements
`awaiting-author`	Set by reviewers after comments, removed with `-awaiting-author` once addressed
`LLM-generated`	The PR contains a substantial amount of LLM-generated code

gh pr status shows CI results from the terminal. After CI passes, lake exe cache get downloads the compiled files for the branch.

AI tools and contributor responsibility

Mathlib's AI policy splits into three parts:

Mind map of mathlib's AI policy: AI-assisted code allowed with disclosure and the LLM-generated label, LLM-written comments not allowed, and full understanding always required

Disclosure: a contributor who used AI explains in the PR description which tools were used and how. A PR with a substantial amount of LLM-generated code also gets the LLM-generated label.
Comments: using an LLM to write comments on GitHub or Zulip is not allowed. Replies to reviewers are in the contributor's own words.
Understanding: the contributor must understand all AI-written content. Reviewers close low quality LLM-produced PRs without comment, and repeated low-effort PRs can lead to a ban.

A practical test before submitting: explain the proof without looking at the tactic script. If the explanation cannot say why the hypotheses are enough, the PR is not ready.

Frequently asked questions

How small can a first PR be?

A one-line docstring correction is a valid PR. Small, self-contained PRs are reviewed faster because a reviewer can check the whole change at once.

Does the full `lake build` have to finish locally?

No. The workflow guide accepts pushing the branch and letting CI run the full build. The edited module should still build locally first, so CI does not fail on a basic error.

Can an AI assistant write the proof?

Yes, if the PR description discloses it, substantial generated code carries the LLM-generated label, and the contributor understands and can defend every line. Comments in the review discussion must be written without an LLM.

A workspace for contribution practice

The informal argument, source references and open questions can sit in a note next to the proof branch. Oyren's Lean and LaTeX notes keep that note beside the formal work. The Lean 4 and mathlib in cloud VS Code guide covers running the same lake commands in a browser editor.