What was already known
Mirtabatabaei and Bullo proposed graph stabilization and eventual pseudostability in these models. Their main conjecture that every trajectory converges remains open.
AI involvement
The three authors credit Claude Opus 5.5 with finding the examples after their prompts. They wrote the explanations and checked every example by hand; JD Jones directed the later Lean formalization.
The authors explicitly credit Claude Opus 5.5 with finding the retained counterexamples after their prompts.
Importance
The examples overturn two conjectures and one theorem about heterogeneous opinion dynamics.
Limitations
The later Lean work also contains smaller examples and extensions, which are separate from these four paper examples.
Technical verification
The paper authors report checking all four examples by hand, and the cited Lean development reports complete proofs of their closed forms, neighborhood tables and refutations. These are two documented checks of the same paper examples; the later repository’s extra systems are outside this assessment.
Formal checking
Hand verification of the examples and written proofs
- Checker
- Hegarty, Ognissanti and Wedin
- Scope
- The explicit SBC and SBI counterexample trajectories in §§2–5
- Basis
- Reported by the linked checker
Formal checking
Lean proof build and axiom audit
- Checker
- Lean 4 kernel in JD Jones’s reported build
- Scope
- Closed forms, neighborhoods, convergence and refutations for the four paper systems
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The human authors explain the explicit trajectories, alternating modes, and why these defeat the earlier claims. Their prose and hand check cover the central mechanism of the assessed examples.
Correction and publication history
The examples overturn two conjectures and one theorem about heterogeneous opinion dynamics.
Read this published revision