scholarly journals Formally Proving the Boolean Pythagorean Triples Conjecture

10.29007/jvdj ◽  
2018 ◽  
Author(s):  
Luís Cruz-Filipe ◽  
Peter Schneider-Kamp
Keyword(s):  
Natural Number ◽  
Mathematical Problem ◽  
Propositional Formula ◽  
Natural Numbers ◽  
Original Proof ◽  
Pythagorean Triples ◽  
Mathematical Argument ◽  
Pythagorean Triple ◽  
The Relationship

In 2016, Heule, Kullmann and Marek solved the Boolean Pythagorean Triples problem: is there a binary coloring of the natural numbers such that every Pythagorean triple contains an element of each color? By encoding a finite portion of this problem as a propositional formula and showing its unsatisfiability, they established that such a coloring does not exist. Subsequently, this answer was verified by a correct-by-construction checker extracted from a Coq formalization, which was able to reproduce the original proof. However, none of these works address the question of formally addressing the relationship between the propositional formula that was constructed and the mathematical problem being considered. In this work, we formalize the Boolean Pythagorean Triples problem in Coq. We recursively define a family of propositional formulas, parameterized on a natural number n, and show that unsatisfiability of this formula for any particular n implies that there does not exist a solution to the problem. We then formalize the mathematical argument behind the simplification step in the original proof of unsatisfiability and the logical argument underlying cube-and-conquer, obtaining a verified proof of Heule et al.’s solution.

Frege’s Theorems on Simple Series

2019 ◽  
pp. 207-234
Author(s):  
William Stirton
Keyword(s):  
Natural Number ◽  
Natural Numbers ◽  
Cardinal Numbers ◽  
Points Of Interest ◽  
Main Observation ◽  
The Relationship

The paper discusses theorems 207, 263, 327 and 348 and the proofs thereof. With fidelity to Frege’s own terminology, we can describe all four theorems as being about simple series. An attempt is made to explain what he meant by “simple series”. The main observation concerning theorems 207 and 263 is that the proofs of these theorems, slightly modified, yield a proof that a set is denumerable if and only if it is simply infinite in Dedekind’s sense. Some philosophical points of interest in this result are noted. Attention is drawn to some technical results proven by Frege which help in understanding the relationship between his own concept of natural number and Dedekind’s. The discussion of theorems 327 and 348 concentrates on critically assessing the claim, made by Heck, that by proving these theorems in the particular way he did Frege was meaning to demonstrate that finite cardinal numbers can be made to do work normally thought of as proper to finite ordinals. While this claim is not clearly wrong, some grounds for doubt are mentioned. One moral is that we should be sceptical about claims like “every foundation of arithmetic must treat the natural numbers as either fundamentally finite cardinals or fundamentally finite ordinals”.

The Natural Numbers

2018 ◽  
Author(s):  
Øystein Linnebo
Keyword(s):  
Natural Number ◽  
Peano Arithmetic ◽  
Number Sequence ◽  
Natural Numbers ◽  
Ordinal Numbers ◽  
Cardinal Numbers

How are the natural numbers individuated? That is, what is our most basic way of singling out a natural number for reference in language or in thought? According to Frege and many of his followers, the natural numbers are cardinal numbers, individuated by the cardinalities of the collections that they number. Another answer regards the natural numbers as ordinal numbers, individuated by their positions in the natural number sequence. Some reasons to favor the second answer are presented. This answer is therefore developed in more detail, involving a form of abstraction on numerals. Based on this answer, a justification for the axioms of Dedekind–Peano arithmetic is developed.

THE SHUFFLE VARIANT OF JEŚMANOWICZ’ CONJECTURE CONCERNING PYTHAGOREAN TRIPLES

2011 ◽  
Vol 90 (3) ◽  
pp. 355-370
Author(s):  
TAKAFUMI MIYAZAKI
Keyword(s):  
Unique Solution ◽  
Pythagorean Triples ◽  
Pythagorean Triple ◽  
Positive Integers

AbstractLet (a,b,c) be a primitive Pythagorean triple such that b is even. In 1956, Jeśmanowicz conjectured that the equation ax+by=cz has the unique solution (x,y,z)=(2,2,2) in the positive integers. This is one of the most famous unsolved problems on Pythagorean triples. In this paper we propose a similar problem (which we call the shuffle variant of Jeśmanowicz’ problem). Our problem states that the equation cx+by=az with x,y and z positive integers has the unique solution (x,y,z)=(1,1,2) if c=b+1 and has no solutions if c>b+1 . We prove that the shuffle variant of the Jeśmanowicz problem is true if c≡1 mod b.

scholarly journals A unified treatment of syntax with binders

2012 ◽  
Vol 22 (4-5) ◽  
pp. 614-704 ◽  
Author(s):  
NICOLAS POUILLARD ◽  
FRANÇOIS POTTIER
Keyword(s):  
Natural Number ◽  
Data Structures ◽  
Transformation Function ◽  
Natural Numbers ◽  
Programming Error ◽  
Free Variables ◽  
De Bruijn ◽  
Abstract Interface ◽  
Representation Techniques ◽  
De Bruijn Indices

