相关论文: Formal verification of Zagier's one-sentence proof

We show that Fermat's last theorem and a combinatorial theorem of Schur on monochromatic solutions of $a+b=c$ implies that there exist infinitely many primes. In particular, for small exponents such as $n=3$ or $4$ this gives a new proof of…

In this paper, we investigate two methods to express the natural powers of $2$ as sums over integer partitions. First we consider a formula by N. J. Fine that allows us to express a binomial coefficient in terms of multinomial coefficients…

We present formalized proofs verifying that the first-order unification algorithm defined over lists of satisfiable constraints generates a most general unifier (MGU), which also happens to be idempotent. All of our proofs have been…

We give a new proof that there are infinitely many primes, relying on van der Waerden's theorem for coloring the integers, and Fermat's theorem that there cannot be four squares in an arithmetic progression. We go on to discuss where else…

Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dynamically change the precision of each intermediate operation…

We prove two positivity conjectures proposed by Guo for alternating sums and factorial ratios built from Gaussian coefficients. The first result proves the positivity of the odd $q$-super Catalan numbers \[…

By combining classical techniques together with two novel asymptotic identities contained in [FL], we analyse certain single sums of Riemann-zeta type. In addition, we analyse Euler-Zagier double exponential sums for particular values of…

One of the proposed solutions for improving the scalability of semantics of programming languages is Component-Based Semantics, introduced by Peter D. Mosses. It is expected that this framework can also be used effectively for modular meta…

The purpose of this paper is to discuss the relationship between prime numbers and sums of Fibonacci numbers. One of our main results says that for every sufficiently large integer $k$ there exists a prime number that can be represented as…

Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a…

With the aid of Hensel Lemma, we refine the 2-adic Newton polygon algorithm proposed by Magron, Koprowski, and Vaccon at ISSAC 2023 to express computationally a given positive univariate polynomial with rational coefficients as a sum of…

In this document we define a method of proof that we call proof by dichotomy. Its field of application is any proposition on the set of natural numbers N. It consists in the repetition of a step. A step proves the proposition for half of…

Zaremba's conjecture (1971) states that every positive integer number $d$ can be represented as a denominator (continuant) of a finite continued fraction $\frac{b}{d}=[d_1,d_2,...,d_{k}],$ with all partial quotients $d_1,d_2,...,d_{k}$…

We describe the formalisation in Coq of a proof that the numbers e and $\pi$ are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex…

Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and…

MaxSAT, the optimization version of the well-known SAT problem, has attracted a lot of research interest in the last decade. Motivated by the many important applications and inspired by the success of modern SAT solvers, researchers have…

We develop a diagrammatic proof system for a fragment of structural semantics inspired by the Greimas semiotic square, using spider diagrams as the underlying formalism. The basic terms are represented as diagrammatic configurations, and…

We give a new sufficient condition which allows to test primality of Fermat's numbers. This characterization uses uniquely values at most equal to tested Fermat number. The robustness of this result is due to a strict use of elementary…

An efficient intuitionistic first-order prover integrated into Coq is useful to replay proofs found by external automated theorem provers. We propose a two-phase approach: An intuitionistic prover generates a certificate based on the matrix…

We revisit the direct sum questions in communication complexity which asks whether the resource needed to solve $n$ communication problems together is (approximately) the sum of resources needed to solve these problems separately. Our work…