Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking)

TL;DR

This paper provides early evidence that consumer LLMs like ChatGPT-5.2 can assist in research-level mathematics, specifically in spectral region characterization, by supporting proof search and iterative refinement, though human oversight remains crucial.

Contribution

It demonstrates the practical use of a consumer LLM in a complex mathematical proof, highlighting its strengths in high-level proof search and identifying verification bottlenecks.

Findings

LLMs aid in high-level proof search and iterative refinement.

Human experts are essential for correctness-critical steps.

The study offers a process characterization of LLM assistance in research workflows.

Abstract

Large Language Models (LLMs) are increasingly used as scientific copilots, but evidence on their role in research-level mathematics remains limited, especially for workflows accessible to individual researchers. We present early evidence for vibe-proving with a consumer subscription LLM through an auditable case study that resolves Conjecture 20 of Ran and Teng (2024) on the exact nonreal spectral region of a 4-cycle row-stochastic nonnegative matrix family. We analyze seven shareable ChatGPT-5.2 (Thinking) threads and four versioned proof drafts, documenting an iterative pipeline of generate, referee, and repair. The model is most useful for high-level proof search, while human experts remain essential for correctness-critical closure. The final theorem provides necessary and sufficient region conditions and explicit boundary attainment constructions. Beyond the mathematical result, we contribute a process-level characterization of where LLM assistance materially helps and where verification bottlenecks persist, with implications for evaluation of AI-assisted research workflows and for designing human-in-the-loop theorem proving systems.