Poking of certain exponential Diophantine equation

Stream: new members

[Ilmārs Cīrulis]

It is this one: w + k2 = k1 * a ^ w, where k1 and k2 are fixed parameters (such that 2 <= k1 < k2) and a and w are variables.
I explored number of solutions, depending on values of the parameters k1 and k2, and it seems that two solutions are the maximum number.

Anyway, I formulated such two conjectures after some experimentation with computer calculations:

import Mathlib

lemma conjecture₁ {k₁ k₂ : ℕ} (hk₁ : 2 ≤ k₁) (hk₂ : k₁ < k₂) :
    {(a, w) | w + k₂ = k₁ * a ^ w}.ncard = 2 ↔
    (∃ t₁ t₂ t₃ : ℕ, k₁ = t₁ + 2 ∧ k₂ = k₁ * ((t₂ + 2) ^ (k₁ * (t₃ + 1) + 1) - (t₃ + 1)) - 1) := by sorry

lemma conjecture₂ {t₁ t₂ t₃ : ℕ} :
    let k₁ := t₁ + 2
    let A := t₂ + 2
    let B := k₁ * (t₃ + 1) + 1
    let C := t₃ + 1
    let k₂ := k₁ * (A ^ B - C) - 1
    ∀ {a w : ℕ}, w + k₂ = k₁ * a ^ w ↔ ((a, w) = (A, B) ∨ (a, w) = (A ^ B - C, 1)) := by sorry

The first one gives me a bijection or smth like that (?) between triples of natural numbers and pairs (k1, k2) such that the equation has exactly two solutions.

The second one gives me way to use any triple to generate specific instance of the equation with two solutions and also to get these two solutions.

Any suggestions how to approach these two? Probably I shouldn't get too hopeful, but what's the worst that can happen? :sweat_smile:

[Kevin Buzzard]

I would first write a loop using a fast computer algebra package to look for counterexamples (having first spent some time thinking how to write the loop efficiently) and leave it on overnight at least. Unfortunately the general theory of Diophantine equations is undecidable and many general statements of this nature turn out to be false (or true but super hard to prove eg beyond known methods)

[Ilmārs Cīrulis]

I arrived at this Diophantine equation when exploring another Diophantine equation --- a ^ b ^ k1 = b ^ a ^ k2 with 2 <= k1 < k2.

It's not for any AI company to teach AI. :grinning_face_with_smiling_eyes: Neither it is a homework or something similar. It's just a result of exploration, which I will keep poking periodically with hope of proving it.

[Ilmārs Cīrulis]

Okay, I will do that. Thank you!

[Ilmārs Cīrulis]

Proving conjecture₂, I got this far. This is the only part left.

import Mathlib

theorem conjecture₂.extracted_1_11 {t₁ t₂ t₃ a d : ℕ}
    (h₈ : 1 ≤ d) (ht₁ : 2 ≤ t₁) (ht₂ : 2 ≤ t₂) (ht₃ : 1 ≤ t₃)
    (h : d + t₂ ^ (t₁ * t₃ + 1) = t₃ + a ^ (t₁ * d + 1) :
    a = t₂ ∧ d = t₃ := by
  sorry

Looks very annoying (at least for me). I checked it using computer, so far looks good, but haven't proved it yet. Will try again later.

[Kevin Buzzard]

Why do you think this is true? This just says "the only solutions to a random exponential Diophantine equation are the ones I can think of". Fermat's Last Theorem says exactly the same kind of thing, and there are also plenty of random Diophantine equations which do have surprising large sporadic solutions (for example there are nontrivial solutions to $a^4+b^4+c^4=d^4$ in positive integers even though a naive computer search will never find them). This is also not really anything to do with Lean. This is a (possibly straightforward but possibly highly nontrivially true and possibly false but with nontrivial techniques needed to find a counterexample) number theory question.

[Ilmārs Cīrulis]

This is also not really anything to do with Lean.

Fair point.

[Snir Broshi]

Kevin Buzzard said:

(for example there are nontrivial solutions to $a^4+b^4+c^4=d^4$ in positive integers even though a naive computer search will never find them)

btw such a solution is in Mathlib counterexamples
They were found with a computer search but indeed not the naive one, there were some algebraic manipulations first