bibkey: oeis2026a394694 authors: OEIS Foundation Inc. year: 2026 title: OEIS A394694 doi: null url: https://oeis.org/A394694 claim: A394694’s conjectural count is complementary to A033831, whose divisor-count formula was published in OEIS in 2023; this attempt is downgraded to a literature note. strata_touched: [] license: citation-only triage: anchor

OEIS A394694

The first-tier 2026 OEIS conjecture reads verbatim:

Conjecturally: a(n) = A000005(n-1)/2 + e(n), where e(n) = 1/2 if n-1 is a perfect square, 1 if n-1 is pronic, and 0 otherwise.

The counted triangle is A081493. Its formula, attributed to David Wasserman on June 3, 2004, is T(i,j) = i + (i-1)*(j-1), with 1 <= j <= i. For n >= 2, put m = n-1: occurrences correspond to positive factor pairs d*b = m with b <= d+1. The index n = 1 must be handled separately.

Preregistered Proof Obligation

Before implementation, the proposed escape witness is the small-divisor classification: if d divides positive m and d*d < m, then m <= d*(d+1) holds exactly when m = d*(d+1). Such a divisor is unique and is the integer square root of m. This is to be used on the active proof path in the divisor count, then transported to the bounded triangle count. The bind-only attempt must precede construction of a module. This records the proposal at checkpoint 0d48ae94c1, not an observed witness in an elaborated proof. The literature finding below retires implementation for this attempt under the user’s explicit downgrade condition.

Earlier Published Formula

Direct reading of A033831 on September 9, 2026 (revision 30, July 2, 2025) found the following definition:

Number of numbers d dividing n such that d >= 3 and n/d <= d-2.

Its formula field explicitly states:

a(n) = floor(A000005(n)/2) - 1 if n is oblong (A002378); and floor(A000005(n)/2) otherwise. - Max Alekseyev, Oct 09 2023

This is an earlier OEIS publication of the complementary formula, not a located journal proof or a Lean declaration. The following elementary identification is an informal argument by this worker.

For positive m, let A(m) count the positive factor pairs d*b=m with b <= d+1. A pair excluded from A(m) has b >= d+2. Exchanging the factors maps it bijectively to a divisor e=b with e >= 3 and m/e=d <= e-2, exactly the defining set for B(m)=A033831(m). Positivity makes division exact and excludes a zero factor. Thus A(m)+B(m)=tau(m).

Put P(m)=[m is pronic] and S(m)=[m is a square]. The published formula is B(m)=floor(tau(m)/2)-P(m), whence A(m)=ceil(tau(m)/2)+P(m). Complementary divisor pairing gives odd tau(m) exactly when m is a square, so 2*A(m)=tau(m)+S(m)+2*P(m), the requested identity.

The triangle identification preserves its row length: for 1 <= j <= i, T(i,j)=1+(i-1)*j; set d=i-1, b=j. For n>=2 both factors are positive, and the inverse is (i,j)=(d+1,b). An explicit finite counting box is 1 <= i <= n, 1 <= j <= i, since T(i,j) >= i. When n=1, only (1,1) occurs. For m>0, a pronic m=k*(k+1) has k>0 and k*k < m < (k+1)*(k+1), so k=floor(sqrt(m)); this also shows that a positive pronic is not a square. The square-root indicators in the brief are faithful.

The user requires note/cover-only output when a published explicit statement is found. This complementary formula meets that condition via the displayed bijection and classical parity fact. The attempt therefore produces this note only. No Lean module, Scribe resolution claim, frozen entry, or atom coverage is created. Literature equivalence does not certify bind-only in the pinned formal library.

Search And Environment Log

