Related papers: Formalising the Bruhat-Tits Tree

For performance and verification in machine learning, new methods have recently been proposed that optimise learning systems to satisfy formally expressed logical properties. Among these methods, differentiable logics (DLs) are used to…

In this sequel to [1], we take up a second approach in bending the Bruhat-Tits tree. Inspired by the BTZ black hole connection, we demonstrate that one can transplant it to the Bruhat-Tits tree, at the cost of defining a novel "exponential…

We investigate Bruhat-Tits buildings and their compactifications by means of Berkovich analytic geometry over complete non-Archimedean fields. For every reductive group G over a suitable non-Archimedean field k we define a map from the…

While Chain-of-Thought (CoT) prompting enhances the reasoning capabilities of large language models, the faithfulness of the generated rationales remains an open problem for model interpretability. We propose a novel theoretical lens for…

Programs that manipulate tree-shaped data structures often require complex, specialized proofs that are difficult to generalize and automate. This paper introduces a unified, foundational approach to verifying such programs. Central to our…

This paper proposes a natural language translation method for machine-verifiable formal proofs that leverages the informalization (verbalization of formal language proof steps) and summarization capabilities of LLMs. For evaluation, it was…

Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting…

We study the action on the Bruhat-Tits tree of unit groups of maximal orders in certain quaternion algebras over $\mathbb{F}_q(T)$ and discuss applications to arithmetic geometry and group theory.

While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structures in concrete settings. With the goal of auto-formalizing…

Artificial intelligence assisted mathematical proof has become a highly focused area nowadays. One key problem in this field is to generate formal mathematical proofs from natural language proofs. Due to historical reasons, the formal proof…

In this paper we investigate the use of the concept of tree dimension in Horn clause analysis and verification. The dimension of a tree is a measure of its non-linearity - for example a list of any length has dimension zero while a complete…

We apply the theory of fundamental strata of Bremer and Sage to find cohomologically rigid $G$-connections on the projective line, generalising the work of Frenkel and Gross. In this theory, one studies the leading term of a formal…

Let k be a local field and let A be the two-by-two matrix algebra over k. In our previous work we developed a theory that allows the computation of the set of maximal orders in A containing a given suborder. This set is given as a sub-tree…

The continuous functional calculus is perhaps the most fundamental construction in the theory of operator algebras, especially $C^{*}$-algebras. Here we document our formalization of the continuous functional calculus in Lean, which…

We use the theory of arithmetic quotients of the Bruhat-Tits tree developed by Serre and others to obtain Dirichlet-style theorems for Diophantine approximation on global function fields. This approach allows us to find sharp values for the…

Using theory of props we prove a formality theorem associated with universal quantizations of (strongly homotopy) Lie bialgebras.

We give an algorithm to explicitly compute the largest subtree, in the local Bruhat-Tits tree for PSL_2(k), whose vertices correspond to orders containing a given suborder H, in terms of a set of generators for H. The shape of this subtree…

Based on bulk reconstruction from the finite boundary of the Bruhat-Tits tree, the boundary effective theory is obtained after integrating out fields outside this boundary. According to the $~p$-adic version of Anti-de Sitter/Conformal…

There is a long tradition of fruitful interaction between logic and social choice theory. In recent years, much of this interaction has focused on computer-aided methods such as SAT solving and interactive theorem proving. In this paper, we…

We present an exposition of the *Chain Bounding Lemma*, which is a common generalization of both Zorn's Lemma and the Bourbaki-Witt fixed point theorem. The proofs of these results through the use of Chain Bounding are amongst the simplest…