Formalising the Bruhat-Tits Tree
arXiv:2505.12933 · doi:10.46298/afm.15738
Abstract
In this article we describe the formalisation of the Bruhat-Tits tree - an important tool in modern number theory - in the Lean Theorem Prover. Motivated by the goal of connecting to ongoing research, we apply our formalisation to verify a result about harmonic cochains on the tree.
arXiv comment27 pages. Final version, to appear in Annals of Formalized Mathematics