Pell and quadratic Diophantine equations

Pell and negative Pell equations, norm equations, Pythagorean triples, Markov triples and quadratic equations in two or three variables.

• Büchi's problem
• Generalized Markov triples
• Negative Pell equation and angle bisectors
• Pell equation solutions in a rotated square
• Pell's equation
• Pythagorean triples
• Shadow Markov triples
• Sums of consecutive squares

TheoremChen's theorem for Markoff graphs#●ready to prove

Let \(p > 3\) be a prime. The Markoff graph over \(\mathbb{Z}/p\mathbb{Z}\) has as vertices the nonzero triples \((x_0, x_1, x_2)\) of elements of \(\mathbb{Z}/p\mathbb{Z}\) with \(x_0^2 + x_1^2 + x_2^2 = 3 x_0 x_1 x_2\), and two distinct triples are adjacent when one is obtained from the other by a Vieta involution, which replaces one coordinate \(x_i\) by \(3 x_j x_k - x_i\) and keeps the other two coordinates \(x_j\), \(x_k\), where \(\{i, j, k\} = \{0, 1, 2\}\). Every connected component of this graph has a number of vertices divisible by \(p\).

public theorem_wanted dvd_card_connectedComponent_markoffGraph
    {p : ℕ} (hp : Nat.Prime p) (hgt : 3 < p) :
    ∀ c : (markoffGraph p).ConnectedComponent, p ∣ Nat.card c

Sources

• https://link.springer.com/article/10.1007/s00222-025-01346-9. Problem dvd_card_connectedComponent_markoffGraph of the lean-eval benchmark.

TheoremInteger solutions of \(x^2 - xy - y^2 = \pm 1\)#✓fully proved

For integers \(x\) and \(y\), we have \(x^2 - xy - y^2 = 1\) or \(x^2 - xy - y^2 = -1\) if and only if there are an integer \(n\) and a sign \(s \in \{1, -1\}\) with \(x = s F_n\) and \(y = s F_{n-1}\). Here \((F_n)_{n \in \mathbb{Z}}\) is the Fibonacci sequence extended to all integers by \(F_0 = 0\), \(F_1 = 1\) and \(F_{n+2} = F_{n+1} + F_n\) for every integer \(n\).

theorem fibonacci_norm_eq_one_or_neg_one_iff (x y : ℤ) :
    (x ^ 2 - x * y - y ^ 2 = 1 ∨ x ^ 2 - x * y - y ^ 2 = -1) ↔
      ∃ n s : ℤ, (s = 1 ∨ s = -1) ∧ x = s * Int.fib n ∧ y = s * Int.fib (n - 1)

Sources

• Bahar Demirtürk and Refik Keskin, “Integer Solutions of Some Diophantine Equations via Fibonacci and Lucas Numbers”, Journal of Integer Sequences 12 (2009), Article 09.8.7, Theorem 1.2 at source lines 171–175, https://cs.uwaterloo.ca/journals/JIS/VOL12/Demirturk/demirturk3.tex.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.