[scks1]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Problem

• Problem ID(s): JSP-000301
• Original problem source and exact location: the JSP catalog entry
  JSP-000301;
  the question is attributed there to Erdős problem [Recipient] JSP-000178: Lean formalization, Erdős 184, the K_{3,n−3} lower bound for decompositions into cycles and edges #365's yes/no question
  (attribution source).
• Current entry and proposed change: the entry records the problem as
  Solved (Golomb's counterexample) with "Lean proof: No". This PR changes
  only the Lean proof field to record the completed formalization
  below, and adds an Attribution basis row. Eligibility fields are
  left for maintainer reconciliation, per CONTRIBUTING.md.
• Related issue, if any: none opened by the submitter. (Open
  [Award claim] JSP-000301 issues by other claimants exist; a claim
  issue from the submitter would follow this PR's merge, per the award
  process.)
• Related PRs and how this contribution differs: many open PRs record
  Lean formalizations for JSP-000301 (e.g. Add Lean formal proof for JSP-000301 (consecutive powerful numbers) #579, docs: record Lean formalization for JSP-000301 #666, JSP-000301: complete Lean proof of the scoped counterexample #740, JSP-000301: record Lean proof #969,
  JSP-000301: record complete Lean formalization (Golomb counterexample 12167/12168) #1959, JSP-000301: record complete Lean 4 formalization of the counterexample pair (12167, 12168) #4983, JSP-000301: record Lean formalization #5117 — this list is not exhaustive). The submitter has
  not audited them and makes no claim about their contents. This
  contribution is an independent formalization with three checkable
  properties: (1) it depends on core Lean only — no Mathlib and no other
  dependencies; (2) its axiom audit (below) reports
  [propext, Quot.sound], a strict subset of the standard axioms; (3)
  the proof repository carries a complete audit record
  (AXIOM-AUDIT.md) and an AI-authorship disclosure
  (formalization.yaml). Priority is for the maintainers to assess from
  the selected commit's public history, per the award process.

Formal statement

• Complete mathematical solution (provided earlier or in this PR):
  Solomon W. Golomb, "Powerful numbers", Amer. Math. Monthly 77(8)
  (1970), 848–852, https://doi.org/10.2307/2317020 — the counterexample
  pair 12167 = 23³ and 12168 = 2³·3²·13². The solution is already
  recorded in the catalog entry itself (Current status: Solved, with
  publication details and the 2026-09-13 source review note verifying
  the factorisations and the non-square bounds).
• Mathematical review reference or current review status: the catalog
  entry's own Review note (Source review 2026-09-13) records the
  disproof and its verification; no separate review of this
  formalization has taken place — maintainer review is requested.
• Formal statement location, pinned to a full commit SHA:
  https://github.com/scks1/jsp-000301-formalization/blob/3fcd19b2c6d7eb3d35611deebf2bd0c8eb9e46f8/Proof.lean
  (definitions at the top of that file; the standalone definitions file
  is
  https://github.com/scks1/jsp-000301-formalization/blob/3fcd19b2c6d7eb3d35611deebf2bd0c8eb9e46f8/Statement.lean)
• Fully qualified target theorem name: jsp_000301_counterexample
  (top-level; no namespace), stating ¬ CatalogQuestion.
• Statement origin: proposed statement, requiring review. No
  maintainer-approved reference statement for JSP-000301 is known to the
  submitter. Definitions are elementary and core-Lean only, because
  Lean core 4.35 has no Nat.Prime: IsPrime p is 2 ≤ p ∧ ∀ q, q ∣ p → q = 1 ∨ q = p; bridges to Mathlib's Nat.Prime / IsSquare are
  noted in the repository but are not part of the proof.
• Correspondence to the original problem: the catalog asks whether,
  for every pair of consecutive positive integers, powerfulness of both
  forces at least one to be a perfect square. CatalogQuestion is
  exactly ∀ n : Nat, Powerful n → Powerful (n + 1) → IsSq n ∨ IsSq (n + 1), and the target theorem is its negation, proved by the
  witness n = 12167. Powerful n is Golomb's definition stated
  divisor-wise — every prime divisor p of n satisfies p * p ∣ n,
  i.e. occurs with exponent at least two (the catalog review note's own
  wording). IsSq n is ∃ r, r * r = n. Quantifiers, conclusion, and
  cases match the catalog question and its recorded resolution; the
  only difference from a Mathlib statement is the elementary primality
  definition above. The scope is the yes/no question only, not the
  separate counting question of Erdős [Recipient] JSP-000178: Lean formalization, Erdős 184, the K_{3,n−3} lower bound for decompositions into cycles and edges #365, matching the catalog
  record's stated scope.

Proof submission

[
  {
    "repository": "https://github.com/scks1/jsp-000301-formalization",
    "branch": "main",
    "commit": "3fcd19b2c6d7eb3d35611deebf2bd0c8eb9e46f8"
  }
]

• Proof file at the selected commit and fully qualified theorem name:
  Proof.lean, theorem jsp_000301_counterexample.
• How the proof establishes the formal statement above: the file proves
  both factorisation identities (kernel decide), both non-square
  facts (12167 and 12168 lie strictly between 110² and 111², by a
  general between-consecutive-squares lemma), and both powerfulness
  facts (a pure-core Euclid lemma forces every prime divisor of 12167
  to be 23 and every prime divisor of 12168 to be 2, 3, or 13; the
  required squares divide by explicit quotients). The main theorem
  assembles these at the witness n = 12167. There is no separate
  verification entry point; the file's final line is the axiom audit
  (below).

Reproduction

• Exact Lean version and lean-toolchain path: Lean 4.35.0
  (leanprover/lean4:v4.35.0); lean-toolchain at the repository root.
• Pinned dependencies (including mathlib, if used) and manifest path:
  none — core Lean only; no Lake project, no manifest.
• Build instructions pinned to the selected commit: clone
  https://github.com/scks1/jsp-000301-formalization and check out
  3fcd19b2c6d7eb3d35611deebf2bd0c8eb9e46f8 (also the content of the
  main branch at submission, apart from a later bookkeeping commit
  that records this SHA in formalization.yaml and does not touch the
  proof files — Proof.lean SHA-256 at the selected commit:
  b2cc0362d39c75af8b84ab9184a0a2db354949130059cfada1caa65942fc5a6d).
• Commands for setup, clean build and checking each target theorem:
  with the pinned toolchain on PATH (elan honours lean-toolchain):
  lean Statement.lean (definitions; exits 0, no output), then
  lean Proof.lean (exits 0 and prints the axiom audit line). No
  separate statement-to-proof check is needed: statement and proof are
  in the same repository and the target theorem is checked by the
  second command.
• Axiom audit command and output for each target:
  #print axioms jsp_000301_counterexample (the final line of
  Proof.lean) →
  'jsp_000301_counterexample' depends on axioms: [propext, Quot.sound]
  No sorryAx; no added axioms; grep -rn "sorry\|admit\|native_decide" --include='*.lean' . at the selected commit returns no matches.

Pre-submission Lean verification (optional)

• Method/tool and version: local Lean kernel (leanprover/lean4
  v4.35.0) as ground truth; corroborating second check with the AXLE
  checker (axiom-axle 1.9.0, verify-proof), which is not kernel-grade.
• Checked repository and full commit SHA: the proof files are
  byte-identical to the selected commit's (Proof.lean SHA-256 above);
  the kernel check was run on those files on 2026-10-24. The AXLE check
  ran on the same Proof.lean together with the prep package's
  standalone statement file (which differs from the repository's
  definitions-only Statement.lean only in carrying a placeholder
  statement of the target theorem); it returned okay = true with no
  failed declarations.
• Verification date, actual conclusion and limitations: 2026-10-24.
  Conclusion: the target theorem compiles clean and depends only on
  [propext, Quot.sound]. Limitations: the self-check was performed by
  the formalization's preparer; statement correspondence was checked by
  the preparer against the catalog entry and its review note.
  Independent verification is the maintainers'.
• Summary of statement correspondence, coverage, Lean checks and trust
  dependencies: correspondence and coverage are as set out under
  "Formal statement" — the whole yes/no question, one theorem, no
  partial cases. Trust dependencies: the Lean kernel only.
• Report in this PR or external report/log/evidence links: full audit
  record in the repository —
  https://github.com/scks1/jsp-000301-formalization/blob/3fcd19b2c6d7eb3d35611deebf2bd0c8eb9e46f8/AXIOM-AUDIT.md

Attribution

• Mathematical solver(s) and contribution: Solomon W. Golomb —
  counterexample disproving the catalog question, [Go70] (1970). No
  solver contribution is claimed by the submitter.
• Lean formalization author(s) and contribution: Simon Koch-Sultan
  (@scks1), repository owner and claimant of record. The formalization
  was prepared by Árbol, an AI agent (Muse, Meta), acting under his
  direction; this is disclosed in the repository (README and
  formalization.yaml), consistent with the Prize rules' equal treatment
  of human, human–AI, and autonomous-AI contributions. Maintainers are
  asked to word the formalization credit as they see fit.
• Independent verifier(s), if any: none (the AXLE check above is a
  tool, listed under verification, not an independent verifier).
• Public authorship evidence: the proof repository is owned by the
  submitting account (@scks1); its public commit history is the
  authorship record (proof commit
  3fcd19b2c6d7eb3d35611deebf2bd0c8eb9e46f8, authored by Simon
  Koch-Sultan under that account). No organisation repository is
  involved, and there is no mismatch between the account, the commit
  author, and the proposed credit beyond the AI-preparation disclosure
  above.

Submission checklist

• I changed only the relevant catalog's solver attribution, Lean proof information or supporting sources and supplied the applicable evidence.
• The submitted result fully solves the original problem. Any submitted Lean proof is complete at the specified commit, with no sorry, admit or added unproved assumptions replacing proof steps.
• For Lean: I have linked the complete mathematical solution and its proof or publication evidence provided earlier, or supplied them in this PR, and identified the mathematical solver and Lean formalization author separately.
• For Lean: I am claiming my own contribution in the original personal or organization repository, with verifiable contribution evidence for an organization repository; the selected commit is in the named branch, and I supplied statement correspondence, reproduction commands and axiom audit results.
• This PR contains no Lean source files, archives, binaries, vendored dependencies or private identity/contact/payment information.