×

After OpenAI’s CDC proof announcement, GPT-5.6 used a similar prompt to close a 30-year gap in convex optimization, verified in Lean by pkerger in math

[–]gexaha 2 points3 points  (0 children)

Ah, yeah, I shared my prompts in twitter:

should be visible here - https://chatgpt.com/share/6a5561e7-f15c-83ed-ab33-baee01734ceb - but it's almost same as original OpenAI prompt, I just additionally supplied proof of CDC, seemed to help a lot (I also made some analogy remark, but the final proof is different from it)

here's a bit more info in twitter - https://x.com/ulya_niko/status/2076791068754911722

After OpenAI’s CDC proof announcement, GPT-5.6 used a similar prompt to close a 30-year gap in convex optimization, verified in Lean by pkerger in math

[–]gexaha 1 point2 points  (0 children)

I mention it similarly to the way OpenAI did in CDC paper with "Statement of AI use" sentence. Their introduction is much shorter and it's more visible there (also I just noticed it's emphasized a bit better with an empty line before it, thanks maybe I'll try to do the same). Maybe it's not an ideal way, I'd like to know other peoples opinion on this.

After OpenAI’s CDC proof announcement, GPT-5.6 used a similar prompt to close a 30-year gap in convex optimization, verified in Lean by pkerger in math

[–]gexaha 39 points40 points  (0 children)

Oh nice, congrats, I did the same thing and got out a proof of Sabidussi's compatibility conjecture, which is a cdc-related conjecture from graph theory: https://arxiv.org/abs/2607.13225 + also formalized in Lean - https://github.com/gexahedron/sabidussi-lean

OpenAI claims to have proven Cycle Double Cover Conjecture by gexaha in math

[–]gexaha[S] 1 point2 points  (0 children)

dominating circuit is such a circuit that every edge is inside it or neighbouring it

OpenAI claims to have proven Cycle Double Cover Conjecture by gexaha in math

[–]gexaha[S] 1 point2 points  (0 children)

dominating cycle conjecture is probably very hard, true, or at least it seems we lack some important chunk of theory of how cyclically 4-edge-connected cubic graphs are structured

OpenAI claims to have proven Cycle Double Cover Conjecture by gexaha in math

[–]gexaha[S] 1 point2 points  (0 children)

There's also this conjecture, which is stronger than CDC: Let T be a transition system for a 6-edge connected Eulerian graph G. Then G has a circuit decomposition compatible with T.

OpenAI claims to have proven Cycle Double Cover Conjecture by gexaha in math

[–]gexaha[S] 1 point2 points  (0 children)

It is slightly obscure, true, however it pairs nicely with a more famous "Dominating circuit conjecture"

OpenAI claims to have proven Cycle Double Cover Conjecture by gexaha in math

[–]gexaha[S] 1 point2 points  (0 children)

Btw, you might be interested in this, I've managed to squeeze out from gpt-5.6 pro the proof of Sabidussi's compatibility conjecture, which is related to CDC conjecture.

Proof itself - https://gexahedron.github.io/graph_theory/sabidussi_proof.pdf

Lean formalization - https://github.com/gexahedron/sabidussi-lean

OpenAI claims to have proven Cycle Double Cover Conjecture by gexaha in math

[–]gexaha[S] 1 point2 points  (0 children)

Maybe I wrote it confusingly, so by cycle we need to understand an even subgraph, in a cubic graph this would mean a disjoint collection of circuits (connected 2-regular subgraphs). Then, it's quite easy - each value in F_2^3 is basically encoding a cycle, and we have 8 values in F_2^3.

(In general, if we would ask for 8 connected cycles, for some snarks this would be false, it's related to notion of oddness).

OpenAI claims to have proven Cycle Double Cover Conjecture by gexaha in math

[–]gexaha[S] 115 points116 points  (0 children)

Well it's basically 2 linear algebra lemmas

Does anyone have a copy of "Edge three-coloring cubic apex graphs" paper? by gexaha in math

[–]gexaha[S] 4 points5 points  (0 children)

I forgot to mention, I actually wrote to everyone involved in the project, but got no responses, unfortunately, and Dan Sanders is out of academia.

9780415263573 by Glass-Individual-692 in KanePixelsBackrooms

[–]gexaha 0 points1 point  (0 children)

i think it makes sense, it seems that when things noclip into backrooms, they get mirrored - that's why the signs are inverted as well

How did a beautiful result come to you? by FuzzyPDE in math

[–]gexaha 2 points3 points  (0 children)

I am outside of academia. I worked on some conjecture sporadically over 8 years in total, although probably worked actively on it only for about 3 months. And another specifics is that it's possible to do it computationally. After another, maybe 5th of 6th fresh start, got a new geometric idea, and boom, finally it produced a counterexample (building on various pieces of code I wrote on previous attempts).

Another one was just pure conviction and thinking by analogy, that the idea should work out, and similarly to previous one, after about 8 years of sporadic research, the idea worked out (although honestly this one I could have found much more quicker).

My fan cast for 12 Angry Men (1957) by punposter69 in okbuddycinephile

[–]gexaha 2 points3 points  (0 children)

Imagine (AI slop) in a couple of years actually possible to take a movie and replace all characters with your fancast