I don't hate AI preprints, I hate slop grenades, which is what this is. Either you did that on purpose (which was what I thought looking at your website - that you created a honeypot to trap agents) or you don't realise that's what you're doing, in which case this makes me very sad.

It's tragic that you spend time harassing and diminishing about your subjective aesthetic response instead of learning to check the machine-checkable proofs using the tools.

Test coverage in Lean might be a good feature to contribute.