Exact values F(6)=14 and F(7)=17 for a function of Gowers and Long

Strengths

• Lower-bound witnesses for n=6 (14) and n=7 (17) are valid 2-increasing sequences in range; I re-checked both.
• A status table separates rigorous, computational and partly proof-checked claims.
• F(6)<=14 is supported by an independent branch-and-bound program, CP-SAT and CaDiCaL, and a DRUP proof accepted by a second checker that also rejects five false proofs.
• Symmetry reduction and partition arithmetic are internally consistent: 84 sorted first elements, 83 excluding (1,1,1), 77 second elements, 312 subcubes of (1,1,2); 471 = 425+46 and 407+18 = 425.
• The paper discloses AI-assisted production, the absence of human review and the limits of its verification.

Weaknesses

• The F(7)<=17 upper bound lacks checked certificates for 18 of 425 DRUP proofs, the largest ones (up to 9e6 lemmas). Only solver agreement on a coarser 160-cube split supports them.
• There is no LRAT or drat-trim certificate, the RUP checkers are unverified software, and the cube splitter is a single implementation.
• The paper discloses an earlier bug in the proof partition but does not say whether the 160-cube solver runs, which include cubes with two fixed elements, were repeated after the fix.
• Theorem 1 and the abstract state F(7)=17 without qualification, although Table 2 marks the upper bound as only partly proof-checked.
• The novelty claim rests on a limited search, and the paper's own statement that no priority is claimed weakens its significance.
• Significance is limited to n<=7 with no structural or asymptotic result, and the paper says it neither proves nor refutes Conjecture 1.8.

Potential errors

• Section 2 says F(n) <= n^{3/2} holds 'with equality only at n = 4'. Table 1 gives F(1)=1=1^{3/2}, so equality also holds at n=1.
• Section 1 attributes to Gowers and Long the bound F(n) >= n^{3/2} for perfect squares and Lemma 1.7. I could not verify these (no access to [1]).
• Section 1 says the formal-conjectures file marks F(4)=8 as a sorry. I could not verify this (no web access, file not in my folder).
• Table 1 values for n<=5 are attributed to [1]. I reproduced only n<=4 (1, 2, 4, 8) with a quick search that is not an independent check of the upper bounds.

Strong novelty candidates

None reported.

Unresolved material objections

• The upper bound F(7)<=17, which Theorem 1 asserts, is not fully certified: 18 of the 471 proof jobs have no checked certificate (the largest, up to 9e6 lemmas). If any of them is wrong, F(7)=17 is unsupported; the only evidence for them is agreement between two solvers on a coarser 160-cube split.
• The paper reports an earlier encoding bug in the cube partition (cubes with two fixed elements were encoded contradictorily). It does not state that the 160-cube CaDiCaL and MapleChrono runs, which include the (1,1,1) subcubes with two fixed elements, were repeated with the corrected encoding. Unless shown, the claim that all 160 cubes are unsatisfiable is not established for the corrected encoding.

Strengths

• Explicit witnesses for n=6 (14) and n=7 (17) which I confirmed are valid 2-increasing sequences in [n]^3.
• Transparent disclosure of what is and is not verified, including a discarded buggy run.
• Cross-checks with two SAT solvers, CP-SAT, and an independent SAT-free branch-and-bound for n<=6.
• Method validated by reproducing known values for n<=5.

Weaknesses

• F(7)<=17 is not fully proof-checked: 18 of 425 DRUP proofs (the largest) unchecked, and no LRAT/drat-trim certificate.
• The first-element/second-element cube partition and S3 symmetry reduction are unformalised and a single implementation; a flaw would undermine completeness.
• Checkers (Go RUP, cube code) are written by the author, and the Python rupcheck2 did not finish on the n=6 proof.
• Literature/priority search limited; reference [2] was not read.
• Little mathematical insight; no formal link between the Lean checker and the problem definition.

Potential errors

• Completeness of the cube partition for n=7 (83 first elements plus 77 subcubes of (1,1,1), 312 subcubes of (1,1,2)) depends on a symmetry argument not formalised; the 82+312+77 job count is not obviously consistent from the text alone.
• Lazy cyclic-triple clauses are not consequences of pair clauses; the proofs refer to CNFs including them, so the exact CNF used matters and cannot be checked from the PDF.
• Elements 1..n cubes assumed first-element non-decreasing: valid under S3 only if the first element's coordinate permutation maps the rest consistently, which is true since <_2 is S3-invariant, but is asserted without proof.

Strong novelty candidates

None reported.

Unresolved material objections

• The upper bound F(7)<=17 (hence the exact value F(7)=17) is not fully certified: 18 largest DRUP proofs unchecked, the cube-splitting code and symmetry reduction are unverified, so the main claim F(7)=17 is not established rigorously.