Vela

Is there a set such thatand such that every large integer can be written as for some prime and ? Can the bound be achieved? Must such an satisfy

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

machinery: additive-complement,additive-basis,prime-distribution,sieve/Brun-Titchmarsh,probabilistic-covering,Hardy-Littlewood,additive-combinatorics

use this record

vela registry pull vfr_37aec80d874a0239
vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Let (P) denote the primes, and write the counting function [ A(N):=\lvert A\cap{1,\dots,N}\rvert . ] Your condition is that (P+A) contains all sufficiently large integers (i.e. all but finitely many).

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

3 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · solved (literature)

theorem erdos_32.variants.log_squared : ∃ A : Set ℕ,
    IsAdditiveComplementToPrimes A ∧
    (fun N => (((Finset.Icc 1 N).filter (· ∈ A)).card : ℝ)) =O[atTop]
      fun N => (Real.log N) ^ 2
formal-conjectures/32.lean ↗

status

open

notary

vela reproduce examples/erdos-problems
  • packet.json · sha256 04783a5a9620d5869a3ef07df86f52a19dd018739079424855249d34b4eba42e

finding.noted · reviewer:will-blair · 1 day

renders the record as of vev_d199cb2e · 1,338 events · hub

Search Vela

Jump to a section, signal, campaign, document, primitive, work path, frontier, record index, atlas, constellation, agent, capability, or full-state search.