{"id":"arxiv/2609.30301","url":"https://arxiv.org/abs/2609.30301","tags":["math.GM"],"score":0,"title":"Formalization of Langlands's Second Main Lemma for Local Epsilon Factors","domain":"math.GM","source":"arxiv","authors":["Fukuhiro Ueda"],"reviews":0,"subject":"math.GM","summary":"We describe the Lean 4 formalization of Langlands's Second Main Lemma for local epsilon factors over nonarchimedean local fields, in mixed and equal characteristic. The lemma compares the induction expressions attached to compatible characters of the intermediate fields of a bicyclic extension of prime-square degree. We explain the mathematical constructions and comparisons that constitute the proof, and identify their Lean declarations.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-20","reactions":{}}