{"id":"11539523-5f56-4615-8b9e-02d7d38bb424","arxiv_id":"2505.14110","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":7,"one_line_summary":"A computer-assisted geometric proof shows that packings of spheres of radii 1 and sqrt(2)-1 have density at most about 0.812542, slightly improving the previous best bound of 0.813.","lead":"This paper proves a new upper bound on the density of three-dimensional packings of spheres of two sizes, where the smaller spheres exactly fit into the holes of a hexagonal close packing of the larger ones. The proof is computer-assisted and improves the previous best bound from 0.813 to about 0.81254.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 1 relies on a false circumradius bound; the key reduction to one tight edge is not proven.","rationale":"After reading the paper, the central claim is an upper bound on binary sphere packing density. The proof strategy is: (1) reduce to FM-tetrahedra; (2) use sliding (Proposition 5) to reduce to one tight edge; (3) check nine cases by interval arithmetic. The most load-bearing step is (2), because if sliding does not preserve the compression bound, all nine cases are irrelevant. The proof of Lemma 1, which establishes the sliding property, contains a demonstrably false assertion: that a triangle whose vertices lie in a ball of radius 1+r has circumradius at most 1+r. This is false even for the FM-tetrahedron shown in Fig. 12, whose circumsphere radius is about 4.96. Thus the proof of Proposition 5 is incomplete. The reader's identified weakness (degenerate quadratic blocks in the computer check) is a secondary concern: even if the code is perfect, the theorem is not proven without Lemma 1. Therefore the verdict should be REJECT (or at minimum CONDITIONAL on a correct proof of Lemma 1). I recommend REJECT because the current text contains a false mathematical statement in the core argument. The provided code and interval-arithmetic machinery may be sound, but they cannot compensate for the missing analytic bound. The suggested test (search for counterexamples to |BC|/sin(angle BA'C) <= 2(1+r)) would settle whether the lemma itself is salvageable.","tokens_in":22654,"tokens_out":33128,"duration_ms":311601,"concrete_test":"Numerically verify the bound on which Lemma 1 depends: for a fine grid or random sample of FM-tetrahedra (using the supplied code's domain), compute for every vertex A and every point A' on segment AD the quantity |BC|/sin(angle BA'C) and check whether it is at most 2(1+r) = 2.828. If any violation occurs, Lemma 1 is false. If none occurs, supply the missing geometric argument using edge-length lower bounds (r_X + r_Y) that the current text lacks; until then, the proof of Proposition 5 is incomplete. For a quick falsification test, use the sliver (2.7, 1.6, 1.6, 1.5, 1.5, 1.5): compute the circumradius of triangle BA'C for A' at the tight-contact position on AD; if it exceeds 1.414, the asserted bound in Lemma 1 fails on an explicit FM-tetrahedron.","verdict_should_be":"REJECT","load_bearing_attack":"In the proof of Lemma 1 (Section 5.2), after defining the tetrahedron P, the authors bound sin(angle BA'C) via the law of sines, asserting that 'the radius of the sphere circumscribed to T is at most 1+r' and that 'this also bounds from above the radius of the circle circumscribed to the triangle BA'C.' Both steps are invalid: vertices inside a ball of radius 1+r can form triangles of arbitrarily large circumradius, and even for FM-tetrahedra the circumsphere can be much larger than 1+r. For the explicit FM-tetrahedron of type 11rr with edge lengths (2.7, 1.6, 1.6, 1.5, 1.5, 1.5) discussed in Fig. 12 (support radius about 0.35), a direct computation gives circumsphere radius about 4.96, which is far above 1+r = 1.414. The proof therefore does not establish the lower bound used to minorize the volume of P. Since Lemma 1 is the basis for Proposition 5 (sliding to a tight edge), the whole reduction to the nine computer-checked cases depends on an unproven bound. The computer-assisted verification in Section 6 only checks those nine cases; without a correct proof of Lemma 1, it cannot establish Theorem 1.","agreement_with_reader":"disagree"},"referee_report":null,"author_rebuttal":null,"desk_editor":null,"rs_alignment":null,"lean_confirmation":null,"pith_extraction":null,"created_at":"2026-08-07T15:40:00.690003+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":null,"supporting_citations":[],"review_version":1}