Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro

• URL: http://arxiv.org/abs/2607.20525v1
• Date: Thu, 09 Jul 2026 23:28:37 GMT
• Title: Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro
• Abstract summary: We present a problem-agnostic, three-stage prompting pipeline built on GPT-5.5 Pro.<n>The agent autonomously generated correct proofs that the sum-product conjecture is false over $mathbb R$ in 7 of 8 independent trials.
• Score: 5.634825161148485
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: OpenAI's recent disproof of the Erdős unit distance conjecture marked a milestone for AI in mathematics. It also inspired another breakthrough: a human disproof of the Erdős--Szemerédi sum-product conjecture over $\mathbb R$. In this paper, we present a simple agent built on GPT-5.5 Pro. Using a problem-agnostic, three-stage prompting pipeline -- proof-plan proposal, proof construction, and review -- the agent autonomously generated correct proofs that the sum-product conjecture is false over $\mathbb R$ in 7 of 8 independent trials; in the remaining trial, it identified an unresolved gap in its argument. The seven proofs are diverse: some are close to existing unit-based constructions, while others avoid units by using $L^p$-type regions of algebraic integers. The system used an average of 132.4k reasoning tokens per trial. We release the code, intermediate outputs, and generated proofs, providing a reproducible, data-contamination-free case study in autonomous proof generation.

Related papers

• The Condition-Number Barrier in Sparse Least Squares [77.64108812086542]
  In [AS21], Axiotis and Sviridenko conjectured that the linear dependence on the restricted condition number in convex optimization cannot be improved by a sparse-time algorithm.<n>We establish their conjectured lower bound for least-squares objectives, conditional on the randomized exact-volume Small-Set Expansion Hypothesis.
  arXiv  Detail & Related papers  (2026-08-03T17:57:01Z)
• Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings [0.2538209532048866]
  We use Lean 4's kernel-level tracking of axiom dependence to show that the axiom of choice has a measurable geometric correlate in proof space.<n>We show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source.
  arXiv  Detail & Related papers  (2026-06-26T19:57:00Z)
• Mathematics with large language models as provers and verifiers [1.1029146548022293]
  ChatGPT solves five out of six IMO problems, and close about a third of the sixty-six number theory conjectures in [Cohen, Journal of Sequences, 2025].
  arXiv  Detail & Related papers  (2025-10-11T20:35:25Z)
• Gödel Test: Can Large Language Models Solve Easy Conjectures? [40.906606632144694]
  We propose the G"odel Test: evaluating whether a model can produce correct proofs for very simple, previously unsolved conjectures.<n>We study the performance of GPT-5 on five conjectures in algorithm optimization.<n>GPT-5 may represent an early step toward frontier models eventually passing the G"odel Test.
  arXiv  Detail & Related papers  (2025-09-22T20:11:40Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thought prompting has become the de facto method to elicit reasoning capabilities from large language models (LLMs)<n>To mitigate hallucinations in CoT that are notoriously difficult to detect, current methods operate as opaque boxes and do not provide checkable evidence for their judgments, possibly limiting their effectiveness.<n>We propose a retrospective, step-aware formal verification framework $Safe$. Rather than assigning arbitrary scores, we strive to articulate mathematical claims in formal mathematical language Lean 4 at each reasoning step and provide formal proofs to identify hallucinations.
  arXiv  Detail & Related papers  (2025-06-05T03:16:08Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  We introduce Goedel-Prover, an open-source language model that achieves state-of-the-art (as of April 5 2025) performance in automated formal proof generation for mathematical problems.<n>First, we train LLMs to convert natural language math problems from the Numina dataset to equivalent formal statements in Lean 4.<n>Next, we develop a large dataset of formal proofs by training a series of provers.<n>Finally, we obtain the dataset Goedel-Pset-v1-solved, which contains proofs for over 800K statements from Goedel-Pset-v1
  arXiv  Detail & Related papers  (2025-02-11T15:27:35Z)
• Post-quantum encryption algorithms of high-degree 3-variable polynomial congruences: BS cryptosystems and BS key generation [0.0]
  We will construct post-quantum encryption algorithms based on three-variable Beal-Schur congruence. We will apply this result to generate simple and secure post-quantum encryption algorithms.
  arXiv  Detail & Related papers  (2024-08-14T14:19:46Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Partial Proof of a Conjecture with Implications for Spectral Majorization [0.43512163406551996]
  We present new results relating to a conjecture regarding properties of $ntimes n$, $nleq 6$, positive definite matrices. We conclude with general considerations on the future of computer-assisted and AI-based proofs.
  arXiv  Detail & Related papers  (2023-09-04T01:02:19Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  Theorem proving in natural mathematical language plays a central role in mathematical advances and education. We develop NaturalProver, a language model that generates proofs by conditioning on background references. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time.
  arXiv  Detail & Related papers  (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  We present a novel stepwise method NLProofS (Natural Language Proof Search) NLProofS learns to generate relevant steps conditioning on the hypothesis. It achieves state-of-the-art performance on EntailmentBank and RuleTaker.
  arXiv  Detail & Related papers  (2022-05-25T02:22:30Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
  arXiv  Detail & Related papers  (2021-06-02T17:58:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.