 |
Judith Ludwig ; Christian Merten - Formalising the Bruhat-Tits Tree
afm:15738 - Annals of Formalized Mathematics, April 21, 2026, Volume 2 - https://doi.org/10.46298/afm.15738Formalising the Bruhat-Tits TreeArticle
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.
27 pages. Final version, to appear in Annals of Formalized Mathematics
Source: arXiv.org:2505.12933
Volume: Volume 2
Published on: April 21, 2026
Accepted on: April 13, 2026
Submitted on: May 23, 2025
Keywords: Number Theory, Logic in Computer Science