Don Knuth's "Claude-like" directed Hamiltonian cycles decompositions

32 points by Nezteb

I apologize for the mouthful of a title in advance. "Claude Cycles" was a bit concise for my taste.

Filip told me that the explorations reported above, though ultimately successful, weren’t really smooth. He had to do some restarts when Claude stopped on random errors; then some of the previous search results were lost. After every two or three test programs were run, he had to remind Claude again and again that it was supposed to document its progress carefully.

smlckz

Theorem. A Claude-like decomposition is valid for all odd m > 1 if and only if each of the three sequences that it defines for m = 3 is generalizable.

[...]

All in all, however, this was definitely an impressive success story. I think Claude Shannon’s spirit is probably proud to know that his name is now being associated with such advances. Hats off to Claude!

.....

Don't tell me, now we will have math stuff named after LLMs? That things have progressed so far, even a giant like Knuth is impressed?

gspr

I'm far over on the LLM-skeptic side of things, and I won't have them generate code or natural language for me at all.

But the beauty of math is that a theorem is a theorem no matter how it ended up in our hands. If LLMs synthesize theorems that help advance math, then that is (1) good and (2) impressive. Once the proof has been verified, either by a human or partially automatically in a theorem prover, we have new knowledge that is independent of its origins. Cool!

I'm still very surprised that LLMs that work in natural language are suited for this task – one would think that generating sequences of symbols in a language where you can only formulate logically consistent statements would make more sense. But hey.
- bakkot
  
  Note that the proof here was all human - Claude wrote a piece of code which empirically worked on the cases they tried it for, and then Knuth looked at Claude's reasoning and what it was doing and proved it works in general.
  
  (There are other examples of LLMs writing correct proofs, but that wasn't even attempted here from what I can tell.)
- lygaret
  
  one would think that generating sequences of symbols in a language where you can only formulate logically consistent statements would make more sense. But hey.
  
  With all due respect, I disagree with this one -
  
  I think the ability to formulate statements that don't have to conform to any yet-to-be-given rules gives a lot of freedom to explore a space -- the final result will need to be logically consistent, but allowing exploration to say "so, let's just pretend this is actually a thing and see where that takes us" seems like an important part of how LLMs are able to work things out.
  - gspr
    
    You misunderstand me. What you suggest is very much possible within the constraints of being logically consistent. "Given these unproven assumptions, would be it be true that..." does not at all set you up for logical inconsistency.
    
    I do not suggest we should eradicate hypotheticals. I'm saying it's (to my intuition) silly to be working in languages where "given that it's yellow's 7, can cats marry under the great funny?" is a perfectly fine phrase as far as the language is concerned.