Related papers: Spreads and Packings of PG(3,2), Formally!
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 paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic…
Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover.…
Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different tools are being increasingly used in…
In this work we find new minimum sizes for the maximal partial spreads of PG$(3,q)$, for $q=8,9,16$ and for every $q$ such that $25\leq q\leq 101$. Furthermore, for $q=8,9,16,25$ and 27 we find all the unknown sizes between our minimums and…
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…
What provides the highest level of assurance for correctness of execution within a programming language? One answer, and our solution in particular, to this problem is to provide a formalization for, if it exists, the denotational semantics…
Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive…
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…
In this paper we give a preliminary formalization of the p-adic numbers, in the context of the second author's univalent foundations program. We also provide the corresponding code verifying the construction in the proof assistant Coq.…
Let $\mathrm{PG}(3,q)$ be the projective space of dimension three over the finite field with $q$ elements. Consider a twisted cubic in $\mathrm{PG}(3,q)$. The structure of the point-plane incidence matrix in $\mathrm{PG}(3,q)$ with respect…
A spread of a Hermitian unital in PG(2,q^2) is a set of q^2+q+1 pairwise disjoint blocks that partition the points of the unital. In this paper, we discuss the results of an exhaustive computer search for spreads of Hermitian unitals of…
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…
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…
Let X be a projective complex 3-fold, quasihomogeneous with respect to an action of a linear algebraic group. We show that X is a compactification of SL_2/G, G a discrete subgroup, or that X can be equivariantly transformed into the 3-dim.…
This report describes three particular technological advances in formal proofs. The HOL Light proof assistant will be used to illustrate the design of a highly reliable system. Today, proof assistants can verify large bodies of advanced…
The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with…
In this article, the partial plane spreads in $PG(6,2)$ of maximum possible size $17$ and of size $16$ are classified. Based on this result, we obtain the classification of the following closely related combinatorial objects: Vector space…
An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and…
Distribution theory is a cornerstone of the theory of partial differential equations. We report on the progress of formalizing the theory of tempered distributions in the interactive proof assistant Lean, which is the first formalization in…