Yes, it seems indeed the models even obtained the results on the same day. I haven't had a chance to look through the OAI claimed proof yet, but in the spirit of the AGMAI recommendations to improve exposition before release, some of us did read Claude's proof last week before release to try to incorporate a better quality high level overview and exposition overall, which I hope is reflected in the pdf (published via the AI repository Hexagon, see hexagonmath.org/2610.00577; lean available at github.com/anthropics/formal…; also see the google drive shared via @rrwilliams's post drive.google.com/drive/u/0/f… in preparation for the upcoming workshops he's organizing with Impagliazzo and Paturi). Sharing what I understood from the proof below: Basic idea (below is for runtime 2^{delta n} for arbitrary constant delta>0; it seems both proofs ultimately get roughly exp(O(n / sqrt(log n))) time with lower order terms in the exponent), * can assume num clauses = O(n) wlog via previous sparsification results (n = num variables) * Solve #3-SAT not 3-SAT (i.e. count satisfying assignments, don't just decide satisfiability) * Convert to graph problem: clauses are nodes, and edges between clauses that share a variable (whether it's x or not(x) doesn't matter; we care about same variable, not same literal). Weight of an edge is # of shared variables. * Divide and Conquer idea: if there's a cut with total weight W, you can iterate over all 2^W fixings of those shared variables, and for each fixing you recurse on both sides and multiply, then add it up. Base case is constant # vertices, then you can just brute force count in 2^O(1) time. Unfortunately, you're not going to always find such a cut. (aside: from now on you can imagine every occurrence of a literal gets its own variable, and edges are functions enforcing equality constraints between those copies) * Instead of the above D&C, group the vertices into g^2 groups for some large constant g = g(delta). It matters how to do this grouping (it's not arbitrary); without getting into the details (see paper), a random grouping has properties the D&C wants (probabilistic method), and this existence is enough to allow for a slow-but-fast-enough algorithm to find a good grouping deterministically. * Imagine laying out the g^2 vertices arbitrarily on a g x g grid. Some edges are "side edges" (purely horizontal or purely vertical) and some are "diagonal" (the rest). There are (g choose 2)^2 = Theta(g^4) diagonal ones (choose two rows and two columns to define the corners) but only 2*g*(g choose 2) = O(g^3) side edges. You can pick g a large enough constant that the side edges have much less total weight than the diagonals -- the D&C will save on the diagonals, so we want there to be many more of them. * The sum we want is sum_z prod_{vertices a} W_a(z_a) * prod_{edges a,b} P(z_a,z_b), where W_a(z_a) at the highest level of recursion is a table of 2^3=8 values for each of the settings of the 3 literals in clause a, with value 0 or 1 indicating whether z_a satisfies clause a or not, and P() is the equality constraint checker I mentioned on the edges (deeper levels of recursion also all involve sums of this form where P() is always an equality checker on some set of bits, but deeper W's have arbitrary integer outputs and not necessarily 0/1) Write prod_{edges} P(..) = prod_{side edges} P(..) prod_{rectangles r} P_1(..) P_2(..) where P_1, P_2 are the diagonals for the rectangle r *The key step* (eqn 15 in the pdf): first assume all edges in the entire graph have exactly 3 bits on them (it turns out reducing to this isn't *too* complicated; see (19)), and replace P_1*P_2 with a hyperedge that involves some function on the corners of the rectangle, times a sum of two products of edge functions. This replacement comes from something called the "eight square identity"; this is related to octonions, which I still know nothing about. :) So P_1*P_2 = HyperEdgeFunction(corners)*(Q_1*Q_2 + Q_3*Q_4) Two interesting things here: (1) Q_1,Q_2,Q_3,Q_4 are all side edges (Q_1,Q_2 are horizontal and Q_3,Q_4 are vertical), and (2) whereas P1,P2 have total weight 6 (3 and 3), if you merge each row of the grid into a supervertex then Q_1,Q_2 vanishes and the hyperedge becomes a regular edge with total weight 3 whereas hyperedge*Q_3*Q_4 still involves 6 bits (and vice versa if you merge each column into a supervertex). In particular, the average weight from using Q_1*Q_2 vs. Q_3*Q_4 is (3+6)/2 = 4.5. We went from weight 6 (P_1*P_2) to weight 4.5 "on average". * So back to the original sum, we can rewrite it: sum_a W_a(z_a) * prod_{side edges} P(..) * prod_{rectangles r} hyperedge(r) * (Q_1*Q_2 + Q_3*Q_4) Now imagine distributing that product over that final sum involving the Q's, to get a new sum that has a factor 2^{# rectangles} more terms multiplicatively. (but there are only poly(g) = O(1) rectangles, so this is only a 2^{poly(g)} = O(1) blowup in the number of summands) * Each one of these terms in the new, bigger sum, has a prod_rectangles in it. Either >=1/2 of the rectangles chose the Q_1*Q_2 when we distributed the product, or >=1/2 chose the Q_3*Q_4. That means we can either merge all row edges or merge all column edges, and one of those wil decrease the total number of weights on edges by a 4.5/6 factor. This is the heart of why D&C makes progress; D&C is supposed to reduce one instance to simpler instances, and "simpler" in this case means decreasing the total weight on all edges (here by a 4.5/6 factor). This overall looks like a recursion with branching factor 2^{poly(g)} = O(1), but in reality the branching factor becomes poly(m) when you account for the trick in the proof to reduce to the case of 3 bits on each edge. In any case, there are more steps to get everything to work, but the above gives some taste of how the Divide & Conquer works. If you optimize the right way to choose g to not be a constant but a slow enough growing function, you get runtime exp(O(n / log^c n)), but for a tiny c. If you replace the eight square identity with something fancier, and replace the black-box invocation of the sparsification lemma with a more white box version that adds in some more ideas, you get down to the exp(O(n loglog n / sqrt(log n))) in the paper.