This isn’t so much a math post, as it is an AI post, describing an experiment / sidequest. Over on the CT zulip Mike Shulman wrote the following:
On a slightly different topic, I was struck by the fact that at CT26 approximately zero of the talks I attended mentioned any use of AI. I don't have any experience yet myself actually using AI for category theory, since basically all I've been doing myself since it got good at math is coding. But I mentioned this to some non-category-theorist mathematician friends and they were also very surprised; one of them said that he just submitted a paper in which all the proofs were done by AI. Is there some reason that AI is less useful for category theory than for other branches of math? (I must admit that would please me, but it seems like wishful thinking.) Or are category theorists living in the past, either out of ignorance or by choice?
I made some reply breaking down a distinction between AI being useful for computational work and being much shakier for theoretical work — of course we all know about the recent resolution of the Jacobian conjecture, and a lot of the successes have been counterexamples to things. I had just come off using an LLM to compute some d-Segality of spheres which involved quite a bit of computation, and earlier this year I was having an LLM generate code for enumeration of partial groups. I do ask theoretical questions, but it’s mostly for help understanding things I’m reading, and it’s been really hit-or-miss. But I hadn’t really done that recently, models change all the time!
A theorem of Bergner, Osorno, Ozornova, Rovelli, and Scheimbauer (BOORS) states that a simplicial object $X$ is 2-Segal if and only if its edgewise subdivision $\sd X$ is Segal. I’ve wondered for a while if something similar was true for $d$-Segal spaces for $d>2$, but never quite got up the motivation to fully investigate it. The $d=2$ case came up in Paula Verdugo’s talk at DV60 and when talking to her and Julie Bergner afterwards I said I thought it was really unlikely that there were any extensions to $d > 2$. I think I was not optimistic because I had tried to look into it a little bit at some point.
Anyway, this leads me to the experiment: I now had a bunch of new, simple examples of d-Segality (the spheres), and figured it was worth hitting them against the problem to see if it failed. The actual question:
Is there a version of the edgewise subdivision criterion that is true for d-Segal spaces for d > 2?My instinct is that if anything like this were to be true it would be for 2k-Segal spaces, since edgewise subdivision contains in a sense both upper and lower décalage, and the path space criterion already relates upper or lower 2k-Segality to lower (2k-1)-Segality of these décalages.
(But it also may just be false for d > 2, who knows!)
A bit about the setup: I worked on this using Claude Code, using the Opus 5 model (at medium effort). I provided a few (tex) fragments of things that I’d written, including the full version of my paper the decomposition space perspective where I gave a different proof of the BOORS result.
There were four prompts total (see transcript):
- “Read instr.md and let me know if you have any questions” – the mentioned instructions file first described the various inputs, and then included the question above.
- Claude came back with a precise version of the question and asked me several questions. This prompt was mostly me responding to those questions.
- “Please commit them. Then try out the retract lemma in the way you think best.” — Claude had written some scripts, and sketched the forward direction of the results, and indicated what it wanted to try (retract lemma) for the backwards direction.
- “sure let’s do that” — Claude had proved the backwards direction and had said “Next most useful thing, if you want it: write the pasting induction out in full LaTeX in your
from_coskelconventions — at which point (A) and (B) are a short paper-section, since the two lemmas are each about a page.”
At this point I was committed, and sat down with pen-and-paper and worked through the argument (roughly 5 pages). It’s very good. Not perfect, but correct and clean. So here’s a couple new theorems, with $k \geq 1$ and $X$ a simplicial object:
Theorem 1: $X$ is $2k$-Segal if and only if $\sd X$ is lower $(2k{-}1)$-Segal.
Theorem 2: $X$ is upper $(2k{+}1)$-Segal if and only if $\sd X$ is upper $2k$-Segal.
For me these feel right and good — Theorem 1 is the evident generalization of the BOORS result (the $k=1$ case), the exact analogue one might hope for (given Poguntke’s path space criterion). Theorem 2 at first looked strange to me, since it included an “upper $2k$-Segal” bit, but it really is the right thing based on what the edgewise subdivision sees. Even the $k=1$ case of Theorem 2 is new. (Notice there is no characterization of lower odd Segal here. This is not unexpected: it mirrors what happens with the path space criterion, and basically occurs since that is the most essential of the higher Segal conditions, and is where the dimensions of the cubes under consideration change.)
I’ll speculate that this experiment may have been helped along by two things. First, my proof of the BOORS result explicitly relies on the relationship between edgewise subdivision and décalage, and is able to leverage the path space criterion; Claude generalized this proof and was able to do the same. Second, it used the perspective on higher Segal conditions that Justin and I developed following Tashi Walde’s approach based on cartesian cubes. This makes everything extremely uniform, and allows one to argue similarly no matter what $k$ is. It’s possible that there’s a nice proof based on triangulations of cyclic polytopes, but I’m not going looking for it.
I’m also guessing that reading it was pleasant for me since the input was literally things I’ve written, all from a perspective that I like and think is powerful.
I’m still left with the question of what to do with this. As I wrote on Zulip “It’d probably have been a paper I’d read if someone else wrote it, or a little paper I’d have felt good about if I figured it out and wrote it myself.” The theorems are cute, interesting, and not so hard. But each day there’s new 100+ page AI-assisted stuff being posted on arxiv, and it’s extremely off-putting and miserable. And “what to do with this” isn’t just about the artifacts (two new theorems + proofs), but also how to process how I feel about all of this: I felt very hollow after finishing working through the Opus-written proofs. I guess we’re all feeling a lot of confusion right now.
Here is the documentation from the experiment: Claude Code transcript, GitHub repository, and a release featuring the initial PDF produced.