An Effective Method for Solving a Class of Transcendental Diophantine Equations
Zeyu Cai
TL;DR
The paper tackles the Type-I transcendental Diophantine equation $a^x+b=c^y$ by developing an effective, constructive algorithm that first eliminates trivial non-coprime configurations and then applies modular-exclusion with a priority-queue of prime-power moduli. It combines an initial bounding step, a cyclic-group solvability test, and a search for magic primes to derive contradictions, supported by a heuristic termination framework and Lean-based semi-formal proofs. Empirical results for parameters with $a,b,c\le 250$ show that the maximum number of solutions is $2$, and only $10$ equations achieve this bound, reinforcing a conjecture that all instances have at most two solutions. The work provides an open-source C implementation, symmetry-aware handling of $a$ and $c$, and a pathway to rigorous verifications via external validation, contributing a practical methodology for finite-solution guarantees conditioned on conjectural termination. This has potential implications for understanding finiteness phenomena implied by the ABC conjecture in specific Diophantine settings and offers a framework for automated, verifiable solution completeness proofs.
Abstract
This paper investigates the exponential Diophantine equation of the form $a^x+b=c^y$, where $a, b, c$ are given positive integers with $a,c \ge 2$, and $x,y$ are positive integer unknowns. We define this form as a "Type-I transcendental diophantine equation." A general solution to this problem remains an open question; however, the ABC conjecture implies that the number of solutions for any such equation is finite. This work introduces and implements an effective algorithm designed to solve these equations. The method first computes a strict upper bound for potential solutions given the parameters $(a, b, c)$ and then identifies all solutions via finite enumeration. While the universal termination of this algorithm is not theoretically guaranteed, its heuristic-based design has proven effective and reliable in large-scale numerical experiments. Crucially, for each instance it successfully solves, the algorithm is capable of generating a rigorous mathematical proof of the solution's completeness.