Cognition's Devin generated proofs and counterexamples for four graph conjectures

Why it matters

Zoneraich's experiment moves coding agents into mathematical research, where parallel search can generate candidates quickly but public proofs and expert review still determine validity.

Jared Zoneraich (@imjaredz), a Builder in Residence at Cognition, said on July 23rd that Devin produced proofs or counterexamples for four long-open graph theory conjectures across three assignments.

The results described in Zoneraich's thread cover Graffiti Conjectures 39, 40 and 154, along with Brandt's regular supergraph problem. Zoneraich said Devin proved Conjectures 39 and 40 and refuted the other two. The Graffiti problems had remained open for roughly 40 years, according to Zoneraich, while Brandt's problem had been listed for about 20 years.

The claims have not reached the point where mathematicians would treat the four problems as settled. Zoneraich's thread did not include a public repository, paper or independent expert review. It offered the most detail for Conjecture 154, including a proposed counterexample and a description of its formal verification. The posts provided less public evidence for the other three results.

That distinction matters because Zoneraich was testing Devin, Cognition's software engineering agent, as a parallel mathematical researcher. The experiment pushed Devin beyond its primary job of navigating codebases, writing software and submitting pull requests.

Five agents per problem

Zoneraich said he first assigned several Devin instances to search for suitable open problems resembling a separate result posted on X. He selected the strongest candidates and then launched about five Devin instances in Ultra mode for each problem, asking the agents to find and verify solutions.

The workflow resembles a research lab running several independent approaches at once. Agents can try different constructions, search references, test examples and challenge one another's output before a human chooses which line to pursue.

Cognition has been building that operating model directly into Devin. In March, Cognition released a feature that lets one Devin manage other Devin instances, breaking a larger task into pieces and delegating them to agents running in separate virtual machines.

Zoneraich joined Cognition this year after co-founding the AI development platform PromptLayer. In his announcement about joining Cognition, he described coding agents as the next step in a broader shift toward software creation through natural-language instructions. The graph theory test applies that thesis to research work where code, symbolic reasoning and literature search overlap.

The counterexample Devin found

For Graffiti Conjecture 154, Zoneraich said Devin constructed a graph by joining a 50-vertex clique to a path containing 70 edges, producing a graph with 120 vertices. The resulting graph allegedly violates the conjectured inequality.

According to Zoneraich, Devin reduced the violation to an integer inequality and formalized the argument in Lean, including the calculation of the graph's distance sum. That is stronger evidence than an unverified numerical search because Lean checks whether a proof follows from its formal definitions and assumptions.

Lean's own documentation on proof validation describes an important boundary. Kernel acceptance establishes that the formal theorem follows from the definitions, imported results and axioms encoded in the file. Reviewers must still confirm that the formal statement accurately represents the original informal conjecture and that the proof does not rely on incomplete or inappropriate assumptions.

The public thread does not provide enough material to perform those checks. A reproducible Lean project would let mathematicians inspect the graph construction, compare the encoded inequality with Conjecture 154's original wording and list the axioms used by the proof.

Zoneraich also said Devin refuted Brandt's regular supergraph problem. Douglas West's open-problems collection states the conjecture as a claim that every maximal triangle-free graph with minimum degree at least one-third of its vertex count has a regular supergraph obtainable through vertex multiplications. Zoneraich did not publish the claimed counterexample's construction in the text of the thread.

The same evidence gap applies to Graffiti Conjectures 39 and 40. Zoneraich labeled both proven without supplying their full statements or proofs in the posts.

Cognition originally presented Devin as an autonomous software engineer. Zoneraich's experiment shows how the same agent infrastructure can be aimed at problems that combine mathematical search with executable verification. The parallel run also illustrates the cost profile of this approach: several agents searched for candidates, followed by roughly five high-compute sessions for every selected problem.

The decisive test will be reproducibility. Public proof artifacts and review by graph theorists would turn Zoneraich's demonstration into a mathematical result. Until then, the thread documents a promising agent-assisted research workflow and four claims awaiting scrutiny.