Make provenance a required project-card field

.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

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/<YourProject>/`, 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/<YourProject>/`, 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
 

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/<YourProject>/`, 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/<YourProject>/`, 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
 

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/<YourProject>/`, 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/<YourProject>/`, 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
 

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"]):

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.