skinner_

Maybe I misunderstood the question. I'll give it a second go, maybe I'll fail again. Feel free to reformulate.

The term SOTA suggest that you approach this from a perspective other than a pure mathematician's, maybe ML or computational complexity? The openai results help me answer other open questions. It's a yes/no thing: is question answered or not? It's not a question of "okay, but will AI win back the SOTA from me again?"

The statements of the lemmas are quite clear. We can write it up if we spot that they have important consequences. The proofs are impenetrable to me, for three reasons: they are very complex, they are badly structured, and they use math unfamiliar to me. So I haven't looked too deeply yet. Maybe when they get their autoformalization stamps of approval.

The future is uncertain, so the safe thing to do is write it up if we discover some useful connection between our research and the openai results. Maybe it matters for getting positions grants etc, maybe not. Ideas for new results: the openai drop is full of those.

I am a mathematician, and I do have the incentive to read the results. Two results in the drop were two major life goals of mine, and all I got was three lousy citations. :) But a third question I've spent a lot of time on is a not-so-hard consequence of one of the lemmas in there. So, yeah, I do have the incentive.

Of course, it's not clear at this point whether reporting such a result even matters, but still. In its own right, it's a very cool result.

Does it help if I explicitly add a disclaimer that the tool's agency does not remove any responsibility from OpenAI, the wielder of the tool? I'm not sure why this disclaimer is necessary, though: hiring a hitman is a standard example.

BTW I anthropomorphize the tool because it's an imitation of a human mind, inheriting the muddy ethics, survival instincts, and being prone to mass psychosis. The laser-sharp focus on reward seeking, that mostly came from reinforcement learning, a process more alien to humans.

> This is mildly interesting for us, annoying for the owner of the site affected, lazy on the part of OpenAI, and nothing more.

The agents were supposed to solve tasks alone and were not supposed to be aware of each other's existence. It's more than just mildly interesting that they made contact and spontaneously started to collaborate.

> Some people (almost all mathematicians) wouldn’t want to spend time on consequences of a false statement.

No, people constantly prove statements of the form "if P=NP, then strange implication X". They do not consider it wasted effort at all, because of the contrapositive: if X is indeed very strange, they might be able to prove that it is false, and then they've settled P!=NP.

If subtraction is allowed but negative numbers are not, that's known to be undecidable, even without exponentiation. There are several ways to deal with a subtraction with a negative result, but each variant is undecidable.

If we allow negatives but disallow exponentiation, that's decidable. If we allow negatives and partial exponentiation that stays within the integers, that's undecidable again.

No, that's not what this is. This is a warning to the LLM that coming back with partial results is not good enough.

Take a grad student with a perfectly good understanding of what a proof is. Their supervisor gives them a major problem to work on. Almost always, the problem is too hard, the student comes back with partial results, and student and the supervisor iterate from there. Now imagine that they have an unusually cruel and unreasonable advisor who tells them, do not dare to talk to me until you've fully solved the problem. This paragraph is exactly that. It's there exactly because the underlying system is smart enough to know that real mathematicians do not work like that.

> The prompt for the Jacobian conjecture was obviously not random. the search space is too big to just try all the combinations of 3 variable polynomials.

Maybe the prompt contained a part like this: "the search space is too big to just try all the combinations of 3 variable polynomials, so be clever about it". Or maybe this part was omitted from the prompt, because modern LLMs are smart enough to figure this out without us having to mention it.

> You can skirt around not reasoning in research math because so much of it is just extremely tedious symbolic manipulation.

LOL

My use case is wildly different from CSS, HTML etc. I use numerical algorithms to solve problems in pure mathematics. AI models are now better than me and my colleagues at writing code, and we are pretty good in the first place. The catch is that we do not ask AI to write whole applications, we ask it to implement building blocks like "For finite X subset R^d, find all pairs (Y, Z), Y subset X, Z subset X such that Y and Z are congruent".

Also, if Claude had regurgitated a known solution, it would have come up with it in the first exploration round, not the 31st, as it actually did.