Vibe-mathing: the Generalized Vanishing Conjecture

A developer known as 'vibe-mathing' used AI-assisted exploration to investigate the Jacobian Conjecture, leading to the Generalized Vanishing Conjecture, which holds for every constant-coefficient differential operator in one or two variables but fails from dimension three onward. The experiment, sparked by a counterexample posted by Levent, demonstrates that AI can help locate exact boundaries and counterexamples in mathematics, though proofs still require human scrutiny.

I am a developer . Right now it is difficult to ignore the argument around “ vibe coding .” People who could not have written an application in the traditional way are describing what they want to an AI, running the result, reporting what broke, and iterating. Some of the resulting software is fragile . Some of it is surprisingly capable. Either way, the phenomenon is real . The uncomfortable part for experienced developers is not only that code is being generated. It is that the people producing it do not necessarily read or understand every line of code. They generate tests and just look at the result. Vibe-coders sometimes even seem to have a major advantage . Their unwillingness or unability to read the code makes it possible to work with several agents in parallel, producing incredible speedups. However, I am not going to settle the questions of viability or quality of vibe-coded software here… I’m too invested. Instead, I decided to take that instinct somewhere else: to vibe my way into a field about which I had very limited knowledge, not burdened by knowledge, deep understanding, or preconceptions : As a developer, I have spent a lot of time using tools like Codex, refining prompts, and running parallel experiments. Also, large software systems have always exceeded the understanding of any one person . So abstractions and unknowns is part of what we do. We navigate them through interfaces, types, tests, logs, debuggers, reproducible builds, and carefully chosen experiments. None of these makes a program correct. Together, however, they let us ask much better questions than “does this code accomplish the goal s ?” I began to wonder whether something similar was possible in mathematics . Could I enter a field in which I did not have the expected training, use AI to navigate definitions and possible constructions, generate exact data, loop through failed ideas, and gradually replace intuition with artifacts that could be checked? Could I begin exploring before I understood the whole territory in the traditional order? Or, stated more provocatively : could I too vibe-math my way to a genuine mathematical frontier? The real spark here was Levent posting the JC 3 counterexample https://x.com/ alpoge /status/2079028340955197566 . hello there the jacobian conjecture is false thanx to my close friend akhil for asking about it and my other close friend fable for working during the world cup final Suddenly there was a concrete mathematical object to inspect: a three-variable construction connected to the Jacobian Conjecture , with a new algebraic structure that could be tested, generalized, formalized, and attacked from several directions. This was my starting point. Instead of just asking whether AI could “do a breakthrough”, or produce mathematics that looked plausible, I could ask whether an AI-assisted process could locate the exact boundary or a new counterexample. Counterexamples are especially useful here, they are easy to check and verify . Do the calculation, and done. Proofs require way more human feedback, analysis and scrutiny . The experiment was never supposed to be “can AI produce a paper that looks like mathematics?” We already know that it can. There is more than enough slob online. That is precisely the problem: A plausible-looking proof is now almost free, while the time needed to find the hidden gap still belongs to a human reader. The real question was: Can AI-assisted exploration turn this counterexample into a result that survives exact computation, independent implementations, formal proof, explicit statement boundaries, and eventually human mathematical review? The Generalized Vanishing Conjecture became one of my test cases, one of my goals. And the result is a sharp boundary: it holds for every constant-coefficient differential operator in one or two variables, and it fails from dimension three onward. This is the story of how Levent’s post became a theorem, a counterexample, and a collection of steps/receipts. The Generalized Vanishing Conjecture: The Two-Variable Theorem and the First Failing Dimension https://zenodo.org/records/21782342 The counterexample and failure in every dimension at least three are fully Lean-verified; nearly all supporting algebraic machinery and much of the binary proof infrastructure are checked as well Repository source: papers/generalized-vanishing-two-variables/main.tex https://github.com/royvanrijn/jacobian-research/blob/main/papers/generalized-vanishing-two-variables/main.tex Lean proof: github.com/royvanrijn/jacobian-research/tree/main/formal/gvc https://github.com/royvanrijn/jacobian-research/tree/main/formal/gvc Lets start with the Generalized Vanishing Conjecture GVC : Let \ \Lambda\ be a constant-coefficient differential operator and let \ P\ be a polynomial. GVC asks whether \ \Lambda^m P^m =0\quad\text{for every }m\geq1\ forces \ \Lambda^m QP^m =0\quad\text{for all sufficiently large }m\ for every fixed polynomial multiplier \ Q\ . The statement grew out of work around the Vanishing Conjecture and the Jacobian Conjecture. But what made it especially interesting to me was its shape. The premise is an infinite sequence of exact identities, and the conclusion is eventual vanishing after inserting any fixed multiplier. This is exactly the kind of statement on which vibe-mathing can go wrong. A search can verify the first ten powers, or the first hundred, and still prove nothing about the next one. Perhaps we can explain why a visible pattern “should” continue and bury the missing quantifier inside a polished proof. My biggest rule became: A bounded search will not proof GVC. It does not mean bounded searches are useless, but it changed what I allowed them to mean. I began classifying low-degree cases in two variables . The calculations separated operator symbols by root type, exposed exceptional coefficient branches, and tracked which weighted faces could survive the first several pure identities. Again and again, the same patterns appeared. Surviving supports became one-sided. Moment ideals developed staircase-shaped radicals. A complicated coefficient system would collapse onto a face where a simple weighted degree deficit forced every mixed expression to vanish eventually. Degree by degree, exact calculations closed polynomial degrees four, five, six , and seven for arbitrary binary constant-coefficient operators. These were real theorems in their stated ranges. They were not a license to draw an all-degree curve through four data points. The attempted general proof grew into a much larger machine: Hall matchings, factorial packets, prime-power carries, characters, Graver bases, and finite traces. AI was useful here in the same way it is useful in an unfamiliar codebase. It could suggest representations, translate between formulations, generate experiments, and help turn a failed idea into a smaller exact question. Many pieces of that machine became valid mathematics. The machine as a whole did not close the conjecture. One promotion step kept moving away: I could understand a packet after it had been isolated, but I could not prove that the original infinite vanishing premise always exposed one fixed packet in the required way. This was an important part of the experiment. The repository accumulated more positive results without quietly changing the status of the missing step. The route was productive, but it remained incomplete. I kept telling Codex to “find general patterns, try to think about global structures at play here” . Sometimes I would have one thread list ideas, and spin up agent threads to experiment until they either reach an extension, elimination, or a dead end. Then the proof became shorter. Take the symbol of \ \Lambda\ and the support of \ P\ . For every positive weight \ w s= s,1 ,\ look at two faces: The pure vanishing identity passes to these extremal faces. Hall’s marriage theorem orders their horizontal Newton intervals just after ordinary degree. A separate prime-dilation argument shows that, while the two faces have unequal weights, their intervals cannot overlap. In two variables, this has a decisive consequence. The projection of each face is an interval on a line. Two disjoint intervals cannot exchange order without meeting. Now define the lower operator envelope \ L s \ and the upper polynomial envelope \ U s \ . Their gap \ \Delta s =U s -L s \ is piecewise linear because both supports are finite. Just after \ s=1\ , Hall localization puts the operator interval strictly to the right of the polynomial interval. Shifted-ray rigidity prevents the intervals from overlapping, so they cannot pass one another while \ \Delta s 0\ . The gap cannot stay positive forever. After the last breakpoint its slope is forced to be negative, so it must reach zero. At the first meeting, every operator monomial lies on or above one common weighted threshold and every polynomial monomial lies on or below it. A fixed multiplier contributes only a bounded defect; it cannot repair a deficit that grows linearly with the power \ m\ . That proves: Over a characteristic-zero field, every constant-coefficient differential operator in two variables satisfies the Generalized Vanishing Conjecture. The short proof also explains the staircase radicals from the earlier computer algebra. They were not mysterious survivors. They were finite shadows of a geometric fact: the moving Newton intervals were forbidden to overlap. Years of imagined mathematical labor had collapsed into following two piecewise-linear envelopes until they met. The binary theorem raised the obvious question: was two variables merely the first case of a higher-dimensional principle? It turns out: no Put \ \rho=t^2+xy,\qquad A=\rho+x^2,\ \ C=y\rho^2-2xt^2\rho-x^3t^2, \qquad P=AC^2,\ and let \ \Delta=4\partial x\partial y+\partial t^2, \qquad \Lambda=\Delta^6.\ Then, for every \ m\geq1\ , \ \Lambda^m P^m =0, \qquad \Lambda^m x^2P^m \ne0.\ The first identity supplies the complete pure premise. The second uses the single fixed multiplier \ Q=x^2\ and fails at every power, not merely infinitely often. This is a homogeneous counterexample in three variables. And once it fails in three variables , every larger dimension follows almost for free . Rename the three variables \ x 1,x 2,x 3\ and regard the same polynomial as one in \ ngeq4\ variables: \ \widetilde P x 1,\ldots,x n =P x 1,x 2,x 3 ,\ so \ \widetilde P\ is completely independent of \ x 4,\ldots,x n\ . Extend the three-variable quadratic operator by putting \ \widetilde\Delta n =4\partial {x 1}\partial {x 2}+\partial {x 3}^2 +\sum {i=4}^n\partial {x i}^2.\ For every polynomial \ f\ depending only on the first three variables, \ \widetilde\Delta n f =\left 4\partial {x 1}\partial {x 2}+\partial {x 3}^2\right f =\Delta 3f,\ because \ \partial {x i}f=0\qquad i\geq4 .\ Applying the same observation repeatedly gives \ \widetilde\Delta n^k f=\Delta 3^k f\ for every \ k\geq0\ . We can therefore take \ \Lambda n=\widetilde\Delta n^6.\ The pure identity is inherited verbatim: \ \Lambda n^m \widetilde P^m =\widetilde\Delta n^{6m} \widetilde P^m =\Delta 3^{6m} P^m =0.\ And for the same multiplier \ Q x 1,x 2,x 3 \ , the obstruction survives: \ \Lambda n^m Q\widetilde P^m =\Delta 3^{6m} QP^m \neq0.\ So the counterexample in three variables automatically produces one in every dimension \ n\geq3\ . Combined with the binary theorem, the exact dimensional classification is: \ \boxed{\operatorname{GVC} n \text{ holds if and only if }n\leq2.}\ The same boundary already holds when the differential operator is required to be homogeneous. In two variables , Newton faces project to intervals and inherit a total order. In three variables , higher-dimensional faces can move around one another. The mechanism that makes the binary proof work is precisely what disappears at the first failing dimension. Because we’re using AI here, we want to be extra careful and complete . One way to achieve this is formal verification in Lean, next to the Python, SymPy and Singluar scripts used in the discovery. The GVC public Lean development https://github.com/royvanrijn/jacobian-research/tree/main/formal/gvc is not a small certificate attached to the end of the project. It currently contains more than 3,100 lines across sixteen modules and 164 theorem or lemma declarations, with no sorry , admit , or explicit axiom declarations. We have now checked almost every part of the argument that can be cleanly isolated into an algebraic interface. Most importantly, the three-variable counterexample is formalized end to end . The development does not check a list of sample powers. It defines the literal polynomials \ \rho,A,C,P\ , the operator \ \Delta\ , its sixth power \ \Lambda\ , and the multiplier \ Q\ . It then proves the algebraic machinery connecting them: The resulting Lean theorem is unconditional : GVC fails over every characteristic-zero field in every finite dimension at least three That is the entire negative half of the dimensional classification, fully checked for all powers, fields, and finite dimensions in its stated scope. Nothing in the counterexample is left as an assumed computational bridge. The formalization goes considerably further . It checks the coefficientwise definition of GVC, operator composition, top contraction, the full endpoint coefficient ladder, formal beta evaluation, exact factorial valuations, Reynolds expansion, Laurent phase extraction, coefficient-ring base change, unused-variable padding, the winding–profile–radial degree formulas, and the final piecewise-linear envelope crossing used by the positive theorem. What remains outside Lean is concentrated: the global Hall-localization and shifted-ray separation bridge that drives the short binary proof, together with its no-reversal and common-threshold termination argument. Those steps are common and proved in the paper. Everything around that bridge has been reduced to explicit definitions, exact lemmas, or independent degree-four through degree-seven regressions. This combination matters to me. Exploration found the construction and the proof architecture. Exact computation kept killing false branches . Formalization then converted the entire negative half of the dimensional classification, and as much of the positive machinery as possible, into declarations that can be checked from definitions . The strongest version of “vibe-mathing” is not mathematics without understanding. It is mathematics in which understanding does not always have to arrive first. I could begin by navigating representations, generating examples, asking AI for possible bridges, and trying to falsify every bridge that appeared. Exact computation let me reject bad directions. Formalization forced vague claims to split into precise ones. Writing the proof forced me to explain why the surviving path worked. Most of my understanding followed the artifacts. It did not precede all of them. That changes what may be possible for people outside the normal research pipeline. It does not abolish expertise, and I would not say that it makes the work easier for them. It creates a new and confusing landscape and experience: people will begin exploring unfamiliar mathematics before they have the usual training, but they will probably also produce a great deal of low-quality material that needs to be filtered. AI may actually be very useful for a first pass, helping rate, sort, and identify which artifacts deserve closer human attention. But that is only a pre-check, not a substitute for expert judgment. The remaining human questions become: Those are exactly the questions on which I now want expert criticism. The GVC project forced the process in both directions at once: a general positive theorem in two variables and a concrete failure in three . Crossing between those modes was far harder than generating plausible candidates. It required a growing system of definitions, tests, exact certificates, failed searches, formal proofs, literature boundaries, and prose. I do not know yet how the mathematical community will judge the result. That judgment cannot be automated, sped up, made easier… As a software developer struggling with accepting vibe-coded codebases, I can imagine what mathematicians are going through right now. But the right response is the same, now we inspect the statement, run the checks, read the proof, and try to break it. The vibes helped find the path. Verification decided what survives, counterexamples are easy to verify, proofs are definitely not. There was one final twist . On the very same day, Christopher D. Long messaged me and reported https://x.com/octonion/status/2084445366972244168 that he had independently found two other proofs , using ideas unrelated to this one. We had reached the same conclusion from three different directions, without coordination. For a result about the exact boundary between truth and failure, that convergence felt especially remarkable. The formal development is pinned to Lean and Mathlib versions recorded in the repository. From the repository root, build the GVC verification with: make verify-gvc-lean