I'm not a mathematician but it seems to me that if all it took to solve the problem was an enthusiast level understanding of the domain and a few hundred dollars of tokens then the result probably isn't that valuable. Even assuming you are the first person in the world to solve it, these kinds of LLM-friendly problems that are now easy to solve and easy to verify will almost certainly be picked off by one person or another in the near future.

It's also possible that the result is already known and you just weren't aware of it. It's easy for someone outside of a field, or even one steeped in it, to not be aware of certain solutions.

> 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.

It is interesting isn't it.

You asked for a painting. A robot made the painting. You looked at it and said, "well, I guess it's good. Should I put it online or something? Dunno. Hey Fred, what do you think of this?"

Meanwhile, your next door neighbor spends their entire life developing their understanding of life through art. They "understand" (maybe not in a way they can articulate) art. You go next door, you look at their painting and say, "well I guess it's good." But you also understand that your neighbor is just like you, and maybe you are a painter in another way.

I find it strange that, people can't see that, we don't need to solve hunger and poverty and work balance, and etc, by a round-about make-super-intelligent-AI. We could just solve it. It's pretty obvious how to, as well.

We can all be painters, if we put restrictions on the psychopaths.

How do you know the proofs are correct?

I mean, let's say you spun up a swarm of agents to rewrite a large component of a well used open source library to be memory safe. You could dump it in a big PR and walk away (we all know how that would go), or you could try engaging, see if they're interested, write something up and see where it goes.

The biggest problem is, IMO, drivebys uninterested in actual results, just getting a check mark, and the equivalent of dropping a 200k line PR on people and expecting them to be interested and do the work for you. These are things many on HN are familiar with and know how to do better :)

It depends.

If you are trying to understand better the field, then do a good write up of the proofs so that people can learn from it.

If you want to earn the respect of people because you found interesting proofs. Then do a good write up of the proofs so thst people can learn from it.

If you want to plant flags and pollute peoples minds. Then please publish it anonimously, no one wants to correct LLM slop for you.

Probably we should build a repository of AI slop proofs that are only allowed to be publish anonimously. That way people may be more inclined to work on it because they would feel like they are cleaning your house for free.