> I am at a loss about what to do with these results.

I would recommend publishing them to Palomar (https://palomar-registry.org/) - I have no affiliation, this is an online registry of Lean-verified proofs created by Terrence Tao.

I have submitted a proof there that's also minorly important in an extremely niche field.

Anyway, I feel like it's a good place to dump AI slop lean proofs because the main point of the registry is that it verifies that: 1) your Lean challenge statement is the same as what you informally state you're trying to prove; 2) your Lean proof actually compiles.

This could be useful to future AI slop researchers who want to know if a given result has already been formalized, and they may be able to mine some lemmas from your work. Also, it's good to know for the field in general what has been proven.

I'm fairly certain you can set your publishing name to be whatever you want, so you could set it to be just the word "Anonymous", or the name of the model you used.