Formalising the Bruhat-Tits Tree
Number Theory
2026-04-22 v4 Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.2505.12933,
title = {Formalising the Bruhat-Tits Tree},
author = {Judith Ludwig and Christian Merten},
journal= {arXiv preprint arXiv:2505.12933},
year = {2026}
}
Comments
27 pages. Final version, to appear in Annals of Formalized Mathematics