I think there's a typo in the [second line of mathd_numbertheory_35](https://github.com/openai/miniF2F/blob/4e433ff5cadff23f9911a2bb5bbab2d351ce5554/lean/src/valid.lean#L693). It should be `∀ (n : S)`.