• Source base: b2f83a3306b7aed53f1c2d2a3980a9855d3331af.
• First command: make lean-cache-ensure. Receipt: status=present, method=none, project_olean_state=warm, mathlib_olean_state=warm. Missing Mathlib olean files: 0. No cold bare Lake invocation occurred.
• Direct HTTP reading on September 9, 2026 of the OEIS text endpoints for A394694 and A081493 succeeded. The former is revision 29, April 14, 2026; it still prints the conjecture. The latter is revision 20, March 31, 2025.
• rg -n 'A394694|A081493' Meta Library Problems Blueprint D5 before adding this note returned zero matches. No atom identifier was supplied in this OEIS brief, so make show-atom is not applicable; the OEIS entry is the documentary source, with no atom coverage claimed.
• Authenticated GitHub code search A394694 language:Lean returned total_count=0. This is a bounded ecosystem search, not exhaustive.
• The same GitHub search for A081493 language:Lean returned total_count=0.
• All 30 direct Lean files in D5/S3/Factorization/ were read (5,466 lines). TwoDenseDivisorBlocksPalindrome uses complementary divisors for row sums and reversal, but does not state this square/pronic count. Child domains were not exhaustively read. D5/S1/Digit/CompositeGasPronic.lean was also read and concerns quadratic roots, not this divisor count.
• rg -n '\b(A394694|A081493)\b' D5 --glob '*.lean' found zero matches. Positive control with the same word-boundary syntax, rg -n '\bdivisors\b' D5/S3/Factorization/TwoDenseDivisorBlocksPalindrome.lean, found four lines (65, 70, 71, 91). The broader divisor/pronic searches and full directory reading above address the limitation of same-name searches.
• Pinned Mathlib searches for divisors.*sqrt|sqrt.*divisors|card_divisors|pronic in NumberTheory and Data/Nat found no matching square/pronic count theorem. Nat.card_divisors in ArithmeticFunction/Misc expresses the exponent product; Nat.card_divisors_le_self is only a bound.
• The brief names tools/scripts/agent/bindonly-probe.sh, but that path is absent at the fixed base. The orchestrator’s status=open seconds=50 receipt is user-supplied evidence, not a locally reproduced run.
• The pinned Mathlib declaration Nat.image_div_divisors_eq_divisors states image (fun x => n / x) n.divisors = n.divisors. Nat.sum_div_divisors supplies the corresponding sum reindexing.
• A local scratch file importing only Mathlib successfully elaborated the exact requested statement. Pure exact? failed to close it. Instantiating Nat.image_div_divisors_eq_divisors and Nat.card_divisors_le_self, followed by simp_all; omega, also failed to close it. Lean exited 1 with precisely these two proof errors. An earlier normalization probe also remained open; its failed tactic layout did not provide an independent exact? result. These bounded failures do not prove that every library composition fails.

Evidence

This worker independently recomputed the following on September 9, 2026 using Python integer arithmetic, math.isqrt, and the actual triangular range 1 <= j <= i <= n. The script retrieves the OEIS text DATA fields through curl; an initial urllib request received HTTP 403, while the curl-backed rerun succeeded. All listed comparisons had zero mismatches.

The required pronic witness is n=7, m=6: the actual pairs are (3,3),(4,2),(7,1), the divisor-filter count is 3, and the closed formula is 4/2+0+1=3; its doubled sides are both 6. The square but nonpronic witness is n=5, m=4: pairs (3,2),(5,1), count 2, and 3/2+1/2+0=2; its doubled sides are both 4. Further checks give sqrt(12)=3 with pronic indicator 1 and sqrt(8)=2 with pronic indicator 0.

The excluded boundary is m=0: the divisor set is empty while both indicators are 1, so the doubled core has sides 0 and 3. In contrast, the separate triangle count at n=1 is 1, with sole pair (1,1). These are finite experimental checks, not a kernel proof of the unbounded statement. The earlier orchestrator ranges in the brief remain attributed to the orchestrator rather than retroactively relabelled worker results.

Formal Admission Assessment

There are no new public Lean theorems: the per-public-theorem report is an empty list. Direct frozen dependencies are none; no GID or statement ID is claimed as a dependency or coverage target. No admission basis is sought. The target remains unclosed by the bounded local bind-only attempts, and no content classification is certified by a finished proof.

For the preregistered candidate witness, clause 3.2’s four checks have the following limits: (i) no completed proof supplies an elaborated transitive constant closure; (ii) the inspected interfaces supply reindexing and a bound, not the small-divisor classification, but the search is not exhaustive; (iii) classifying one small divisor is distinct from the final cardinality identity; (iv) no completed proof supplies an active dependency path. Thus the proposed witness does not establish content admission for this attempt.

ASSUMED-UNVERIFIED

The orchestrator explicitly performed no targeted literature search before dispatch. Pairing complementary divisors is classical. First publication priority is not established; the explicit 2023 OEIS formula above is now known prior literature. This note does not call the requested identity a new mathematical theorem. The bounded searches do not exclude unindexed or private proofs. This worker has not kernel-proved the target or the complement bridge, and claims neither formal completion nor an exhaustive impossibility of bind-only closure. No connection with a larger conjecture is claimed. The OEIS-to-definition identification is documentary.

Provenance

One Codex implementation worker, using the lean4 skill, performs the local work. The informal reduction and proposed witness were supplied by the user. The orchestrator’s numerical readings are attributed to the brief; the worker’s independent recomputation is separately recorded above. No independent agent review has been performed by this worker.

Validation

The local gates ran in order and exited 0: make lean LAKE_JOBS=3 (12,753 build jobs), make lean-report, then make emit (zero changed Blueprints and no tracked projection changes). No OpenProblemResolutionClaim exists for this note, so no ledger-align --add step applies. git diff --check also passed. These repository checks do not turn the informal argument into a Lean proof.