google-deepmind / google-deepmind/formal-conjectures

Add metadata integrity checks to CI

Open
#3,973 2 comments 1 reaction 0 assignees View on GitHub
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.