Cognition's Devin generated proofs and counterexamples for four graph conjectures
Cognition builder Jared Zoneraich ran roughly five Ultra-mode agents per problem, with one counterexample checked in Lean.
By Ryan Merket · Published
Primary source: X - Jared Zoneraich
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.…
When you purchase through links in our articles, we may earn a small commission. This doesn’t affect our editorial independence.