From 60c9a24f913aeff1745b4c28adcbc953478a8b91 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 13:04:09 -0400 Subject: [PATCH] docs(AGENTS): quotations are copied from the pinned source or labeled paraphrase Samuel approved this rule on 2026-10-25 after reviewers caught several "verbatim" source quotes in PR descriptions that do not occur in the cited source. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- AGENTS.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 739ff11759..f80a463b6a 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -396,8 +396,11 @@ and [API review with explicit nonblocking nits](https://github.com/leanprover/cs When a declaration claims to formalize a cited result, the PR quotes the source statement with its exact locator and maps the source's notation to the Lean statement: quantifiers, models, encodings -and resource conventions. Reviewers check that mapping rather than an impression. New mathematics -and new proof ideas need no source; label them as original. +and resource conventions. Reviewers check that mapping rather than an impression. Text presented as +a quotation is copied from the pinned source version, with its locator checked there rather than +taken from an issue, a PR or other library text; anything else is labeled as a paraphrase. Reviewers +check quotations against the source, and a quoted passage that is not in the source blocks approval. +New mathematics and new proof ideas need no source; label them as original. Whether a new definition needs checked examples on both sides (an instance where it holds and one where it fails) is for the author and reviewers to judge; reviewers may ask for them when a