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.

翻译：本文描述了在 Lean 定理证明器中形式化 Bruhat-Tits 树——现代数论中的一个重要工具——的过程。基于与当前研究接轨的目标，我们应用此形式化结果验证了该树上调和余链的一个性质。