Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking)
ai-assisted-maththeorem-provingllm-copilotvibe-provinghuman-in-the-loop
Abstraction: LLM-assisted iterative mathematical proof via generate-referee-repair pipeline
Key points:
- Introduces "vibe-proving": iterative pipeline of generate, referee, and repair using a consumer-subscription LLM to collaboratively construct mathematical proofs
- Case study resolves Conjecture 20 of Ran and Teng (2024) on exact nonreal spectral region of a 4-cycle row-stochastic nonneg-matrix family
- Used ChatGPT-5.2 (Thinking); analyzed 7 shareable threads and 4 versioned proof drafts
- LLM is most useful for high-level proof search and idea generation; human experts remain essential for correctness-critical closure
- Verification bottlenecks persist: the model cannot reliably certify its own proofs are correct
- Provides process-level characterization with implications for evaluating AI-assisted research and designing human-in-the-loop theorem-proving systems
Connections: Chatgpt · Openai · AI Assisted Proof · Human In The Loop · Large Language Models
Source: https://arxiv.org/abs/2602.18918