Wonder is what appears when art and science refuse to stay apart. I work in that seam: where a proof starts to feel like a picture, and a picture starts to behave like a law. Patterns that listen back. Structures that react. Atmospheres that feel almost alive. Not one illustrating the other. The two held as one material, and wonder is what comes through.
The Discrete Jacobian asks whether a rewrite that can be uniquely undone from local data must still be injective on whole graphs. It does not. A rule can keep every vertex and every edge, admit a unique local undo, and still erase which match produced the result.
Two non-isomorphic sources can share one successor class. The image forgets which vertex carried the loop. That collision is Lean-checked.
A later result separates two kinds of reversibility. On a two-vertex sector, at most one past class can still carry two complete causal histories. The cores are machine-checked. The newest theorem is a working draft, not peer reviewed.
The Zarankiewicz problem asks for the maximum number of edges in a bipartite graph with equal parts that still avoids a complete bipartite subgraph of a given size. For small orders those maxima are exact integers, and they belong on the public encyclopedia of integer sequences, not in a private notebook.
In 2026 I published new exact values there: the order-11 and order-12 terms of one classical sequence, and the order-12 term of its companion. Those are finished numbers, not estimates.
For the next open case the search splits into independent cells. Each cell is a propositional encoding. A SAT-class solver either finds a forbidden drawing or produces a machine-checkable proof that none exists. A second program, a resolution-proof checker, has to accept that proof before the cell counts.
