Density one for lattice point visibility along polynomials with at least two distinct roots
Abraham Lobsenz
math.NT
Sep 5, 2026 · v2
TL;DR
The main density theorem is fully formalized in Lean 4 with Mathlib, with no admitted proofs, in a public GitHub repository.
Abstract
We prove that every nonzero integer polynomial with at least two distinct complex roots has lattice point visibility density one, resolving the generalized form of the Visibility Density Conjecture for nonzero polynomials. This extends the origin-passing case established by Chaubey, Pandey, and Regavim. Visibility is taken along the curves $y=tF(x)$ with rational $t$, with a point visible if no positive lattice point on the same curve has a smaller horizontal coordinate. The proof uses a greatest common divisor cutoff to reduce the problem to finitely many equations of the form $F(b)=qF(a)$, with $0<q<1$; for each equation, the positive integers $a$ admitting a positive integer solution $b<a$ form a set of density zero. This elementary argument removes the proper-power hypothesis of earlier work without requiring estimates uniform in the ratio.
Problem
The Visibility Density Conjecture asks whether lattice points visible along polynomial curves y=tF(x), with rational t, have density one. Earlier work handled origin-passing polynomials and proper powers F=f^m.
Approach
A GCD cutoff shows that pairs with large gcd(|F(a)|,h) have small density. This reduces invisibility to finitely many equations F(b)=qF(a) with 0<q<1. An elementary argument, splitting into cases where q^{1/d} is irrational or rational, shows each such equation has a solution set of density zero. The full proof is formalized in Lean 4.28.0 with Mathlib, with AI assistance acknowledged.
Results
Every nonzero integer polynomial with at least two distinct complex roots has visibility density one, which resolves the generalized conjecture for nonzero F. The Lean formalization is complete and contains no sorries or extra axioms.
