The Bruhat-Tits tree is an important combinatorial tool in number theory and representation theory of GL_n, but it has not been formalized in a proof assistant or connected to ongoing research applications.

The authors formalize the Bruhat-Tits tree in Lean, starting from the Cartan decomposition of GL_n(K) over a discrete valuation ring. The tree is constructed from lattice classes in K^2 modulo homothety, with edges defined by containment relations. The formalization is applied to verify a result about harmonic cochains on the tree.

The formalization covers the Cartan decomposition, the construction of the Bruhat-Tits tree from lattice classes, and a verified result on harmonic cochains. Parts of the work have been integrated into Mathlib via merged pull requests, including the notion of R-lattices and cardinality results for projectivizations of finite vector spaces.