Related papers: Formalising the Bruhat-Tits Tree
We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define…
The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO and have made significant progress. This paper focuses on formal verification,…
In this short note we discuss recent results on hook length formulas of trees unifying some earlier results, and explain hook length formulas naturally associated to families of increasingly labelled trees.
This work presents a formalization of the theorem of existence of most general unifiers in first-order signatures in the higher-order proof assistant PVS. The distinguishing feature of this formalization is that it remains close to the…
We present a formalization, in the theorem prover Lean, of the classification of solvable Lie algebras of dimension at most three over arbitrary fields. Lie algebras are algebraic objects which encode infinitesimal symmetries, and as such…
This report presents a formalization of May's theorem in the proof assistant Coq. It describes how the theorem statement is first translated into Coq definitions, and how it is subsequently proved. Various aspects of the proof and related…
This thesis documents a voyage towards truth and beauty via formal verification of theorems. To this end, we develop libraries in Lean 4 that present definitions and results from diverse areas of MathematiCS (i.e., Mathematics and Computer…
This work is devoted to the study of representations of finite subgroups of the group of units of quaternion division algebras over a global or local field arising from the inclusion via extension of scalars splitting the algebra. Following…
Clustering procedure for the case where instead of a fixed metric one applies a family of metrics is considered. In this case instead of a classification tree one obtains a classification network (a directed acyclic graph with non directed…
Let \Gamma be a geometrically finite tree lattice. We prove a Khintchine-Sullivan type theorem for the Hausdorff measure of the points at infinity of the tree that are well approximated by the parabolic fixed points of G. Using Bruhat-Tits…
In order to properly train a machine learning model, data must be properly collected. To guarantee a proper data collection, verifying that the collected data set holds certain properties is a possible solution. For example, guaranteeing…
The paper offers a mathematical formalization of the Turing test. This formalization makes it possible to establish the conditions under which some Turing machine will pass the Turing test and the conditions under which every Turing machine…
Viewing formal mathematical proofs as logical terms provides a powerful and elegant basis for analyzing how human experts tend to structure proofs and how proofs can be structured by automated methods. We pursue this approach by (1)…
Trellises are crucial graphical representations of codes. While conventional trellises are well understood, the general theory of (tail-biting) trellises is still under development. Iterative decoding concretely motivates such theory. In…
We provide a rigorous framework for handling uncertainty in quantitative fault tree analysis based on fuzzy theory. We show that any algorithm for fault tree unreliability analysis can be adapted to this framework in a fully general and…
Motivated by the Bruhat and Cartan decompositions of general linear groups over local fields, double cosets of the group of label preserving automorphisms of a label-regular tree over the fixator of an end of the tree and over maximal…
We formalise the proof of the first case of Fermat's Last Theorem for regular primes using the \emph{Lean} theorem prover and its mathematical library \emph{mathlib}. This is an important 19th century result that motivated the development…
To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. The…
We have developed a web-based pedagogical proof assistant, the Proof Tree Builder, that lets you apply rules upwards from the initial goal in sequent calculus and Hoare logic for a simple imperative language. We equipped our tool with a…
Parikh's theorem is a fundamental result of the formal language's theory. There had been published many proofs and many papers claimed to provide a simplified proof, but most of them are long and still complicated. We provide the proof that…