Related papers: Formalising Sylow's theorems in Coq
This is the second installment of an exposition of an ACL2 formalization of finite group theory. The first, which was presented at the 2022 ACL2 workshop, covered groups and subgroups, cosets, normal subgroups, and quotient groups,…
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…
Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proof systems, making the formalization of circular proof…
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of…
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic…
Galois theory is developed using elementary polynomial and group algebra. The method follows closely the original prescription of Galois, and has the benefit of making the theory accessible to a wide audience. The theory is illustrated by a…
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support…
This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex…
This notes explains how a standard algorithm that constructs the discrete Fourier transform has been formalised and proved correct in the Coq proof assistant using the SSReflect extension.
In this paper, we describe the formalization of the axiom of choice and several of its famous equivalent theorems in Morse-Kelley set theory. These theorems include Tukey's lemma, the Hausdorff maximal principle, the maximal principle,…
The note offers a proof of Darboux and Liouville theorems from a symplectic group action perspective.
We consider the question whether a Sylow like theorem is valid in the normalized units of integral group rings of finite groups. After a short survey on the known results we show that this is the case for integral group rings of Frobenius…
A new, configuration-space picture of a formalism of group quantization, the GAQ formalism, is presented in the context of a previous, algebraic generalization. This presentation serves to make a comprehensive discussion in which other…
For G = PSL(2,p^f) denote by ZG the integral group ring, by V(ZG) the group of normalized units of ZG and let r be a prime different from p. Using the so called HeLP-method we prove, that units of r-power order in V(ZG) are rationally…
Using theory of props we prove a formality theorem associated with universal quantizations of (strongly homotopy) Lie bialgebras.
We give a direct and elementary proof of the theorem on formal functions by studying the behaviour of the Godement resolution of a sheaf of modules under completion.
Previous formulations of group theory in ACL2 and Nqthm, based on either "encapsulate" or "defn-sk", have been limited by their failure to provide a path to proof by induction on the order of a group, which is required for most interesting…
Viewing Kan complexes as $\infty$-groupoids implies that pointed and connected Kan complexes are to be viewed as $\infty$-groups. A fundamental question is then: to what extent can one "do group theory" with these objects? In this paper we…
We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their…
The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal…