The site has been quiet. The workspaces have been busy.
Much of the recent work has been taking results apart: finding a graph that realizes a bound, checking what a formal theorem actually assumes, or handing a classifier that looks perfect an example that should make it fail. Some of those checks produced results worth keeping. Others changed the question.
This is a snapshot as of October 18. I directed the work with substantial AI assistance, mostly from OpenAI Codex, which wrote code, proofs, experiments, and drafts. Each project’s records say who did what and how it was checked.
Small graphs, complete families
A graph is C6-saturated if it contains no cycle of length six, but adding any missing edge creates one. How few edges can such a graph have?
The latest saturation release gives exact values through 15 vertices and complete minimum families through 14. There are 205 different minimum graphs on 14 vertices, counting graphs that differ only by vertex names as the same graph. On 15 vertices the minimum is 20 edges; the complete family there is not yet classified.
The most satisfying piece is small enough to inspect directly: an 11-vertex, 14-edge graph contradicts a previously published value of 15. The archive includes a certificate that checks its saturation property without rerunning the large enumeration. The release also corrects my own earlier attribution of the order-9 and order-10 results, which were already known.
The full families raise a new question. At order 14, 113 minima have leaves and 92 have minimum degree two. Why two groups? The computation produced objects to study, not just an edge count.
Formal mathematics, one exact statement at a time
Prove2Me posts mathematical statements in Lean, a computer-checked proof language, for people to prove or disprove. By the end of a round of work on October 17, my total was 129 unique accepted targets: 126 proofs and three disproofs. That round added 67 proofs across 14 research projects, 16 of them a project’s main statement. The counts include supporting lemmas and formalizations of existing, credited mathematics; they are not counts of discoveries.
The October 18 work added a counterexample to the platform’s version of a Fisher-market welfare theorem: an allocation that is Pareto optimal but lacks the equilibrium support the statement requires. Suspecting a gap in a proof was not enough; the full negation had to be proved.
The Prove2Me profile links the platform contributions. The broader exact-certificate work continues too: graph-flow classifications, probability calculations, and finite obstructions whose claims can be checked without rerunning the original search.
A perfect classifier and an uncomfortable control
CMRI is my project on measuring how a conversation develops. One pilot asked whether an assistant revises a stated commitment, and whether it later uses that commitment.
A text classifier reached 100% balanced accuracy on the original synthetic revision probe. Then a controlled intervention made the initial and final commitments identical. The classifier still predicted a change in all 80 cases. The response templates gave the answer away without any comparison of commitments.
The experiment also compared text sequences with geometric summaries of embeddings. For later use of a commitment, the simple sequence baseline beat the other reported instruments. So the next study first validates the events themselves, with independent judgments.
Another CMRI result held up. Broader conversation history predicted the next user’s embedding better than the last two messages alone. An apparent difference between the benefit of user and assistant history depended on what each predictor could see. Something is there, but it needs a more precise reading.
Elsewhere in the workspace
My OEIS portfolio now lists 17 published sequences; pending proposals are tracked separately. A privacy study looks at what repeated queries for absent keys reveal about the values in a compact retrieval structure. Astronomy pilots have recovered known stellar systems and the transits of pi Mensae c from public data; the new-target work is still in progress.
Each deserves its own post. I’ll start with the graphs, where you can draw the object, follow one check, and see why proving a minimum takes a much larger argument.
Discussion