[shimiei]

Submission type

• Mathematical solver information
• Lean proof or formalization author information

Lean formalization only. The mathematical solution is not claimed by this submission: it is
Solomon W. Golomb's published counterexample, which the catalogue already credits. This PR
records the complete Lean formalization of that solution and links its published evidence.

Problem

• Problem ID(s): JSP-000301
• Original problem source and exact location: problems/catalog-0301-0400.md, entry
  JSP-000301 (#JSP-000301), field Problem description — "If two consecutive positive
  integers are powerful, must at least one be a perfect square?" The record's own origin
  field states: "Unspecified; the original proposal date of this yes/no question is
  unverified."
  https://github.com/TheJustinSunPrize/awards/blob/main/problems/catalog-0301-0400.md#JSP-000301
• Current entry and proposed change: Lean proof is currently No; the index row
  (problems/README.md) shows Solved | No | No | Unavailable | Unavailable. Proposed:
  Lean proof → Yes — [Lean source](https://github.com/shimiei/jsp-000301-lean/blob/531a6e31e098bdb8691bda3a1b829387d9105e0a/Jsp000301.lean) with
  target theorems Jsp000301.golomb_counterexample and Jsp000301.answer_is_no and
  formalization contributor YEUNG CHUN HEI; plus one new Attribution basis row recording the
  formalization source. In the index, only the Lean proof column changes to Yes.
  Current status / Proof contributors: (Golomb), Eligible to claim and both claim-status
  columns are deliberately untouched, because they are maintainer-reconciled fields. The diff
  in this PR totals 2 files changed, 3 insertions(+), 2 deletions(-).
• Related issue, if any: None at the time of opening. A claim issue
  ([Award claim] JSP-000301) will be opened only after this PR merges, as
  docs/award-process.md requires.
• Related PRs and how this contribution differs, including any issue found in an existing
  submission and supporting evidence (optional): this is a supplementary re-formalization,
  not a first submission, and no priority of any kind is claimed. A search of
  https://github.com/TheJustinSunPrize/awards/pulls?q=is%3Apr+JSP-000301 finds many earlier
  JSP-000301 submissions; the earliest Lean formalizations date from 2026-09-16/17 (for example
  JSP-000301: Lean proof of an infinite family of nonsquare powerful pairs #412 and JSP-000301: complete Lean disproof and general-seed quantitative construction #587), and JSP-000301: record Lean formalization (scks1/jsp-000301-formalization) #5134 was opened on 2026-10-25. Nothing here disputes them and nothing here
  is offered as a replacement claim. What this commit adds, all machine-checked at
  531a6e31e098bdb8691bda3a1b829387d9105e0a: (i) answer_is_no_pos carries the catalogue sentence's literal 0 < a,
  0 < b premises instead of leaving positivity to be discharged by the witness itself;
  (ii) answer_is_no_unordered reads "consecutive" symmetrically (b = a + 1 or a = b + 1),
  so no ordering convention is left open; (iii) a ## Statement bridge section of five
  kernel-checked example terms ties each literal reading of the English sentence to the
  theorems, including a proof that the unordered form follows from the ordered one; (iv) the
  development is Classical.choice-free — every audited constant depends only on
  [propext, Quot.sound], which is strictly weaker than the axiom profile of the earlier
  formalizations. If a maintainer prefers one canonical formalization per problem, this PR
  should be compared against the earlier ones rather than treated as superseding them.
• For solver/publication updates: public proof or publication, relevant theorem/pages,
  version or date: Solomon W. Golomb, "Powerful numbers", American Mathematical Monthly
  77(8) (1970), 848–852, https://doi.org/10.2307/2317020. The counterexample is the
  consecutive pair 12167 = 23³ and 12168 = 2³·3²·13², neither a square. The catalogue's
  review note of 2026-09-13 already records this disproof; the entry's publication fields
  additionally cite [Wa76] (Fibonacci Quart. 1976, 111–116) and [Gu04] (Guy, 2004). This PR
  does not change any of those fields.

Formal statement

For Lean contributions only. Repeat the theorem details for each problem.

• Complete mathematical solution (provided earlier or in this PR): public proof or
  publication, relevant theorem/pages, version or date: provided earlier — Golomb, "Powerful
  numbers", Amer. Math. Monthly 77(8) (1970), 848–852,
  https://doi.org/10.2307/2317020. The counterexample pair used here, 12167 = 23³ and
  12168 = 2³·3²·13², is the one also recorded in the catalogue review note of 2026-09-13.

• Mathematical review reference or current review status: the problem-bank record
  JSP-000301 is marked Solved with Proof contributors: Solomon W. Golomb and carries a
  dated review note (2026-09-13) that reproduces the disproof and states that both numbers lie
  strictly between 110² = 12100 and 111² = 12321. This formalization follows that reviewed
  mathematical solution; no new mathematical review is requested in this PR.

• Formal statement location, pinned to a full commit SHA:
  https://github.com/shimiei/jsp-000301-lean/blob/531a6e31e098bdb8691bda3a1b829387d9105e0a/Jsp000301.lean#L321-L400 (definitions at lines 26–33; the
  four statements are at lines 321–354 and the ## Statement bridge section at lines 356–400).

• Fully qualified target theorem name: Jsp000301.golomb_counterexample (the witness form) and
  Jsp000301.answer_is_no (the negated universal form that answers the question).

• Statement origin (maintainer-approved reference and version, or proposed statement requiring
  review): proposed statement, requiring review. No maintainer-approved formal statement
  exists for JSP-000301 (the record shows Lean proof: No); the statement below is a direct
  transcription of the catalogue sentence into Nat, and is offered for review as such.

• Correspondence to the original problem: definitions, assumptions, quantifiers, conclusion
  and all required cases; explain any differences from an approved statement:

  def Prime (n : Nat) : Prop := 2 ≤ n ∧ ∀ m : Nat, m ∣ n → m = 1 ∨ m = n
  def Powerful (n : Nat) : Prop := ∀ p : Nat, Prime p → p ∣ n → p * p ∣ n
  def IsSquare (n : Nat) : Prop := ∃ m : Nat, n = m ^ 2
  
  theorem golomb_counterexample :
      ∃ a b : Nat, b = a + 1 ∧ Powerful a ∧ Powerful b ∧ ¬ IsSquare a ∧ ¬ IsSquare b
  
  theorem answer_is_no :
      ¬ (∀ a b : Nat, b = a + 1 → Powerful a → Powerful b → IsSquare a ∨ IsSquare b)

  • Domain: "positive integers" → Nat. The catalogue question quantifies over positive
    integers only, so no sign case or Int subtraction appears.
  • "consecutive" → b = a + 1, instantiated at a = 12167, b = 12168; the positivity
    condition is met by the witness, not assumed.
  • "powerful" → "every prime factor occurs with exponent at least two", which for a prime
    p is exactly p ^ 2 ∣ n; hence ∀ p, Prime p → p ∣ n → p * p ∣ n. All primes are
    quantified over, not a supplied factorisation, so the property cannot be satisfied by
    choosing convenient factors.
  • "perfect square" → ∃ m, n = m ^ 2; with n m : Nat this is exactly the intended set.
  • The question is the universal statement ∀ a b, b = a + 1 → Powerful a → Powerful b → IsSquare a ∨ IsSquare b; answer_is_no is its negation, proved by instantiating the
    universal statement at the witness and eliminating both disjuncts. Both cases are covered
    (not_square_12167, not_square_12168); no case is assumed away.
  • Difference from a literal transcription (the only one): Prime is defined in the
    file. Core Lean 4.35 without Mathlib has no Nat.Prime — verified on the pinned
    toolchain: #check @Nat.Prime gives
    error(lean.unknownIdentifier): Unknown constant 'Nat.Prime'. The definition used is the
    standard one (n ≥ 2, divisors only 1 and n), so Powerful ranges over genuine
    primes; it is not a computable stand-in and not restricted to a bounded search range.
  • Scope limits, stated explicitly: this formalizes the yes/no question and nothing else. It
    does not formalize the counting question of 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, nor runs of three or more
    consecutive powerful numbers (the separate entry JSP-000300).

Proof submission

For Lean contributions only. Use the original repository containing your contribution, owned
by your submitting account or an organization.

[
  {
    "repository": "https://github.com/shimiei/jsp-000301-lean",
    "branch": "main",
    "commit": "531a6e31e098bdb8691bda3a1b829387d9105e0a"
  }
]

• Proof file at the selected commit and fully qualified theorem name:
  Jsp000301.lean (repository root) at commit 531a6e31e098bdb8691bda3a1b829387d9105e0a;
  theorems Jsp000301.golomb_counterexample and Jsp000301.answer_is_no. The selected commit
  contains that file in branch main.
• How the proof establishes the formal statement above, including any separate verification
  entry: the repository root is a Lake project whose only target is the library Jsp000301
  built from that one file. powerful_12167 proves 12167 = 23 ^ 3 has only the prime
  divisor 23 with 23 * 23 ∣ 12167; powerful_12168 proves that the prime divisors of
  12168 = 2 ^ 3 * 3 ^ 2 * 13 ^ 2 are exactly 2, 3, 13 and that each square divides it;
  not_square_12167 and not_square_12168 place both numbers strictly between 110 ^ 2 and
  111 ^ 2 and conclude with monotonicity of multiplication. golomb_counterexample packages
  those four facts with b = a + 1, and answer_is_no derives the negated universal statement
  from it. The separate verification entry is verify.ps1, which deletes .lake/, rebuilds,
  re-runs the axiom audit and sweeps the sources for unproved-step placeholders and
  compiler-trusting decision procedures; it exits non-zero on any failure. Because core Lean
  has no Bézout or gcd library, Euclid's lemma (Prime.dvd_of_dvd_mul) and the trial-division
  primality criterion are proved inside the file rather than imported, so no unproved number
  theory is assumed.

Reproduction

For Lean contributions only.

• Exact Lean version and lean-toolchain path: leanprover/lean4:v4.35.0, pinned by
  lean-toolchain at the repository root (25 bytes, single line). Reproduced toolchain:
  Lean (version 4.35.0, x86_64-w64-windows-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release),
  Lake version 5.0.0-src+eb6cafb (Lean version 4.35.0).

• Pinned dependencies (including mathlib, if used) and manifest path: none — no Mathlib and no
  other dependency. lake-manifest.json at the root has "packages": []. lakefile.toml
  declares a single lean_lib named Jsp000301 with no require entries.

• Build instructions pinned to the selected commit:
  https://github.com/shimiei/jsp-000301-lean/blob/531a6e31e098bdb8691bda3a1b829387d9105e0a/README.md#build-and-audit.

• Commands for setup, clean build and checking each target theorem; include a separate
  statement-to-proof check if needed:

  # setup: install elan, then
  $env:ELAN_HOME = "$env:USERPROFILE\.elan"
  $env:PATH      = "$env:ELAN_HOME\bin;$env:PATH"
  git clone https://github.com/shimiei/jsp-000301-lean
  Set-Location jsp-000301-lean
  git checkout 531a6e31e098bdb8691bda3a1b829387d9105e0a
  
  # clean build
  Remove-Item .lake -Recurse -Force
  lake build                     # -> "Build completed successfully (3 jobs).", exit 0
  
  # statement + axiom check for all four targets (also printed by the build)
  lake env lean Jsp000301.lean   # runs #check / #print axioms at the end of the file
  
  # full gate: clean build + audit + token sweep, non-zero exit on failure
  pwsh -NoProfile -File .\verify.ps1

  Statement-to-proof check: the file ends with four #check commands
  (golomb_counterexample, answer_is_no, answer_is_no_pos, answer_is_no_unordered) and
  nine #print axioms commands, so a plain lake env lean Jsp000301.lean prints the exact type
  of each target next to its axiom dependencies; a statement change would change the printed
  type.

• Axiom audit command and output for each target (for example,
  #print axioms Fully.Qualified.theoremName):

  > lake env lean Jsp000301.lean
  Jsp000301.golomb_counterexample : ∃ a b,
    b = a + 1 ∧ Jsp000301.Powerful a ∧ Jsp000301.Powerful b ∧ ¬Jsp000301.IsSquare a ∧ ¬Jsp000301.IsSquare b
  Jsp000301.answer_is_no : ¬∀ (a b : Nat),
      b = a + 1 → Jsp000301.Powerful a → Jsp000301.Powerful b → Jsp000301.IsSquare a ∨ Jsp000301.IsSquare b
  Jsp000301.answer_is_no_pos : ¬∀ (a b : Nat),
      0 < a →
        0 < b → b = a + 1 → Jsp000301.Powerful a → Jsp000301.Powerful b → Jsp000301.IsSquare a ∨ Jsp000301.IsSquare b
  Jsp000301.answer_is_no_unordered : ¬∀ (a b : Nat),
      0 < a →
        0 < b →
          b = a + 1 ∨ a = b + 1 →
            Jsp000301.Powerful a → Jsp000301.Powerful b → Jsp000301.IsSquare a ∨ Jsp000301.IsSquare b
  'Jsp000301.golomb_counterexample' depends on axioms: [propext, Quot.sound]
  'Jsp000301.answer_is_no' depends on axioms: [propext, Quot.sound]
  'Jsp000301.answer_is_no_pos' depends on axioms: [propext, Quot.sound]
  'Jsp000301.answer_is_no_unordered' depends on axioms: [propext, Quot.sound]
  'Jsp000301.powerful_12167' depends on axioms: [propext, Quot.sound]
  'Jsp000301.powerful_12168' depends on axioms: [propext, Quot.sound]
  'Jsp000301.not_square_12167' depends on axioms: [propext, Quot.sound]
  'Jsp000301.not_square_12168' depends on axioms: [propext, Quot.sound]
  'Jsp000301.Prime.dvd_of_dvd_mul' depends on axioms: [propext, Quot.sound]
  

  Axioms reported: propext and Quot.sound — both standard, and that is the complete list for
  all nine audited constants. There is no user axiom, no unproved-step axiom and no
  compiler-trusting evaluation axiom, and Classical.choice does not occur in the file at all:
  the least-divisor argument behind Euclid's lemma is constructed explicitly instead of
  classically. decide is applied to numerals only, which the kernel checks by computation.

Pre-submission Lean verification (optional)

• Method/tool and version, if available: manual reproduction on the submission machine — clean
  clone of the selected commit, lake build, lake env lean Jsp000301.lean, plus the
  repository's own verify.ps1 gate (PowerShell 7, Lean 4.35.0, Lake 5.0.0-src+eb6cafb). The
  optional lean-verify skill was not run; this section is a description of what was
  actually done, not a claim of a completed skill run.
• Checked repository and full commit SHA; identify any difference from the submitted version:
  https://github.com/shimiei/jsp-000301-lean at 531a6e31e098bdb8691bda3a1b829387d9105e0a — identical to the submitted version (the same commit was
  cloned fresh and built; nothing was patched afterwards). The proof source
  Jsp000301.lean is byte-identical to the verified development copy (SHA-256
  5f479c7e1186a9908c06e2a32c8a1932bc3ea342aeb9b0babfa829d468b81594).
• Verification date, actual conclusion and limitations: 2026-10-26. Clean clone build:
  exit 0, Build completed successfully (3 jobs); 1.9 s wall clock on a freshly cloned tree,
  while the repository's own logs/build.log records 1.4–1.6 s for the same three-job build on
  the machine that produced it. verify.ps1:
  build exit: 0, audit exit: 0, forbidden hits: 0, unproved axiom: 0,
  RESULT: PASS. Limitations: reproduced on one machine (Windows) by the author; no
  independent third party has checked it; the statement is a proposed transcription, so
  correspondence still needs maintainer review; nothing beyond the yes/no question is covered.
• Summary of statement correspondence, coverage, Lean checks and trust dependencies:
  correspondence is set out field-by-field in the repository README ("Statement and
  faithfulness") and in the Correspondence bullet above; coverage is the full universal
  question plus its negation; Lean checks are the clean build, the printed #check types and
  the #print axioms audit; trust dependencies are the two standard axioms (propext,
  Quot.sound) plus the Lean
  kernel, with no dependency on Mathlib, decide-on-large-terms, or any user axiom.
• Report in this PR or external report/log/evidence links, if available: captured logs in the
  repository — AUDIT.md (verbatim #check / #print axioms capture and timings),
  logs/build.log, logs/axioms.log, all at 531a6e31e098bdb8691bda3a1b829387d9105e0a. No separate report document is
  claimed.

Attribution

• Mathematical solver(s) and contribution, if applicable: Solomon W. Golomb — the 1970
  counterexample and its proof ("Powerful numbers", Amer. Math. Monthly 77(8) (1970),
  848–852). The catalogue already credits him in Current status; this PR does not alter that
  credit and does not claim the result.
• Lean formalization author(s) and contribution, if applicable: YEUNG CHUN HEI
  (@shimiei) — the whole formalization at 531a6e31e098bdb8691bda3a1b829387d9105e0a: the Prime, Powerful and
  IsSquare definitions, the trial-division primality criterion, Euclid's lemma and
  Prime.dvd_of_dvd_pow built from scratch, the four specific primalities, the two
  powerfulness proofs, the two non-square proofs, the four statements, the ## Statement bridge
  section, and verify.ps1
  with its axiom/token gates.
• AI/tooling disclosure: the Lean source was produced with an AI coding agent (DeepSeek Harness,
  a Lean-aware agentic coding tool) working under the submitting account, which directed the
  work, chose the statement reading and reviewed every file. The proof itself is not asserted on
  the agent's authority: it is kernel-checked by Lean 4.35.0 in this repository, and the
  #print axioms output lets a maintainer re-run the same check without trusting either party.
  Toolchain used: leanprover/lean4:v4.35.0, no Mathlib, no automation beyond decide/omega
  on numerals. Disclosed because other submissions to this problem have disclosed AI assistance
  and a reviewer should not have to infer it.
• Independent verifier(s), if any: none. No third party has reviewed the proof; maintainer
  reproduction is requested and expected.
• Public authorship evidence; for an organization repository, link verifiable evidence
  connecting your account to the claimed proof files/theorems: this is a personal repository
  owned by @shimiei (not an organization), created and pushed by that account;
  commit 531a6e31e098bdb8691bda3a1b829387d9105e0a on branch main is the single root
  commit of the repository: it carries the whole formalization and is authored by
  YEUNG CHUN HEI <hayes11424@gmail.com>, the account holder, with no intermediate or
  neutral-author commits in the history (git log --format='%an <%ae>' lists exactly one
  author). The repository contains no third-party proof material: it is a self-contained Lake
  project whose only dependency-free source file is Jsp000301.lean.

Submission checklist

• I changed only the relevant catalog's solver attribution, Lean proof information or
  supporting sources and supplied the applicable evidence. (Two files: one replaced Lean proof row plus one inserted Attribution basis row; one index Lean proof cell. Every
  other field, including Golomb's solver credit and the maintainer-reconciled eligibility and
  claim-status fields, is untouched. The rendered diff in this PR is the complete change.)
• The submitted result fully solves the original problem. Any submitted Lean proof is
  complete at the specified commit, with no unproved-step placeholder, no admit and no added
  unproved assumption replacing proof steps. (verify.ps1 sweep: forbidden hits: 0,
  unproved axiom: 0; axiom audit as quoted above.)
• 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. (Golomb 1970, DOI
  10.2307/2317020; formalization author YEUNG CHUN HEI.)
• 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. (Personal repository; 531a6e31e098bdb8691bda3a1b829387d9105e0a is on main.)
• This PR contains no Lean source files, archives, binaries, vendored dependencies or
  private identity/contact/payment information. (Proof source stays in the external repository;
  the PR edits catalog text only. No identity documents, payment details or private addresses
  are included — those go by email to the official address.)

Request to maintainers

Per CONTRIBUTING.md, Eligible to claim and the two claim-status columns are yours to
reconcile after verification; this PR deliberately leaves them alone. If the proof passes
verification, the record would read Eligible to claim: Yes, and per candidates/README.md
each role would then be Unclaimed until its candidate is published in candidates/. I will
open the [Award claim] JSP-000301 issue and send the identity-verification email only after
this PR merges.