Prime Constellations: Logic and Verification

This repository contains a formal verification and computational search for $k$-twin prime constellations using the Lean 4 interactive theorem prover and LaTeX for algorithmic specification.

🧮 Mathematical Background

A prime constellation is defined by a base prime $p$ and a set of offsets $\mathcal{O} = {o_1, o_2, \dots, o_k}$. This project focuses on:

• Twin Primes: ${0, 2}$
• Prime Triplets: ${0, 2, 6}$ and ${0, 4, 6}$
• Prime Quadruplets: ${0, 2, 6, 8}$

The "Forbidden" Triplet

The constellation ${0, 2, 4}$ is proved to be impossible for $p > 3$ via modular arithmetic: $$p \equiv 1 \pmod 3 \implies p+2 \equiv 0 \pmod 3$$ $$p \equiv 2 \pmod 3 \implies p+4 \equiv 0 \pmod 3$$

💻 Lean 4 Implementation

The core logic utilizes a Decidable instance for $k$-twin properties to allow for direct computation via the kernel.

def is_k_twin_prime (offsets : List ℕ) (p : ℕ) : Prop :=
  offsets.all (fun s => Nat.Prime (p + s))

Verified Results ()

• Triplets [0, 2, 6]: [5, 11, 17, 41]
• Quadruplets [0, 2, 6, 8]: [5, 11]

📜 Formally Documented Algorithm

The search procedure is specified using algorithm2e logic:

1. Iterate through the search space.
2. For each , verify Nat.Prime (p + s).
3. Return if the conjunction holds.

🛠 Usage

Ensure you have Lean 4 and lake installed.

git clone [https://github.com/your-username/primes.git](https://github.com/your-username/primes.git)
cd primes
lake env lean TwinPrimes.lean

---

2. Update your GitHub Repository

Since you’ve already pushed the previous version, simply overwrite the file and push the update:

# Overwrite the README.md with the content above
git add README.md
git commit -m "Refactor: README focused on Lean and Math logic"
git push origin main

3. Final Technical Check

• Git Log: Your commit history now shows a clean transition from "Development" to "Technical Documentation."
• Verification: Running lake env lean TwinPrimes.lean one last time confirms that your output [5, 11, 17, 41] exactly matches what you've documented in your README.