Split project cards and remove the shared import list

[Vilin97]

Independent projects currently share one registry and a generated root import list, causing avoidable merge conflicts. This moves the current 291 projects to one YAML mapping per slug and makes LeanPool.lean fixed while Lake discovers all modules.

Every project-card field is preserved exactly. Existing mathematical sources and public Imports.lean files are unchanged. The only changed paths are LeanPool.lean, the removed LeanPool/projects.yml, and LeanPool/projects/*.yaml.

Validation: exact equality of all 291 registry mappings; generated-index consistency; NOTICE consistency; 679 full Python tests passed with 2 skipped; 98 focused registry, index, attribution, aggregator and workflow-contract tests; whole-pool static quality checks. Hosted build and queue validation will run on the rebuilt main-based head.

The maintainer authorized merging PR610 and PR611 without waiting for exposition. The maintainer subsequently authorized bypassing outstanding CI after 2026-10-08 08:31:47 UTC if it has not passed. No passing hosted result is claimed before it completes.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium risk] Reorganizes project metadata from a single list into individual files.

Fix the older-branch rebase path before merging this registry deletion.

Summary

Moves 291 project cards into separate YAML files and replaces the shared root import list with a fixed LeanPool.lean.

• Older branches that edit the deleted registry can break automatic rebase and Mathlib-update workflows.
• Lake discovery and the inspected registry readers support the new layout.
• Vilin97 explicitly described removing the root imports as intentional; that API change is not reported.
• The complete card diff and exact equality of all mappings were not fully verified. No tests or hosted builds were verified during this review, and doc-gen4's implementation was unavailable.

_{Reviews (1) · Last reviewed commit: "Split the current project registry into ..." · Reviewed by Greptile}

[greptile-apps]

Comments Outside Diff

These findings could not be posted inline.

•  Older PR updates fail LeanPool/projects.yml:1 ▶

  Deleting LeanPool/projects.yml breaks automatic updates for older project PRs that added a card to that file. Merging the new main produces a modify/delete conflict. The rebase workflow accepts that conflict as repairable, then runs git show origin/main:LeanPool/projects.yml. The file is now absent, so the step exits before updating the branch or flagging it for manual repair. The workflow that resumes Mathlib updates has the same missing-file read.

  Teach these workflows to move the older branch's additions into separate cards, or stop cleanly and flag the branch for manual repair.