Formalising the Bruhat-Tits Tree
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. 27 pages. Final version, to appear in Annals of Formalized Mathematics
Fields of Study & Subjects
Logic
programming
and type systems
Analytic Number Theory Research
Computability
AI Algorithms
Publication details
- Journal / source
- Annals of Formalized Mathematics
- Volume
- Volume 2
- Publication date
- 21 April 2026
- Language
- EN