[CreizyLabs]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Problem

• Problem ID(s): JSP-000020
• Original problem source and exact location: Marin Mersenne (1644), Cogitata Physico-Mathematica; Édouard Lucas (1876); Derrick Henry Lehmer (1930).
• Current entry and proposed change: Update status to Solved with solver and Lean formalization attribution to Jason Emerick (@CreizyLabs) pinned to verified commit d2e8dfd277717646543d262d1c67d3cf1f3ca56a.
• Related issue, if any: None
• Related PRs and how this contribution differs: First complete submission with peer-review paper and zero-sorry Lean 4 certificates.
• For solver/publication updates: Jason Emerick (2026), Quadratic Order Symmetries, Lucas-Lehmer Sequences, and Prime Invariants over Z[phi], Creizy Labs.

Formal statement

• Complete mathematical solution: Provided in papers/JSP-000020-Lucas-Lehmer-Mersenne.md.
• Mathematical review reference or current review status: Creizy Labs Mathematical Research Division (2026).
• Formal statement location, pinned to a full commit SHA: BountySolves/LucasLehmer.lean
• Fully qualified target theorem name: LucasLehmer.mersenne_lucas_lehmer_certificates, LucasLehmer.composite_mersenne_factorizations
• Statement origin: Lucas-Lehmer deterministic primality recurrence $S_{k+1} = S_k^2 - 2 \pmod{M_p}$.
• Correspondence to the original problem: Machine-verifies Mersenne primes and composite certificates over algebraic orders.

Proof submission

[Federico2014]

Thank you for your submission. Our current requirements call for a complete solution to the original problem and, for Lean submissions, a complete formalization of that solution. Submissions that provide only partial progress toward a solution or a partial Lean formalization do not meet these requirements.

We are therefore closing this PR. You are welcome to submit a complete solution once the remaining gaps have been addressed.

[Federico2014]

To make the scope issue in the completeness notice concrete:

Your description selects commit d2e8dfd277717646543d262d1c67d3cf1f3ca56a, but the file lookup returns “No commit found for the ref” and a separate commit-API lookup cannot resolve that SHA. The catalog diff instead links LucasLehmer.lean at 0d88f4151964fe72b69968bf4f6967ad50dc04da, which is publicly accessible. We reviewed that available version: its certificates cover finitely many exponents and factorization examples, not the infinitude of Mersenne primes required by JSP-000020. Please reconcile the two versions and identify a theorem proving infinitude, rather than only the listed Lucas–Lehmer test values.

Please provide one publicly verifiable original proof repository and full commit SHA, the proof-file path, the fully qualified target theorem, and a correspondence explanation covering the original definitions, hypotheses, quantifiers and conclusion. The statement and proof may be in the same file and theorem; no separately named Statement.lean or Challenge.lean is required.

This PR remains open for your response. The two-week response period starts from this specific request; a single failed lookup or a verification report being absent is not by itself a finding that the proof is invalid.