发表机构
Research Institute for Mathematical Sciences, Kyoto University（京都大学数学科学研究所）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
在Lean 4中形式化了Langlands第二主引理，解决单位根歧义，涵盖野生二进情形，并验证了数学证明的新部分。
AI 中文摘要
我们在Lean 4中形式化了Langlands关于非阿基米德局部域上局部epsilon因子的第二主引理。该引理比较了双循环伽罗瓦扩张中不同中间域的字符的局部常数。证明遵循作者随附的数学论文，并使用了第一主引理的形式化。第一主引理仅给出幂关系，留下单位根歧义。解决这一歧义是证明的主要部分，需要根据分歧进行进一步分析。野生二进情形是随附证明中数学上新的部分，其Lean形式化提供了对这一新情形的机器检查验证。混合特征和等特征均被包括。我们给出了精确的Lean陈述，识别了各个情形中使用的声明，并描述了形式化所建议的数学证明的六处简化。ChatGPT协助从数学手稿中转移公式和引用，并添加对相应Lean源代码的引用，以及对论文措辞提出改进建议。
英文摘要
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.
