Related papers: Formalization and Implementation of Algebraic Meth…
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…
The formalisation of mathematics is starting to become routine, but the value of this technology to the work of mathematicians remains to be shown. There are few examples of using proof assistants to verify brand-new work. This paper…
In 1970s, a method was developed for integration of nonlinear equations by means of algebraic geometry. Starting from a Lax representation with spectral parameter, the algebro-geometric method allows to solve the system explicitly in terms…
We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concrete models of programs based on languages and execution…
Isabelle/PIDE has emerged over more than 10 years as the standard Prover IDE for interactive theorem proving in Isabelle. The well-established Archive of Formal Proofs (AFP) testifies the success of such applications of formalized…
In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and…
Despite the considerable interest in new dependent type theories, simple type theory (which dates from 1940) is sufficient to formalise serious topics in mathematics. This point is seen by examining formal proofs of a theorem about…
The Riemann hypothesis is, and will hopefully remain for a long time, a great motivation to uncover and explore new parts of the mathematical world. After reviewing its impact on the development of algebraic geometry we discuss three…
An Isabelle/HOL formalisation of G\"odel's two incompleteness theorems is presented. The work follows \'Swierczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of…
Tropical geometry is a piecewise linear "shadow" of algebraic geometry. It allows for the computation of several cohomological invariants of an algebraic variety. In particular, its application to enumerative algebraic geometry led to…
In this paper we introduce elements of algebraic geometry over an arbitrary algebraic structure. We prove Unification Theorems which gather the description of coordinate algebras by several ways.
Designing software systems for Geometric Computing applications can be a challenging task. Software engineers typically use software abstractions to hide and manage the high complexity of such systems. Without the presence of a unifying…
Geometric (Clifford) algebra provides an efficient mathematical language for describing physical problems. We formulate general relativity in this language. The resulting formalism combines the efficiency of differential forms with the…
This document reports on the use of an algebraic, visual, formal approach to the specification of patterns for the formalization of the GoF design patterns. The approach is based on graphs, morphisms and operations from category theory and…
Parametric Gr\"obner bases have been studied for more than 15 years and are now a further developed subject. Here we propose a general study of parametric standard bases, that is with local orders. We mainly focus on the commutative case…
We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph transformations. We have built high-level models of the data…
Applying Gr\"obner basis theory to concrete problems in Lean 4 remains difficult since the current formalization of multivariate polynomials is based on a non-computable representation and is therefore not suitable for efficient symbolic…
Formal methods have provided approaches for investigating software engineering fundamentals and also have high potential to improve current practices in dependability assurance. In this article, we summarise known strengths and weaknesses…
We outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry. We propose a construction of a dictionary between automated theorem provers and (La)TeX exploiting syntactic…
An algebraic technique adapted to the problems of the fundamental theoretical physics is presented. The exposition is an elaboration and an extension of the methods proposed in previous works by the aut