Formalising the Bruhat-Tits Tree

TL;DR

This paper formalizes the Bruhat-Tits tree in the Lean Theorem Prover and applies it to verify a result about harmonic cochains, bridging number theory and formal verification.

Contribution

It introduces a formalization of the Bruhat-Tits tree in Lean and demonstrates its use in verifying a specific mathematical result.

Findings

Successful formalization of the Bruhat-Tits tree in Lean

Verification of a harmonic cochains result on the tree

Enhanced connection between number theory and formal methods

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.