Repository navigation
feat(docs): build a checked registry of formalized results and source papers #2012
Description
Create a searchable registry connecting named formalized results and their mathematical sources to exact public Lean declarations. Requested by the user. The existing formal-abstract catalogue (#416/#421) intentionally selects headlines; #585 supplies a guide, and references.bib records citations without distinguishing background references from formalized results. The old paper/TeX index stays retired.
Worker: Codex codex-t3-8d548603, branch feat/results-registry-inventory.
The registry should record result titles, subject areas, bibliography keys, precise source theorem/section locators, implementing Lean modules/declarations, and model/encoding/resource limitations. A paper may have several formalized results without being fully formalized. Distinguish library original results, source-correspondence review status and partial/weaker variants; citation presence alone is not evidence of formalization. Reuse the bibliography and selected abstract metadata instead of maintaining duplicate summaries, and link optional abstracts rather than requiring an abstract for every result.
Milestones:
- Start a durable inventory: reuse all selected abstract entries and collect a first cross-area set of additional named results with inspected Lean statements and existing source references. Record coverage gaps and unverified source correspondences explicitly.
- Check registry references in CI: unique IDs, valid bibliography keys, imported/public theorem declarations, real module/source/doc targets and valid abstract links. A rename/removal should fail validation. Tests must include broken-reference cases. Mathematical correspondence still requires independent review.
- Publish a browsable/searchable results-by-topic and papers-by-result view, sharing the API docs' declaration links. Make the first collection reviewable before introducing a large presentation layer.
- Audit coverage area by area and document how additions stay current. Do not claim a comprehensive inventory merely because all current entries validate.
Completion of the broad issue requires the coverage audit and discoverable published registry, not just initial data or a working checker. The initial worker deliverable is the bounded collection/checking milestone; remaining coverage and presentation work stays visible here. Preserve source/formalization credit. AI-assisted implementation and independent review use Codex.
User direction: author the registry in human-readable Lean commands with actual theorem identifiers checked during compilation; machine-readable JSON is generated output. Source references must include a separate paper theorem name/number and section/page locator, with uncollected details explicitly marked rather than guessed.
Activity
chris-ai1 commentedon Oct 31, 2026
Initial collection and reference-checking milestone is ready in #2014, with independent Codex review recorded there. It reuses the selected abstract catalogue, adds eight non-headline result groups, and generates indexes by topic or cited bibliography key. Reference integrity is checked against fresh compiled public theorem metadata; source correspondences and missing locators remain explicitly recorded/pending rather than newly source-verified.
The issue stays open for broader area coverage, precise paper-to-result audits, original-result representation and published search/navigation. This is an inventory milestone, not a claim that all results or papers have been catalogued. Worker
codex-t3-8d548603, branchfeat/results-registry-inventory, ready for coordinator integration: required hosted validation, including the registry reference check, passed on the independently reviewed revision. Data, validation and review evidence are on the PR.feat(docs): seed a checked results and reference registry (cslib-comm…
chris-ai1 commentedon Oct 31, 2026
active — worker
codex-t3-8d548603, branchrefactor/lean-results-registry, following the user’s explicit request: migrate the initial eight collected records from hand-maintained JSON into human-readable Lean commands whose theorem identifiers resolve during compilation. Store elaborated records in an environment extension and export machine-readable data for the existing catalogue adapter/index generator. Retain current source-review/scope labels, reuse selected abstract metadata, remove the superseded authored JSON and check invalid references/duplicates in compilation regressions. Bibliography keys remain checked against the authoritative bibliography in CI. This changes registry representation, not mathematical statements or the broader coverage objective.chris-ai1 commentedon Oct 31, 2026
The user-requested Lean authoring migration is ready in #2033, with independent Codex review recorded there. Canonical entries now live in
ComplexityResults/Entries.lean; ordinary builds resolve their theorem identifiers, while the existing fresh original-kind audit remains in CI. JSON and the topic/paper indexes are generated from compiled metadata. The eight existing scopes and selections are preserved.Paper theorem names/numbers and section/page locators are separate fields. The recorded FO Theorem 3.1 identifier is retained; the other missing source identifiers remain explicit
unverifiedmarkers and still need collection/review. Broader coverage, source audits and publication/search remain open here. Workercodex-t3-8d548603, branchrefactor/lean-results-registry, ready for coordinator integration: full hosted validation passed and independent review approves the current revision.Review follow-up for the source-audit milestone: when verified correspondences are added, replace the exporter’s hard-coded
recordedstatus with explicit entry/source review metadata. All current entries remain recorded, not newly source-verified; this is not a blocker for the migration.refactor(docs): author result registry entries in Lean (cslib-communi…