Github should consider this a coordinated spam effort, and (shadow)ban accounts which create PRs consisting of only a `mikotea9` or `tea.yaml` file
I agree in cases like this GitHub should take action, but in general it would be nice to let people set their own filters as it allows maintainers to prevent abuse more specific to their project, instead of letting GitHub themselves chase things around, and makes it easy to fix the next major spam event that comes around.