[cosmos2explorer]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Problem

• Problem ID(s): JSP-000301
• Original problem source and exact location (page, section or problem number):
  Golomb's question as recorded in the catalog entry
  problems/catalog-0301-0400.md#JSP-000301
• Current entry and proposed change: Lean proof field changes from No to
  Yes — [Lean source](https://github.com/cosmos2explorer/JSP-000301/blob/f4789f1f976998575463d3c995d4e094dddc9ecb/JSP000301.lean);
  formalization contributor @cosmos2explorer. No other fields changed.
• Related issue, if any: none
• Related PRs and how this contribution differs:
  Open Lean PRs for the same problem include JSP-000301: Lean formalization of Golomb's counterexample (consecutive powerful numbers) #4872 (universe2explorer),
  JSP-000301: complete Lean disproof and proof of the least counterexample #4698 (DF-dan), docs(problems): add Lean 4 formalization for JSP-000301 #692 (Drag0ndddd1118), JSP-000301: Lean formalization - consecutive powerful numbers counterexample (Golomb 1970) #4704 (kunjunsong-code),
  Lean formalizations: JSP-000301 and JSP-000307 #1084 (qzxuwenlong), Lean formalizations for JSP-000122, JSP-000301, JSP-000307, JSP-000554, JSP-000598, JSP-000945, JSP-001010 #4862 (aznikline). I reviewed the five most recent;
  all are mathematically correct formalizations as far as I could verify.
  Per the award process, the earliest verified commit holds priority — I
  understand this submission is later than JSP-000301: Lean formalization of Golomb's counterexample (consecutive powerful numbers) #4872 and do not claim priority
  over it. This PR offers an independent core-only (no-Mathlib) formalization
  with full reproduction evidence and a disclosed axiom audit, so maintainers
  have a second verified source for the same result.

Formal statement

• Complete mathematical solution (provided earlier or in this PR):
  The solution is already in the catalog entry: Solomon W. Golomb's 1970
  counterexample — 12167 = 23³ and 12168 = 2³ · 3² · 13² are consecutive
  powerful numbers, neither a perfect square (both strictly between
  110² = 12100 and 111² = 12321). [Go70] Powerful numbers, Amer. Math.
  Monthly 77(8) (1970), 848–852, https://doi.org/10.2307/2317020.
  The catalog's Review notes (2026-09-13) record the disproof explicitly.
• Mathematical review reference or current review status: catalog entry
  already records Current status: Solved with Golomb as proof contributor;
  review notes confirm the disproof.
• Formal statement location, pinned to a full commit SHA:
  https://github.com/cosmos2explorer/JSP-000301/blob/f4789f1f976998575463d3c995d4e094dddc9ecb/JSP000301.lean
• Fully qualified target theorem name: jsp000301
• Statement origin: proposed formal statement (no maintainer-approved Lean
  statement exists for JSP-000301; catalog shows Lean proof: No).
• Correspondence to the original problem:
  The original question: "If two consecutive positive integers are powerful,
  must at least one be a perfect square?" The formal theorem is
  ∃ n : Nat, 0 < n ∧ Powerful' n ∧ Powerful' (n + 1) ∧ ¬ IsSquare' n ∧ ¬ IsSquare' (n + 1),
  i.e. there exist consecutive positive integers, both powerful, neither a
  square — the exact negation of the question, hence a disproof.
  Definitions used:
  • Powerful' n := ∀ p : Nat, Prime' p → p ∣ n → p ^ 2 ∣ n
    (every prime divisor occurs with exponent ≥ 2 — the standard definition
    of a powerful number),
  • IsSquare' n := ∃ r : Fin (n + 1), n = r.val * r.val
    (n equals r² for some r — equivalent to the standard "n is a square"
    since any square root of n is < n+1),
  • Prime' p := 2 ≤ p ∧ ∀ m : Fin (p + 1), m.val ∣ p → m.val = 1 ∨ m.val = p
    (bounded-decidable primality, equivalent to standard primality).
    The witness is n = 12167: powerful_12167 (12167 = 23³),
    powerful_12168 (12168 = 2³·3²·13²), not_isSquare_12167,
    not_isSquare_12168 (both between 110² and 111²).

Proof submission

[
  {
    "repository": "https://github.com/cosmos2explorer/JSP-000301",
    "branch": "main",
    "commit": "f4789f1f976998575463d3c995d4e094dddc9ecb"
  }
]

• Proof file at the selected commit and fully qualified theorem name:
  JSP000301.lean (repository root), theorem jsp000301, with supporting
  lemmas powerful_12167, powerful_12168, not_isSquare_12167,
  not_isSquare_12168.
• How the proof establishes the formal statement above:
  Divisor-classification lemmas (divs_12167, divs_12168) enumerate every
  divisor below the bound via native_decide, establishing the prime-divisor
  sets {23} and {2, 3, 13}; each prime's square is shown to divide the
  number, giving powerfulness. Non-squareness follows from
  110² < n < 111² via a bounded search (not_isSquare_of_between style
  argument, discharged by native_decide). The main theorem combines the
  four lemmas at n = 12167. No sorry, no admit, no added axioms.

Reproduction

• Exact Lean version and lean-toolchain path: Lean 4.34.1
  (leanprover/lean4:v4.34.1), lean-toolchain at repository root.
• Pinned dependencies (including mathlib, if used) and manifest path:
  none — core-only proof, no Mathlib, no external dependencies.
  lakefile.toml at repository root declares the JSP000301 library.
• Build instructions pinned to the selected commit: see repository README.md.
• Commands for setup, clean build and checking each target theorem:

  lean JSP000301.lean

  (single-file check; compiles cleanly with exit code 0, no errors).
• Axiom audit command and output for each target:

  lean JSP000301.lean   # file ends with #print axioms lines

  Actual output (Lean 4.34.1, verified 2026-10-09):

  'jsp000301' depends on axioms: [propext, Quot.sound,
    divs_12167._native.native_decide.ax_1_1,
    divs_12168._native.native_decide.ax_1_1,
    not_isSquare_12167._native.native_decide.ax_1_1,
    not_isSquare_12168._native.native_decide.ax_1_1]
  

  propext and Quot.sound are standard Lean axioms; the four
  native_decide axioms are Lean-generated kernel certificates for the
  decidable computations (not sorryAx).

Pre-submission Lean verification (optional)

• Method/tool and version: direct Lean 4.34.1 kernel check
  (lean JSP000301.lean), plus independent Python re-verification of the
  factorizations and the 110² < n < 111² bounds.
• Checked repository and full commit SHA; identify any difference from the
  submitted version: same commit as submitted (f4789f1f976998575463d3c995d4e094dddc9ecb).
• Verification date, actual conclusion and limitations: 2026-10-09 —
  compiles with exit 0, no errors, no sorry/admit; axiom audit as above.
  Limitation: verification is of the formal statement's proof, not of the
  statement-to-English correspondence, which is argued in "Correspondence"
  above for maintainer review.
• Summary: statement matches the original yes/no question's negation;
  coverage is the full disproof (both powerfulness and non-squareness for
  both numbers); trust dependencies are the Lean 4.34.1 kernel plus the
  disclosed native_decide certificates.
• Report in this PR or external report/log/evidence links: repository
  README.md contains the build and axiom-audit record.

Attribution

• Mathematical solver(s) and contribution: Solomon W. Golomb — original
  counterexample (12167, 12168), [Go70] 1970; already credited in the
  catalog entry. This PR claims no mathematical discovery.
• Lean formalization author(s) and contribution: @cosmos2explorer —
  core-only Lean 4 formalization of the disproof (statement, definitions,
  all lemmas, main theorem).
• Independent verifier(s), if any: none.
• Public authorship evidence: the proof repository is owned by the
  submitting account (cosmos2explorer); the PR is opened from that account's
  fork. The formalization was produced for this submission; commit history
  in the proof repository documents authorship.

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.