cs.AIFeb 21, 2026

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

Authors: Brecht Verbeken, Brando Vagenende, Marie-Anne Guerry, Andres Algaba, Vincent Ginis

Organizations: Data Analytics Lab, Vrije Universiteit Brussel, Pleinlaan 5, 1050 Brussel, Belgium · imec-SMIT, Vrije Universiteit Brussel, Pleinlaan 9, 1050 Brussels, Belgium · School of Engineering and Applied Sciences, Harvard University, Cambridge, Massachusetts 02138, USA

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.

Explore similar work

CardsList
  1. LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

    Feb 27, 2026Antoine Peyronnet, Fabian Gloeckle, Amaury HayatMathematical Reasoning BenchmarksAutomated Theorem Proving

  2. Evaluation of LLMs for Mathematical Formalization in Lean

    Jun 4, 2026Tyson Klingner, Drew Bladek, Escher Crawford +6LLM EvaluationLean Theorem Proving

  3. Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs

    Jun 13, 2026Jierui Zhang, Siyuan Tan, Xinhang Li +8Mathematical Reasoning BenchmarksLLM Evaluation