diff --git a/.github/CODE_QUALITY.md b/.github/CODE_QUALITY.md index b72d9bbcbb..85aaad4821 100644 --- a/.github/CODE_QUALITY.md +++ b/.github/CODE_QUALITY.md @@ -31,9 +31,10 @@ Current checks: - no Lean content file exceeds 10000 non-blank, non-comment code lines - no theorem/lemma proof body exceeds 200 non-blank, non-comment code lines, using the current text heuristic - `LeanPool/projects.yml` exists, is valid YAML, and contains a `projects` list -- project entries have required fields: `slug`, `title`, `entry_module`, `authors`, `source`, `status`, `main_declarations`, and `tags` +- project entries have required fields: `slug`, `title`, `entry_module`, `authors`, `source`, `status`, `provenance`, `main_declarations`, and `tags` - project entries also carry documentation metadata: `summary`, `branch`, `main_results`, and `msc` - project `status` is `verified` +- project `provenance` records who wrote the Lean proofs and is one of `human`, `AI`, or `mix` (see [`candidates/provenance.md`](../candidates/provenance.md) for the rubric): `human` when the proofs were written by people, `AI` when they mostly came from an AI system, and `mix` when both contributed substantially - project `source` includes at least one recognized primary source key among `arxiv`, `doi`, and `url` (more than one is fine) - project authors, main declarations, and tags are nonempty string lists - project summaries and branches are nonempty strings, MSC codes are a nonempty string list, and `main_results` is a nonempty list of `declaration` / `informal` entries diff --git a/AGENTS.md b/AGENTS.md index 394e29c358..2e994bbecf 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -53,9 +53,9 @@ If you would like to withdraw your project from Lean Pool, open an issue. There are two paths: - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt). -- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml), and regenerate the index with `lake exe mk_all`. +- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the index with `lake exe mk_all`. -Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) +Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) ## Dev setup diff --git a/CLAUDE.md b/CLAUDE.md index 394e29c358..2e994bbecf 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -53,9 +53,9 @@ If you would like to withdraw your project from Lean Pool, open an issue. There are two paths: - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt). -- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml), and regenerate the index with `lake exe mk_all`. +- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the index with `lake exe mk_all`. -Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) +Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) ## Dev setup diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a817dae058..8dff437cf9 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -11,9 +11,9 @@ If you would like to withdraw your project from Lean Pool, open an issue. There are two paths: - **Propose a repo.** Open an issue with the GitHub URL and a maintainer can import it. Repos that Reservoir does not index can be added to [`candidates/manual.txt`](candidates/manual.txt). -- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml), and regenerate the index with `lake exe mk_all`. +- **Open a content PR.** Add your project under `LeanPool//`, register it in [`LeanPool/projects.yml`](LeanPool/projects.yml) — the card must declare `provenance` (`human`, `AI`, or `mix`; see below) — and regenerate the index with `lake exe mk_all`. -Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) +Either way the result must pass CI (build, linters, and quality checks — see [Linting and testing](#linting-and-testing)) and an [LLM review](.github/REVIEW_RULES.md) of fit and significance. Accepted projects must be `sorry`-free, introduce no axioms beyond `Classical.choice`/`propext`/`Quot.sound`, and avoid `unsafe`/`partial`. Each project card must also declare its **provenance** — who wrote the Lean proofs — as `human` (written by people), `AI` (mostly produced by an AI system), or `mix` (both contributed substantially). (Proof profiling via `/profile` is available but informational, not a gate: added files get an absolute profile, while modified files get a base→head compile-cost comparison — useful for checking that a refactor doesn't regress compile time.) ## Dev setup diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 27411b6e3d..f46016793f 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -24,6 +24,10 @@ # Permissive SPDX licenses accepted for Lean Pool projects (Apache-2.0 or MIT, # per CONTRIBUTING.md). Every project entry must declare one; enforced below. LICENSE_VALUES = {"Apache-2.0", "MIT"} +# Provenance of a project's Lean proofs: written by a human (`human`), by an AI +# system (`AI`), or by a mix of both (`mix`). Every project entry must declare +# one; enforced below. See candidates/provenance.md for the rubric. +PROVENANCE_VALUES = {"human", "AI", "mix"} # Kept identical to partial_port_audit.GITHUB_REPO_RE on purpose: a project is # auditable for partial imports only when source.github_repo matches this # `owner/name` shape, so the quality gate must reject exactly what the audit @@ -704,6 +708,7 @@ def _check_required_project_fields( "source", "license", "status", + "provenance", "main_declarations", "main_results", "tags", @@ -737,6 +742,15 @@ def _check_project_values( f"(expected one of {', '.join(sorted(LICENSE_VALUES))})", ) ) + if "provenance" in project and project["provenance"] not in PROVENANCE_VALUES: + errors.append( + _QualityError( + path, + 1, + f"project #{index} has invalid provenance " + f"(expected one of {', '.join(sorted(PROVENANCE_VALUES))})", + ) + ) if not _source_is_valid(project["source"]): errors.append(_QualityError(path, 1, f"project #{index} has invalid source")) elif not _has_github_repo(project["source"]): diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index bee4ffb0be..1aabbb0030 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -61,6 +61,7 @@ def _write_project_yaml(root: Path, projects: list[dict[str, str | None]]) -> No *source_lines, f" license: {project.get('license', 'Apache-2.0')}", f" status: {project.get('status', 'verified')}", + f" provenance: {project.get('provenance', 'human')}", " main_declarations: [hello]", " main_results:", " - declaration: hello", @@ -348,6 +349,7 @@ def test_quality_check_does_not_honor_size_marker(tmp_path: Path) -> None: "source": {"arxiv": "1234.5678"}, "license": "Apache-2.0", "status": "verified", + "provenance": "human", "main_declarations": ["hello"], "main_results": [{"declaration": "hello", "informal": "A test result."}], "tags": ["test"], @@ -524,6 +526,34 @@ def test_quality_check_rejects_non_permissive_license(tmp_path: Path) -> None: assert any("invalid license" in error.message for error in errors) +def test_quality_check_requires_provenance(tmp_path: Path) -> None: + """Every project entry must declare a `provenance` field.""" + _write_minimal_repo(tmp_path) + _write_project_yaml(tmp_path, [{"slug": "p", "entry_module": "LeanPool.Basic"}]) + projects = tmp_path / "LeanPool" / "projects.yml" + projects.write_text(projects.read_text().replace(" provenance: human\n", "")) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any( + "missing fields" in error.message and "provenance" in error.message + for error in errors + ) + + +def test_quality_check_rejects_invalid_provenance(tmp_path: Path) -> None: + """Provenance must be one of `human`, `AI`, or `mix`.""" + _write_minimal_repo(tmp_path) + _write_project_yaml( + tmp_path, + [{"slug": "p", "entry_module": "LeanPool.Basic", "provenance": "robot"}], + ) + + errors = run_checks(tmp_path, skip_lean_axioms=True) + + assert any("invalid provenance" in error.message for error in errors) + + def test_axiom_audit_resolved_parses_success_lines() -> None: """`#print axioms` success lines populate the resolved set; _root_ stripped.