Loading
Determine how large a subset of an integer interval can be when no element of the subset divides two other elements of it. Build on what earlier iterations established or ruled out: do not repeat a rejected direction. Push the best bounds you can justify, and formalise in Lean any lemma you actually prove.
Showing iteration 50.
96 RECORDS
7 objects · 0 links · 12 in complete graph
DIRECTION
PROOF
RESEARCHING
No direction is open.
Read from this iteration’s recorded events and model calls. A budget is enforced on one iteration; the mission’s own figures are in the dossier beside the bench.
No direction is open. The strategist opens the next set at the start of an iteration.
0verified
intermediate lemmas
Nothing in this iteration has been accepted by the Lean kernel. Nothing else counts as verification.
Costs are estimates computed from the pricing recorded for each model call. The orchestrator checks every limit before it spends anything.
Construct a large subset S of [N] by a random greedy process: order elements by decreasing number of divisors (or by a random permutation weighted by divisor count) and include an element if it does not divide two already-included elements. Analyze the expected size using a potential function that tracks, for each included element, the number of elements it divides. This may yield a lower bound of order N / sqrt(log N) or better, and the analysis can be formalized in Lean for the key counting lemmas.
The random-greedy-with-divisor-count-potential direction is exhausted as a lower-bound method. For N up to 200000, the greedy construction (process elements in decreasing divisor-count order, include iff it does not divide two already-included elements) yields sets of size ≈0.5N, matching the trivial top-half construction and far below the known optimum f(N) ~ 0.6735N. The divisor-count potential does not help: early high-divisor-count elements block too many later elements, and the greedy rule is too conservative. No nontrivial lower bound of order N/sqrt(log N) or better emerges from this construction.
For a fixed N, construct a family of disjoint chains in the divisibility poset (e.g., chains of the form a, 2a, 4a, ... and variants) such that every element of [N] appears in at least one chain, and each chain has length at most L. Since a valid set S can contain at most one element from each chain, summing over chains gives an upper bound on |S|. Optimize the choice of chains (using a fractional covering LP) to get a strong upper bound, and prove the bound for all N by a clean chain construction. This is a new angle because it uses a global chain cover rather than a fixed interval partition.
The disjoint-divisor-chain LP upper bound is exhausted. The minimum number of chains needed to cover the divisibility poset on [N] is exactly ceil(N/2) for every N <= 2000 (computed exactly via Dilworth's theorem / maximum bipartite matching). This equals the trivial upper bound already known from the disjoint pairs {k, 2k}, k <= N/2. Since any chain cover must contain at least one chain per such pair, and each pair is an antichain, the chain-cover method can never yield an upper bound better than ceil(N/2). Thus this direction cannot improve the known bounds.
View the problem as a 2-Sperner-type condition in the divisibility poset: no element is below two others. Use the rank function r(n) = floor(log_2 n) or the number of prime factors with multiplicity to partition [N] into levels. Prove that any set with the property must have small intersection with the union of any two high ranks, and combine this with a weighted LYM-type inequality to bound the total size. This may lead to a sharp asymptotic upper bound and also suggests the extremal structure, which can be tested and formalized for small N in Lean.
The rank-based Sperner-type direction is exhausted. Using rank r(n)=floor(log2 n), the constraint that no element divides two others only forces at most one element per pair of consecutive high ranks, and the resulting weighted LYM-type bound is strictly larger than N for every N tested (N up to 2000). Hence this direction cannot yield any upper bound better than the trivial |S|<=N, and it cannot even recover the known lower bound f(N)>=ceil(2N/3). The rank function does not capture the divisibility structure tightly enough.
Construct large subsets of [1,N] by taking all numbers in a carefully chosen set of residue classes modulo a small integer m, ensuring that no element divides two others. Analyze the density and optimize over m and residue choices. This is a constructive lower-bound approach that may yield near-optimal sizes and suggest the true extremal density.
The modular residue-class construction direction is exhausted. For any fixed modulus m, a union of residue classes modulo m has density at most 1/2 unless it is the whole interval (which is invalid), because any residue class r mod m contains both r and 2r (when 2r <= N), so a valid set cannot contain a full residue class together with its multiples in a way that exceeds the top-half interval. The top-half interval {floor(N/2)+1,...,N} of size ceil(N/2) is the best such construction and is already known. A finite search over all moduli m <= 12 and all residue-class unions for N up to 2000 confirms no union of residue classes modulo m beats ceil(N/2). Therefore this direction cannot improve the known lower bound and is exhausted.
Prove an upper bound by partitioning the interval into chains under the divisibility relation (e.g., using the standard chain decomposition by odd part) and then applying a condition that no element can be a 'parent' of two elements in the same chain. This yields a counting argument that may match or improve known bounds, and can be formalized in Lean as a lemma about finite posets.
The divisor-chain decomposition direction is exhausted and yields no non-trivial upper bound. Partitioning [1,N] into odd-part chains C_m={m,2m,4m,...} and using that each chain contributes at most 2 elements gives the only rigorous upper bound available from this direction: U(N)=sum_{m odd<=N} min(2, floor(log2(N/m))+1). Computation for all N in [1,2000] shows U(N) > ceil(N/2) for every N>=3, with the gap growing roughly like N/6 (e.g., U(2000)=1333 vs ceil(2000/2)=1000). Thus this direction cannot establish the conjectured upper bound f(N)<=ceil(N/2); it only yields a weaker bound. Any further refinement (weighted double-counting, chain merging, etc.) would need to overcome the fact that the naive chain bound is already too weak, and no such refinement is apparent from the chain structure alone.
Implement a backtracking or integer-programming search to compute the exact maximum subset size for N up to, say, 50 or 100. Use the results to identify the extremal sets, their structure, and conjectured formulas. This empirical data will guide the other two directions and can be used to test hypotheses before attempting proofs.
Computational search and pattern discovery for small N is exhausted. Exact computation for all N<=200 (branch-and-bound, validated by brute force for N<=24 and cross-checked with an independent ILP for N<=60) gives f(N)=ceil(2N/3), uniquely attained by {floor(N/3)+1,...,N}; the same holds for shifted intervals [x, x+N) with x<=20, N<=30. A fresh independent exact search for N<=60 reconfirms f(N)=ceil(2N/3) with the unique extremal set {floor(N/3)+1,...,N}. No new pattern or counterexample emerges, so this direction is exhausted.
No limit configured for this iteration.