ProbXiv
sign in
Problem archiveProblem record

Statement

For A⊆FpA \subseteq \mathbb{F}_p let A∗=(A+A)∪(AA)A^* = (A+A) \cup (AA). Sárközy conjectured that for all large primes, every set of size at least cpc\sqrt{p} has A∗=FpA^* = \mathbb{F}_p-like covering behaviour. Disproved with an explicit construction from the classical cross-ratio orbit, together with the exact extremal value.

Record

Added

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. construction · #1

    Quanyu Tang, using Harmonic Aristotle

    That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.

    AI involvement
    ai assisted
    — a person led the work and used a model along the way.

    Aristotle produced formal Lean proofs of all four principal statements of the paper (the formalization is public), and "was also used to assist in the preparation of this paper." The counterexample construction itself builds on a classical projective-geometric orbit.

  2. Machine-checked by Lean on #1 · not a person

    lean: partially checkedLean

    scope Lean formalization of the core argument; statement correspondence not independently audited

    All four principal statements formalized and checked in Lean; Wouter van Doorn assisted with the formalization. No independent expert review yet. Tier: the formalization was produced within the project (Aristotle, with van Doorn assisting); no independent statement audit.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.