Formalising the Local Compactness of the Adele Ring
<|reference_start|>Formalising the Local Compactness of the Adele Ring: The adele ring of a number field is a central object in modern number theory. Its status as a locally compact topological ring is one of the key reasons why, leading to its widespread use within the Langlands Program. We describe a formal proof that the adele ring of a number field is locally compact in the Lean 4 theorem prover. Our work includes the formalisations of new types, including the completion of a number field at an infinite place and the finite $S$-adele ring, as well as formal proofs that completions of a number field are locally compact and their rings of integers at finite places are compact.<|reference_end|>
@article{mercuri2024formalising,
    title={Formalising the Local Compactness of the Adele Ring},
    author={Salvatore Mercuri},
    journal={arXiv preprint arXiv:2405.19270},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.19270},
    primaryClass={cs.LO math.NT}
}