{
  "abstract": "The openai/math release contains an AI-generated Lean 4 proof that the triangular lattice A of covolume one minimises the lower g-energy among all locally finite planar configurations of density one, for every smooth completely monotone g (theorem universal_energy_minimum; Comparator-accepted by us under the pinned toolchain). Inside that pinned environment we derive and kernel-check three named consequences, using only the axioms propext, Classical.choice and Quot.sound: (D1) for every s > 0 the Riesz potential t ↦ t-s/2 (i.e. |x-y|-s) is admissible, so the triangular lattice minimises the Riesz s-energy among all locally finite density-one configurations; (D1b) for s > 2 the lattice's Riesz s-energy (an Epstein zeta value) is finite, so D1 compares with a finite, attained minimum (for 0 < s ≤ 2 the lattice side is infinite and D1 only says E(C) = ∞); (D2) for every density ρ > 0 and every admissible g, the rescaled lattice ρ-1/2A has density ρ and minimises the g-energy among all locally finite density-ρ configurations; without the rescaling the statement is false (proved in Lean at ρ = 1/4, s = 4). The Riesz form ρs/2 Σ|a|-s ≤ E(C) is also kernel-checked. Mathematically each step is short (complete monotonicity of t-s/2, scaling), and the upstream manuscript already states informally that inverse powers are included; what is new is the kernel-checked form, a statement-fidelity audit against Cohn–Kumar–Miller–Radchenko–Viazovska's lower-energy formulation, planted negative controls, and re-verification by separate instances of the same AI model (producer ≠ verifier). Everything is conditional on the upstream theorem, which has not been peer reviewed and which, by its authors' account, does not claim the stronger per-potential form of the Cohn–Kumar conjecture. The Lean proofs, audit, verification runs and drafting were performed by the AI model Claude (Anthropic) under the author's direction; the author is responsible for the content.",
  "abstract_shown": true,
  "affiliations": [
    "SocrateAI Lab"
  ],
  "article_type": null,
  "arxiv": null,
  "author_total": 1,
  "authors": [
    {
      "affs": [
        0
      ],
      "name": "Xavier Callens"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/fhr2avz12mtaq.bib",
  "cited_by": 6,
  "doi": "10.5281/zenodo.23285630",
  "fulltext_url": null,
  "id": "fhr2avz12mtaq",
  "issns": [],
  "landing_url": "https://doi.org/10.5281/zenodo.23285630",
  "language": "en",
  "licence": "CC-BY",
  "licence_label": "CC BY",
  "licence_source": "journal",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": null,
  "native_subjects": [
    [
      "openalex",
      "2602|Analytic Number Theory Research"
    ]
  ],
  "openalex": "W7221337613",
  "pdf_url": null,
  "pmcid": null,
  "pmid": null,
  "published": "2026-10-10",
  "publisher": "European Organization for Nuclear Research",
  "ris": "https://research.draconitic.com/paper/fhr2avz12mtaq.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:17Z",
      "native_id": "W7221337613",
      "source": "openalex",
      "url": "https://doi.org/10.5281/zenodo.23285630"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "openalex:2602|Analytic Number Theory Research",
      "subfield": "algebra-number-theory"
    }
  ],
  "title": "Riesz-energy, finiteness and every-density corollaries of the openai/math planar universal-optimality theorem, kernel-checked in Lean 4",
  "title_text": "Riesz-energy, finiteness and every-density corollaries of the openai/math planar universal-optimality theorem, kernel-checked in Lean 4",
  "type": "preprint",
  "updated_at": "2026-11-06T13:20:22Z",
  "url": "https://research.draconitic.com/paper/fhr2avz12mtaq",
  "venue": "Zenodo (CERN European Organization for Nuclear Research)",
  "versions": []
}