{
  "abstract": "We formalize in Lean 4 Langlands's Second Main Lemma for local epsilon factors over nonarchimedean local fields. The lemma compares local constants of characters of distinct intermediate fields in a bicyclic Galois extension. The proof follows the author's companion mathematical paper and uses the formalization of the First Main Lemma. The First Main Lemma gives only a power relation, leaving a root-of-unity ambiguity. Resolving this ambiguity is the main part of the proof and requires further analysis according to ramification. The wild dyadic case is the mathematically new part of the companion proof, and its Lean formalization provides a machine-checked verification of this new case. Both mixed and equal characteristic are included. We give the exact Lean statement, identify the declarations used in the individual cases, and describe six simplifications of the mathematical proof suggested by the formalization. ChatGPT assisted with transferring formulas and citations from the mathematical manuscript and with adding references to the corresponding Lean source, and suggested improvements to the wording of the paper.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": "2609.30301",
  "author_total": 1,
  "authors": [
    {
      "name": "Fukuhiro Ueda"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/19emkffsj9027.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2609.30301",
  "fulltext_url": null,
  "id": "19emkffsj9027",
  "issns": [],
  "landing_url": "https://hal.science/hal-05756351v1",
  "language": "en",
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "math.GM"
    ],
    [
      "hal",
      "0.math"
    ],
    [
      "openalex",
      "2610|Advanced Algebra and Geometry"
    ]
  ],
  "openalex": "W7214262202",
  "pdf_url": "https://hal.science/hal-05756351/document",
  "pmcid": null,
  "pmid": null,
  "published": "2026-09-21",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/19emkffsj9027.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:36Z",
      "native_id": "hal-05756351",
      "source": "hal",
      "url": "https://hal.science/hal-05756351v1"
    },
    {
      "first_seen": "2026-10-30T12:34:38Z",
      "native_id": "2609.30301",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2609.30301"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "openalex:2610|Advanced Algebra and Geometry",
      "subfield": "mathematical-physics"
    }
  ],
  "title": "FORMALIZATION OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS",
  "title_text": "FORMALIZATION OF LANGLANDS'S SECOND MAIN LEMMA FOR LOCAL EPSILON FACTORS",
  "type": "preprint",
  "updated_at": "2026-10-30T12:34:38Z",
  "url": "https://research.draconitic.com/paper/19emkffsj9027",
  "venue": "HAL",
  "versions": []
}