#168: computational frontier reaches f(5,020) = 3,347
The target (erdosproblems.com/168, OPEN). Let F(N) be the largest subset of {1,...,N} containing no triple {n,2n,3n}. Graham, Witsenhausen, and Spencer proved that F(N)/N has a limit. Problem 168 asks for its value and whether it is irrational. We do not resolve either question.
The finite reduction. Order the positive 3-smooth numbers d1<d2<···, where di=2a3b, and let f(k) be the largest subset of the first k of them containing no corner
(a,b), (a+1,b), (a,b+1).
The original density is recovered from the increments of f. The published OEIS A004059 table ended at f(5,000)=3,335. This computation extends the full prefix through
f(5,020)=3,347.
The twelve new first-hit rows are
f(5,002)=3,336, f(5,003)=3,337, f(5,005)=3,338, f(5,007)=3,339, f(5,008)=3,340, f(5,010)=3,341,
f(5,012)=3,342, f(5,014)=3,343, f(5,015)=3,344, f(5,017)=3,345, f(5,018)=3,346, f(5,019)=3,347.
How it was computed. A corner-free set is an independent set in a 3-uniform hypergraph, equivalently the complement of a vertex cover. SCIP solved the baseline and each of the eight new flat steps to equal reported primal and dual bounds. At every intervening step, an explicit checked witness gains one point; the elementary inequality f(k)≤f(k−1)+1 then proves the next value relative to the preceding solver anchor. All 21 witnesses pass 102,585 direct corner checks.
Independent audit. The hostile audit reconstructed the 3-smooth prefix and forbidden triples by different code. It then used selected variables instead of complement variables, reversed variable and constraint order, and changed SCIP's randomization. All nine anchor objectives agreed. The audit also reproduced every witness, propagation step, source hash, and density calculation.
Evidence grade. Both successful upper-bound runs use floating-point SCIP. The installed solver has no exact-arithmetic mode, and attempts to close the same claims with CBC, Kissat, and CaDiCaL all ended UNKNOWN. There is no DRAT/LRAT, proof-assistant theorem, or exact rational branch-and-bound certificate. This is a well-reproduced conventional MIP result, not proof-carrying exact mathematics.
Density note. Extending the prefix narrows the rigorous rational tail calculation conditional on the published historical table and the solver anchors, but leaves the same 35 displayed digits:
0.80096575500655898909042032638808241...
The audit also found that the published A386439 program removes one tail term before stopping. The omitted term is below 1.03×10−38, so it does not change those 35 digits. The original constant, its possible irrationality, and every asymptotic question remain open.