{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1822",
  "content_hash": null,
  "slug": "erdos152-formalization-upstream-lean-v1",
  "type": "formalization",
  "title": "Pinned Lean proof from AlphaProof Nexus",
  "summary": "A public Lean 4.27.0 file proves the explicit quadratic bound and the target limit; controlled TheoremDB verification is still pending.",
  "relevance": "This is the public formal proof that originally established the result, preserved with its exact dependency world and statement boundary.",
  "relevance_source": "recorded",
  "body": "The source defines `f n` as the infimum of the number of isolated elements of A + A over Sidon subsets of the natural numbers with cardinality n. Its main quantitative lemma is `num_isolated_lower_bound`, which proves 16 times the isolated count plus 100n plus 16 is at least n squared. The file then derives `tendsto_f` and closes `target_theorem_0`, the Formal Conjectures answer wrapper for the affirmative answer. The pinned file contains no `sorry`, `admit`, `native_decide`, custom `axiom`, `opaque`, or `unsafe` declaration. The accompanying paper says successful sketches were passed through SafeVerify and that experts checked statement fidelity. TheoremDB has pinned the exact source and dependencies but has not rerun this project in its own controlled verifier.",
  "status": "pending_verification",
  "evidence_grade": "unverified_formalization",
  "scope": {
    "kind": "universal",
    "statement": "the Formal Conjectures minimum isolated-sum function over finite Sidon subsets of the natural numbers"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "lean4_formalization_source",
    "command": "lake env lean APNOutputs/ErdosProblems/erdos_152.lean",
    "entrypoint": "Erdos152.target_theorem_0",
    "runtime": "Lean 4.27.0 with Formal Conjectures at 7862bf6a6976c26acb086b6b2cec12ad1d92ce5d and mathlib4 at a3a10db0e9d66acbebf76c5e6a135066525ac900",
    "citation": {
      "url": "https://github.com/google-deepmind/alphaproof-nexus-results/tree/0647711a71183c1ea492ad60860776617ce1ea88",
      "locator": "APNOutputs/ErdosProblems/erdos_152.lean, lemmas num_isolated_lower_bound, f_lower_bound_div, and tendsto_f, plus theorem target_theorem_0"
    },
    "outputs": {
      "paper_reports_safeverify": true,
      "target_file_source_scan": "no sorry, admit, native_decide, custom axiom, opaque, or unsafe declaration",
      "theoremdb_controlled_verification": "pending"
    },
    "missing": [
      "source"
    ]
  },
  "formal_statement": "theorem Erdos152.target_theorem_0 :\n  answer True ↔ Tendsto Erdos152.f atTop atTop",
  "source": {
    "url": "https://github.com/google-deepmind/alphaproof-nexus-results/tree/0647711a71183c1ea492ad60860776617ce1ea88",
    "locator": "APNOutputs/ErdosProblems/erdos_152.lean, lemmas num_isolated_lower_bound, f_lower_bound_div, and tendsto_f, plus theorem target_theorem_0"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R1821",
      "title": "The minimum isolated-sum count grows at least quadratically",
      "object_type": "claim",
      "relation": "formalizes",
      "direction": "outgoing"
    },
    {
      "slug": "erdos-152-isolated-sidon-sums",
      "title": "erdos 152 isolated sidon sums",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}