Commit 2025-06-22 14:18 27dacf78

View on Github →

chore: verify statements listed in 1000.yaml and similar actually exist (#26183) yaml_check.py was not adding entries in 1000.yaml with only a statement field to its 1000.json output, so they were not being checked by check-yaml.lean. This caused an error in the Artin–Wedderburn theorem entry to be missed, which is currently breaking the 1000+ theorems page on the website. This PR fixes the error in 1000.yaml and fixes yaml_check.py.

Estimated changes