Formalising the Bruhat-Tits Tree
arXiv:2505.129338.8h-index: 5
AI Analysis
This work provides a foundational formalization for number theory in Lean, enabling verification of research-level results.
The authors formalized the Bruhat-Tits tree in the Lean Theorem Prover and used it to verify a result about harmonic cochains, connecting to ongoing research in number theory.
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.