Formalising the Bruhat-Tits Tree
Pith reviewed 2026-05-22 14:35 UTC · model grok-4.3
The pith
The Bruhat-Tits tree has been formalized in Lean and used to verify a result about harmonic cochains.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
We describe the formalisation of the Bruhat-Tits tree 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.
What carries the argument
The Lean formalization of the Bruhat-Tits tree, which supplies the combinatorial structure needed to define harmonic cochains and prove their properties.
If this is right
- The verified result on harmonic cochains now rests on a machine-checked foundation.
- Researchers can extend the formalization to prove further properties of the Bruhat-Tits tree.
- The work demonstrates that structures from number theory can be rendered in Lean at a level sufficient for ongoing research questions.
- Similar formalizations become feasible for other combinatorial objects arising in p-adic geometry.
Where Pith is reading between the lines
- The same approach could support formal verification of results involving Bruhat-Tits buildings in higher rank.
- Once available, the library might enable computational experiments that mix symbolic proof with numerical checks on the tree.
- It suggests a route for gradually bringing more of the arithmetic theory of p-adic groups under formal control.
Load-bearing premise
The Lean definitions of the Bruhat-Tits tree and of harmonic cochains correctly capture the standard mathematical notions used in number theory literature.
What would settle it
A direct comparison revealing that the Lean statements about the tree or the verified cochain property fail to match the corresponding definitions and theorems in the number theory literature.
read the original 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper describes the formalization of the Bruhat-Tits tree in the Lean theorem prover, with vertices as homothety classes of lattices in a 2-dimensional vector space over a local field and edges corresponding to index-p inclusions, together with the group action of GL(2). It then applies the formalization to verify a result concerning harmonic cochains (functions on edges satisfying a sum-zero condition at each vertex).
Significance. If the Lean definitions faithfully reproduce the standard mathematical notions, the work supplies a machine-checked library for an object central to the study of p-adic groups, automorphic forms, and Bruhat-Tits theory. The verified statement on harmonic cochains provides a concrete, non-trivial example of the formalization's utility and strengthens the case for using Lean in number-theoretic research.
major comments (2)
- [§2] §2 (Definitions of the Bruhat-Tits tree): The formalization of vertices as homothety classes of lattices and of edges via index-p inclusions must be accompanied by an explicit statement or lemma establishing equivalence with the standard construction in the literature (e.g., Serre or the original Bruhat-Tits papers), including the precise treatment of the local field and the induced GL(2) action; without this, the subsequent verification of the cochain result does not automatically transfer to the mathematical statement.
- [§4] §4 (Application to harmonic cochains): The precise mathematical statement being verified should be quoted or referenced (including the original source), together with a clear indication of which properties of the tree are used in the proof; this is load-bearing for assessing whether the formal result substantiates the claimed number-theoretic assertion.
minor comments (2)
- [Abstract] The abstract would be clearer if it briefly indicated the specific result about harmonic cochains that is verified.
- Notation for the local field and the valuation should be introduced once and used consistently throughout the definitions and statements.
Simulated Author's Rebuttal
We thank the referee for the careful reading of the manuscript and the constructive comments. We respond to each major comment below and indicate the revisions we will make.
read point-by-point responses
-
Referee: [§2] §2 (Definitions of the Bruhat-Tits tree): The formalization of vertices as homothety classes of lattices and of edges via index-p inclusions must be accompanied by an explicit statement or lemma establishing equivalence with the standard construction in the literature (e.g., Serre or the original Bruhat-Tits papers), including the precise treatment of the local field and the induced GL(2) action; without this, the subsequent verification of the cochain result does not automatically transfer to the mathematical statement.
Authors: We agree that an explicit link between the formal definitions and the classical construction is necessary for the verified result to apply directly to the standard object in the literature. In the revised version we will add a lemma in §2 stating the equivalence of our definition (vertices as homothety classes of lattices in a two-dimensional vector space over a local field, edges given by index-p inclusions) with the construction in Serre’s Trees and the original Bruhat–Tits papers. The lemma will also record how the GL(2) action is induced on our formal tree so that it matches the usual action. revision: yes
-
Referee: [§4] §4 (Application to harmonic cochains): The precise mathematical statement being verified should be quoted or referenced (including the original source), together with a clear indication of which properties of the tree are used in the proof; this is load-bearing for assessing whether the formal result substantiates the claimed number-theoretic assertion.
Authors: We accept that quoting the exact statement and identifying the tree properties used will improve clarity. In the revised manuscript we will quote the precise result on harmonic cochains (with its original source) at the start of §4. We will also add a short paragraph listing the properties of the tree—its tree structure, the sum-zero condition defining harmonic cochains, and the relevant features of the GL(2) action—that are invoked in the formal proof. revision: yes
Circularity Check
Direct formalization with no circular derivation chain
full rationale
The paper presents a formalization of the Bruhat-Tits tree and harmonic cochains in Lean, followed by verification of an existing result on those cochains. This is a direct encoding of standard mathematical definitions (vertices as homothety classes of lattices, edges via index-p inclusions, and the sum-zero condition for harmonic cochains) rather than a derivation that reduces any claim to fitted parameters, self-definitions, or load-bearing self-citations. The central claim is the correctness of the formal objects and the verification they enable; no step equates a 'prediction' to its own input by construction. The assumption that the Lean definitions match literature notions is an external correctness criterion for formalization work, not an internal circular reduction. No self-citation chains or ansatzes are invoked to force the result.
Axiom & Free-Parameter Ledger
axioms (1)
- standard math Standard axioms and definitions of mathematics as implemented in the Lean theorem prover
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.