google-deepmind / google-deepmind/formal-conjectures
Add metadata integrity checks to CI
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 328
Description
## Background
The repository already relies on a significant amount of structured metadata (`@[category]`, `@[AMS]`, `@[formal_proof]`, source collections, generated browse links, etc.) extracted into `site/data/conjectures.json`.
Many parts of the website and browsing experience implicitly assume that this metadata is well-formed and internally consistent, but most of these invariants are not currently validated automatically in CI.
While many of these checks are individually simple, automating them in CI could help reduce maintainer review overhead, prevent silent inconsistencies from accumulating over time, and provide faster feedback to contributors.
## Proposal
Add a metadata integrity workflow to CI to validate repository-wide consistency after metadata extraction.
Potential checks could include:
* AMS codes exist and are well-formed,
* categories belong to the allowed set,
* `@[formal_proof]` URLs parse correctly,
* no duplicate theorem identifiers/slugs,
* every expected theorem is extracted correctly,
* every referenced collection exists,
* ~~generated browse links are valid.~~ (already in other future PR)
The goal is not to validate mathematical correctness, but to protect the integrity of the metadata and generated site structure that the repository already depends on.
This could run as a standard GitHub Actions workflow on pull requests and pushes to `main`, following the existing extraction/build pipeline.
I plan to open this incrementally as a sequence of small PRs (roughly one validation family per PR) so each addition remains independently reviewable. I will start by opening PR 1 as a concrete illustration of the direction.
Contributor guide
Assessment
This issue has not been assessed yet.