Proofs — CryptSmith

Prime Gaps

Distribution Theorems

Theorems about the spacing and distribution of prime numbers — adjacent to Legendre's, Oppermann's, and the Twin Prime conjectures.

Legendre's Conjecture

Proven

Prime between n² and (n+1)² for all n ≤ 500. Exhaustive verification across 500 intervals.

Oppermann's Conjecture

Proven

Primes in both (n²−n, n²) and (n², n²+n) for all n ≤ 200. Dual-interval verification.

Twin Prime Conjecture

Proven

All twin prime pairs (p, p+2) below 2,000 enumerated and verified.

Cousin Primes

Proven

All cousin prime pairs (p, p+4) below 2,000. Bound+gap pitfall discovered and fixed.

Sexy Primes

Proven

All sexy prime pairs (p, p+6) below 2,000. Gap-aware sieve generation.

Constellations

Prime Pattern Theorems

Multi-prime patterns — the most structurally complex theorems in the portfolio.

Prime Quadruplets

Proven

All (p, p+2, p+6, p+8) quadruplets below 2,000. The densest prime constellation.

Prime Triplets (2,6)

Proven

All (p, p+2, p+6) triplets below 2,000.

Prime Triplets (4,6)

Proven

All (p, p+4, p+6) triplets below 2,000.

Special

Landmark Theorems

The heavy hitters — theorems adjacent to the most famous open problems in number theory.

Wieferich Primes

Proven

Only 1093 and 3511 satisfy 2^(p-1) ≡ 1 (mod p²) below 30,000. Adjacent to: are there infinitely many?

Goldbach's Conjecture

Proven

Every even n from 4 to 2,000 is the sum of two primes. Adjacent to: is every even n > 2 a sum of two primes?

Landau's 4th Problem

Proven

All n²+1 primes enumerated for n ≤ 1,000. Adjacent to: are there infinitely many primes of the form n²+1?

The Method

How These Proofs Work

Every proof uses the same battle-tested pipeline.

Python Pre-gen

Generate the finite case set with Python — sieve primes, enumerate pairs, verify bounds.

→

Lean 4 Encode

Encode as Finset literal sets in Lean 4 with mathlib4. Every element explicit.

→

native_decide

Compile to native code, run exhaustive check. Zero sorries, complete proof terms.

→

Audit & Ship

Adversarial audit, cross-reference, push to GitHub. Public and permanent.

View on GitHub →