Donald Knuth’s “Claude’s Cycles” paper shook the math world earlier this month. Now the follow-up work is getting even more interesting.
As reported on Hacker News, researchers and independent contributors are building on Knuth’s original result with formal proof assistants and multi-AI collaboration, pushing the boundaries of what human-AI teamwork can accomplish in rigorous mathematics.
Quick Recap: What Started This
In early March 2026, the legendary computer scientist published a paper titled “Claude’s Cycles” describing how Anthropic’s Claude Opus 4.6 solved an open graph theory problem he’d been stuck on for weeks. The problem: decompose all edges of a directed graph with m³ vertices into exactly three Hamiltonian cycles for odd values of m.
Claude cracked it in about an hour across 31 guided explorations, with Filip Stappers steering the AI’s attention throughout. Knuth then wrote the rigorous mathematical proof himself. The AI found the pattern. The human verified it was correct.
Knuth opened his paper with “Shock! Shock!” and admitted he’d need to “revise my opinions about generative AI.”
What’s New: Formal Verification and Multi-AI Proofs
The latest developments move beyond discovery into verification, and that’s where things get technically significant.
Lean 4 Formalization. Mikito Iwamasa took Knuth’s paper proof and formalized the entire result in Lean 4, a proof assistant that checks every logical step mechanically. The final development:
- 3,389 lines of code
- ~110 theorems and lemmas
- Zero remaining
sorrystatements (Lean’s marker for unfinished proofs) - Full verification via the Lean engine
AI played a supporting role here too, but not as an “end-to-end prover.” It generated proof scaffolding, suggested local lemma repairs, and produced strategy documents. Blindly asking the AI for “the rest of the proof” didn’t work. What did work: structured collaboration where the human architect directed the AI assistant.
Multi-AI Collaboration. An anonymous correspondent found a separate proof by pasting text back and forth between GPT 5.4 (Extended Thinking) and Claude 4.6 Sonnet (Thinking). Two different AI models, each picking up where the other got stuck.
The Even Case Remains Open
Knuth’s original result (and Claude’s discovery) covers odd values of m. The even case is still unsolved. When pushed toward even-m graphs, Claude made no meaningful progress. The odd-dimension solution is clean and elegant. The even case likely requires fundamentally different techniques.
This is a useful reminder: AI found one of 760 valid constructions for the odd case. It didn’t solve the full problem space.
Why This Matters for Practitioners
Three practical takeaways from this evolving story:
- AI discovery needs human verification. Claude found the construction. Knuth proved it. Iwamasa formalized it in Lean. The chain of trust runs through multiple layers, and each layer matters.
- Proof assistants + AI is a powerful combo. Lean 4 with AI-generated scaffolding let a non-mathematician contribute to formal mathematical verification. That’s a meaningful expansion of who can participate in rigorous math.
- Multi-model collaboration works. Using GPT and Claude together, each compensating for the other’s weaknesses, produced results neither achieved alone. Worth experimenting with for hard technical problems.
The Bigger Picture
What started as one AI solving one problem for one legendary mathematician has become a case study in collaborative intelligence. Humans steering AI discovery. Proof assistants checking AI-assisted proofs. Multiple AI models tag-teaming hard problems.
Knuth’s original paper got 635,000 views and 6,000 likes within hours. The follow-up work is quieter but arguably more important. It’s one thing for an AI to find an answer. It’s another to build the infrastructure of trust that lets mathematics accept it.
More details on the ongoing discussion are available on the original Hacker News thread.