AbstractAtoms and de Bruijn indices are two well-known representation techniques for data structures that involve names and binders. However, using either technique, it is all too easy to make a programming error that causes one name to be used where another was intended. We propose an abstract interface to names and binders that rules out many of these errors. This interface is implemented as a library in Agda. It allows defining and manipulating term representations in nominal style and in de Bruijn style. The programmer is not forced to choose between these styles: on the contrary, the library allows using both styles in the same program, if desired. Whereas indexing the types of names and terms with a natural number is a well-known technique to better control the use of de Bruijn indices, we index types with worlds. Worlds are at the same time more precise and more abstract than natural numbers. Via logical relations and parametricity, we are able to demonstrate in what sense our library is safe, and to obtain theorems for free about world-polymorphic functions. For instance, we prove that a world-polymorphic term transformation function must commute with any renaming of the free variables. The proof is entirely carried out in Agda.

SOME NOTES ON A GENERALIZED VERSION OF PYTHAGOREAN TRIPLES

2020 ◽  
Vol 4 (2) ◽  
pp. 103
Author(s):  
Leomarich F Casinillo ◽  
Emily L Casinillo
Keyword(s):  
Diophantine Equation ◽  
Pythagorean Triples ◽  
Pythagorean Triple ◽  
Positive Integers

A Pythagorean triple is a set of three positive integers a, b and c that satisfy the Diophantine equation a^2+b^2=c^2. The triple is said to be primitive if gcd(a, b, c)=1 and each pair of integers and  are relatively prime, otherwise known as non-primitive. In this paper, the generalized version of the formula that generates primitive and non-primitive Pythagorean triples that depends on two positive integers  k and n, that is, P_T=(a(k, n), b(k, n), c(k, n)) were constructed. Further, we determined the values of  k and n that generates primitive Pythagorean triples and give some important results.

scholarly journals Continued Fractions of Square Roots of Natural Numbers

10.14311/1821 ◽  
2013 ◽  
Vol 53 (4) ◽  
Author(s):  
L'ubomíra Balková ◽  
Aranka Hrušková
Keyword(s):  
Natural Number ◽  
Continued Fractions ◽  
Natural Numbers ◽  
Precise Form ◽  
Square Roots

In this paper, we will first summarize known results concerning continued fractions. Then we will limit our consideration to continued fractions of quadratic numbers. The second author describes periods and sometimes the precise form of continued fractions of ?N, where N is a natural number. In cases where we have been able to find such results in the literature, we recall the original authors, however many results seem to be new.

scholarly journals Transporting functions across ornaments

2014 ◽  
Vol 24 (2-3) ◽  
pp. 316-383 ◽  
Author(s):  
PIERRE-ÉVARISTE DAGAND ◽  
CONOR McBRIDE
Keyword(s):  
Type Theory ◽  
Structured Data ◽  
Dependent Types ◽  
Natural Numbers ◽  
Code Reuse ◽  
Domain Specific ◽  
Definition Of ◽  
The Relationship ◽  
Do So ◽  
Structural Invariants

AbstractProgramming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: We can finally write correct-by-construction software. However, this extreme accuracy is also a curse: A datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: The users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.

Compact serialization of Prolog terms (with catalan skeletons, cantor tupling and Gödel numberings)

2013 ◽  
Vol 13 (4-5) ◽  
pp. 847-861 ◽  
Author(s):  
PAUL TARAU
Keyword(s):  
Natural Number ◽  
Memory Representation ◽  
Ranking Algorithm ◽  
Natural Numbers ◽  
Algorithm Mapping ◽  
Data Objects ◽  
Novel Algorithm

AbstractWe describe a compact serialization algorithm mapping Prolog terms to natural numbers of bit-sizes proportional to the memory representation of the terms. The algorithm is a ‘no bit lost’ bijection, as it associates to each Prolog term a unique natural number and each natural number corresponds to a unique syntactically well-formed term.To avoid an exponential explosion resulting from bijections mapping term trees to natural numbers, we separate the symbol content and the syntactic skeleton of a term that we serialize compactly using a ranking algorithm for Catalan families.A novel algorithm for the generalized Cantor bijection between ${\mathbb{N}$ and ${\mathbb{N}$k is used in the process of assigning polynomially bounded Gödel numberings to various data objects involved in the translation.

THE EXCEPTIONAL SET IN THE POLYNOMIAL GOLDBACH PROBLEM

2011 ◽  
Vol 07 (03) ◽  
pp. 579-591 ◽  
Author(s):  
PAUL POLLACK
Keyword(s):  
Asymptotic Formula ◽  
Finite Field ◽  
Natural Number ◽  
Riemann Hypothesis ◽  
Natural Numbers ◽  
Exceptional Set ◽  
Goldbach Problem

For each natural number N, let R(N) denote the number of representations of N as a sum of two primes. Hardy and Littlewood proposed a plausible asymptotic formula for R(2N) and showed, under the assumption of the Riemann Hypothesis for Dirichlet L-functions, that the formula holds "on average" in a certain sense. From this they deduced (under ERH) that all but Oϵ(x1/2+ϵ) of the even natural numbers in [1, x] can be written as a sum of two primes. We generalize their results to the setting of polynomials over a finite field. Owing to Weil's Riemann Hypothesis, our results are unconditional.

Sign in / Sign up

Export Citation Format

Share Document