{"id":"2692a431-a724-463f-a095-7d9ef6dc091b","arxiv_id":"2506.12726","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Translational tiling of the plane with a set of seven orthogonally convex polyominoes is undecidable.","lead":"New proof shows that no algorithm can decide whether seven orthogonally convex polyominoes can tile the plane by translations. The result moves the undecidability of translational tiling from highly concave shapes toward the open question of genuinely convex tiles.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 'only if' direction rests on Lemma 4 and the locator-lattice induction, but Lemma 4's local-to-global step and the rigid-lattice argument in Section 4 are not actually proved; a shifted or non-rigid tiling would break the Wang encoding.","rationale":"The reader's weakest assumption correctly identifies the rigidity lemmas, especially Lemma 4 and the locator-lattice induction, as the load-bearing point. My reading of the proof confirms that this is where the central equivalence is least secure: Lemma 4's proof depends on an unstated uniqueness claim about gaps, and the locator-lattice argument is a diagrammatic induction without a formal case analysis. These are addressable gaps rather than demonstrated falsehoods, so the appropriate verdict remains CONDITIONAL, not ACCEPT or REJECT. I am not manufacturing a concern: the paper itself gives no detailed proof or formal verification for these steps, and the claims are essential for the undecidability result. The proposed computational test would either expose a concrete counterexample or provide confidence that the rigidity assertions are correct. Thus my read does not change the reader's verdict.","tokens_in":11896,"tokens_out":9510,"duration_ms":115503,"concrete_test":"Write a small program that enumerates all pairwise adjacencies of the seven actual polyominoes (using the coordinates from Sections 2–3) over a bounded set of relative offsets, and classify every boundary gap: perfect match, exactly one tiny filler, or other. If any 'other' gap is geometrically possible, Lemma 4's case analysis is incomplete and the proof of Theorem 2 fails. As a complementary check, run a SAT/SMT-based finite-window search (e.g., 200×200) for a tiling patch that contains a locator but violates the claimed rigid arrangement of Figure 15; a single such patch is a concrete counterexample to the reduction's only-if direction.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim, Theorem 2, depends on the equivalence 'the 7 polyominoes tile the plane iff the corresponding Wang tiles do.' The only-if direction requires that every plane tiling be forced into the rigid pattern of Figure 15, so Wang colors can be read from encoder boundaries. That forcing is supplied by Lemma 4 and the Section 4 bullet 'The locators form a rigid lattice structure.' Lemma 4's proof assumes that any boundary gap between level-3 polyominoes is either a perfect edge match or exactly one tiny filler, and then concludes that level-2 squares must be aligned to the common i,j lattice. But Lemma 3 only rules out two adjacent tiny fillers; it does not rule out a gap that is a tiny filler combined with a shifted level-2 boundary, nor does it prove that every non-perfect gap has the tiny filler's exact shape. The proof therefore presupposes the alignment it is meant to establish. The subsequent locator-lattice argument is equally unsupported: from 'at least one simulated Wang tile is exposed' it asserts locators 2, 3, 4, and 5 must be placed as in Figure 15, then extends inductively. No case analysis eliminates other translations, rotated/reflected arrangements, or partial interlockings of the three locator pieces. These are not merely cosmetic gaps: if any tiling deviates from the rigid lattice, the Wang tile edges are not readable, and the reduction's only-if direction collapses. The paper offers no machine-checked verification and no independent computational evidence for these geometric rigidity claims.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper claims Theorem 2: translational tiling of the plane with translated copies of a particular set of 7 orthogonally convex polyominoes is undecidable. The proof reduces from Wang's domino problem (Theorem 1, Berger). For a given set of Wang tiles, Section 3 constructs one tiny filler, one encoder, two linkers, and three partial locators intended to behave as one locator; the design is meant to ensure that the 7 polyominoes tile the plane if and only if the corresponding Wang tiles do. Section 4 argues that every tiling must follow the rigid pattern of Figure 15, that each encoder exposes a simulated Wang tile, and that linkers enforce color matching. If this equivalence is established, the undecidability of Wang's domino problem transfers, yielding the stated result.","tokens_in":12205,"tokens_out":5249,"duration_ms":65444,"significance":"If correct, this is a notable result: it provides a fixed-size undecidable translational tiling problem under a restricted-convexity condition, and it introduces an elegant high-level encoding of binary strings via dents and bumps on level-3 squares. The construction is explicit and the reduction from Berger's theorem is conceptually clear. However, the proof of the direction from polyomino tilings to Wang tilings rests on several rigidity assertions that are currently only supported by informal, figure-based case analyses. The paper does not ship machine-checked proofs or code, but the burden here is not likely to require that; rather, the missing piece is a complete geometric case analysis for the alignment lemmas and for the global locator lattice. Those gaps are load-bearing for the central equivalence.","major_comments":[{"comment":"The proof of Lemma 3 is not a complete case analysis. It asserts that after placing two adjacent tiny fillers the cells marked with red dots in Figure 14 cannot be covered by any level-3 polyomino, and that the partial tiling cannot be extended, but it does not systematically examine all translations and orientations of the six large polyominoes that could cover those cells while avoiding overlap. Since Lemma 3 is the only stated reason why two tiny fillers cannot be adjacent, and Lemma 4 depends on that exclusion, this needs a rigorous argument or an explicit finite check with coordinates.","section":"Section 3, Lemma 3"},{"comment":"The proof of Lemma 4 assumes part of what it must establish. It moves from Lemma 3 to the assertion that every level-3 polyomino is surrounded by level-3 polyominoes with isolated gaps fillable by a single tiny filler. Lemma 3 only rules out two adjacent tiny fillers; it does not rule out a gap that is a tiny filler combined with a shifted level-2 boundary, nor does it prove that every non-perfect northwest-southeast gap has exactly the shape of the tiny filler. Consequently the concluding sentence 'In all cases, the level-2 squares must be aligned' is unsupported. Without a proof of this lemma, the direction from arbitrary polyomino tilings to Wang tilings cannot be read off.","section":"Section 3, Lemma 4"},{"comment":"This is the central global-rigidity step, but it is only asserted. From the fact that a marker {M|L} must be matched by a selector {L|M}, the text concludes that locators 2, 3, 4, and 5 are placed as in Figure 15 and then extends the pattern inductively. No case analysis excludes other relative translations of locators, rotated or reflected arrangements, or partial interlockings among the three pieces of a locator. The claim that at least one simulated Wang tile is exposed only gives a marker somewhere outside the locator; it does not fix the exact grid placement. If a tiling deviates from Figure 15, the encoder boundaries need not form a valid Wang tiling, so this gap affects the only-if direction of the main equivalence.","section":"Section 4, bullet 'The locators form a rigid lattice structure'"},{"comment":"Theorem 2 asserts that all seven pieces are orthogonally convex, but the verification is dismissed with 'It is straightforward to verify that all of them are orthogonally convex.' Since the level-3 shapes are described symbolically and the locator is deliberately split into three pieces, a check should be supplied: for each of the seven pieces, every horizontal and vertical line should intersect the piece in a segment or empty set. This is not a purely cosmetic point, because the assembled locator is explicitly not orthogonally convex and the splitting into three pieces is what makes the claim possible.","section":"Section 3, end of Section 3"}],"minor_comments":[{"comment":"The text says the two light gray partial locators have size 3 x 15 'in light gray in Figure 12', but Figure 12 depicts the linkers; the light gray pieces appear in Figure 13. The figure reference should be corrected.","section":"Section 3, locator paragraph"},{"comment":"The phrase 'several different notations of restricted convexity' should read 'several different notions of restricted convexity'.","section":"Introduction, Section 1"},{"comment":"The definition of SR writes SR = {Y1, ..., Yi}; since the right part has j entries, this should be {Y1, ..., Yj}.","section":"Section 2.3, notation after Lemma 2"},{"comment":"The final sentence says 'translational tiling of the plane with a set of 7 orthogonally convex is undecidable'; it should say 'a set of 7 orthogonally convex polyominoes is undecidable'.","section":"Proof of Theorem 2, last sentence"},{"comment":"Reference [11] is cited as 'a manuscript'; if it is publicly available, the authors should provide an arXiv identifier or a publication status.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper's dependence on the rigidity lemmas is the main risk. On my reading, the concern raised in the stress-test note about Lemma 4 and the locator-lattice argument is justified: those are not merely presentation gaps but steps that are load-bearing for the claimed equivalence. I do not see circularity, since the reduction uses Berger's theorem and does not feed the constructed tilings back into the argument. The paper may be suitable for publication after the missing case analyses are supplied. I would also ask the editor to verify the status of reference [11], since an unpublished manuscript is used for a technique in the proof."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First, the take: this is a genuine step toward the convex-tile undecidability question, and the construction is clever. The 7-tile set is explicit, the high-level encoding of Wang colors in binary strings on level-3 square sides is new, and the reduction strategy from Berger's theorem is correct in outline. The authors are transparent that the locator must be split into three pieces to keep each piece orthogonally convex. If the rigidity claims hold, Theorem 2 follows. The soft spots are in the proof of rigidity. Lemma 4 claims that every level-2 square in every tiling is aligned to the i,j lattice. The proof argues that by Lemma 3 no two tiny fillers are adjacent, so any gap between level-3 polyominoes is either a perfect match or a single tiny filler. That step is not justified. Lemma 3 only rules out adjacent tiny fillers; it does not rule out boundary configurations involving a tiny filler plus a shifted level-2 square, or boundary shapes that don't match the dent/bump formalism at all. The proof thus assumes the alignment it is meant to establish. The same problem carries into Lemma 5 and into the Section 4 bullet asserting the locators form a rigid lattice. That bullet is a paragraph describing a picture, not a proof: no case analysis eliminates other translations, rotations, or partial interlockings of the three locator pieces. Without the rigid lattice, the Wang edges cannot be read off, and the 'only if' direction of the reduction collapses. The orthogonal convexity of the six large pieces is also asserted as 'straightforward' with no verification; for a paper whose whole point is orthogonal convexity, that needs to be shown. These gaps are load-bearing, not cosmetic. But they are also plausibly addressable: the construction is explicit and the intended geometry is clear. I would not be surprised if the theorem is true and the proofs can be repaired. Who is it for: people working on tiling undecidability and geometric tilings. It deserves a serious referee, not a desk reject. But the referee should send it back for a substantially detailed rewrite of Lemma 4 and Section 4. I would not cite it as an established result until the proof is made rigorous.","headline":"A plausible and important step toward undecidability with nearly convex tiles, but the rigidity lemmas that carry the reduction are asserted rather than proved; the paper deserves a referee but needs a rigorous rewrite of Section 4.","tokens_in":12756,"tokens_out":3830,"would_cite":false,"duration_ms":45107,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["52C20","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that translational tiling of the plane with a set of seven orthogonally convex polyominoes is undecidable, by reducing Wang's domino problem to this tiling problem.","keywords":["translational tiling","undecidability","orthogonally convex polyominoes","Wang tiles","domino problem","fixed tile set","rigid tiling pattern","polyomino"],"falsifier":"Exhibit a plane tiling of the seven polyominoes in which two level-2 squares belonging to different level-3 polyominoes are not aligned on the lattice generated by (13,12) and (-12,13), or in which the locators do not form the claimed grid; such a tiling would directly contradict Lemma 4 or the rigidity argument and would break the only-if direction of the reduction. A finite-patch search with a tiling solver for a violation of Lemma 3 (two adjacent tiny fillers) would be the most direct place to look first.","tokens_in":11658,"feed_emoji":"🧩","tokens_out":10478,"duration_ms":109578,"temperature":0.7,"pith_summary":"The paper proves that no algorithm can decide whether an arbitrary set of seven orthogonally convex polyominoes tiles the plane by translation. The proof reduces Wang's domino problem to this tiling problem: from any finite set of colored square tiles it constructs seven polyominoes that tile the plane exactly when the Wang tiles do. The tiles used are orthogonally convex, meaning every horizontal or vertical slice through a tile is a single segment, whereas previous undecidability results for fixed tile sets relied on deeply concave shapes. If the construction is correct, the undecidability barrier for translational tiling persists even under this restricted convexity, and the question of decidability is pushed down to at most six orthogonally convex tiles.","feed_headline":"No algorithm can decide if 7 orthogonally convex shapes tile the plane","feed_subtitle":"A reduction from Wang's domino problem makes the seven-tile translational tiling problem undecidable.","key_machinery":"The load-bearing object is the level-3 square of order $(13,22)$, a bundle of 22 by 22 level-2 squares, each an order-13 diamond-shaped 'square simulator' that carries either a dent or a bump on its northwest or southeast side. Binary strings written in dents (0) and bumps (1) on these sides encode the colored edges of simulated Wang tiles, and a fixed pattern in the middle twelve positions of each side forces level-3 squares to align edge-to-edge. The set of seven polyominoes — one tiny filler, one encoder, two linkers, and three partial locators that act as a single locator — is engineered so that any plane tiling must align every level-2 square to the common lattice generated by $i=(13,12)$ and $j=(-12,13)$, align every level-3 square in the northwest-southeast direction, and finally arrange the locators into a rigid grid. In that grid the encoder exposes exactly the information needed to simulate a Wang tiling, and the linkers fill the gaps exactly when simulated edge colors match.","core_discovery":"The paper's central claim is Theorem 2: translational tiling of the plane with a set of seven orthogonally convex polyominoes is undecidable. The proof establishes a tiling equivalence: for any finite set of Wang tiles, the constructed seven polyominoes admit a plane tiling by translations if and only if the Wang set does. The 'only if' direction is the hard part; it shows that every tiling of the plane by the seven polyominoes must arrange the pieces in a rigid lattice of locators and encoders, so that the dents and bumps on the tiles read off as encoded colors on simulated Wang-tile edges, and the linkers enforce that adjacent edges share a color. Any algorithm deciding the seven-polyomino tiling problem would therefore decide Wang's domino problem, which is known to be undecidable.","pith_inferences":["Editorial extension: because the locator is split into three partial pieces only to maintain orthogonal convexity, a variant that relaxes the convexity condition slightly might reduce the tile count further, or the same splitting idea might be applied to other gap-filling roles.","Editorial extension: the construction's encoding density — one binary string per building block, rather than one bit per block — suggests that the information-carrying capacity of a single tile can be made large; testing whether a single orthogonally convex tile can simulate arbitrary Wang computation would be a natural stress test of the framework's limits.","Editorial extension: one could computationally instantiate the construction for a small Wang tile set whose tilability is known and search finite patches of the resulting polyomino set for the predicted rigid lattice; if a patch fails to follow Lemma 4 or Lemma 5, it would localize exactly which rigidity claim breaks."],"forward_implications":["No algorithm can decide, for an arbitrary input of seven orthogonally convex polyominoes, whether translated copies tile the whole plane.","The undecidability barrier for fixed tile sets in the plane now holds at $k=7$ with orthogonally convex tiles, where previous fixed-tile-set constructions used extremely concave shapes.","Any Wang tile set that admits only nonperiodic tilings would yield, through this construction, a set of seven orthogonally convex polyominoes that also tiles only nonperiodically, since the polyomino tiling exists exactly when the Wang tiling does.","The decidability question for translational tiling with orthogonally convex tiles is now closed for $k \\geq 7$ and remains open for $k \\leq 6$.","The construction also shows that a relatively simple family of shapes can simulate arbitrary Wang computation, so further restrictions on geometry alone will not automatically restore decidability."],"supporting_citations":[{"why":"Proves Wang's domino problem undecidable, the source of undecidability into which the reduction feeds.","marker":"[2]"},{"why":"Defines Wang tiles and the domino problem, the problem being reduced from.","marker":"[16]"},{"why":"Supplies the fixed-tile-count reduction framework this paper adapts to orthogonally convex tiles.","marker":"[13]"},{"why":"Characterizes when a single connected polyomino tiles the plane by translation; the paper uses it to show the tiny filler alone cannot tile.","marker":"[1]"},{"why":"Provides an optimal algorithm for single-polyomino translational tiling, cited alongside [1] for the same characterization.","marker":"[17]"},{"why":"Contributes the technique of merging two families of gap-filling tiles into one, which the paper uses to hold the tile count at seven.","marker":"[11]"},{"why":"The immediate predecessor result (undecidability with eight polyominoes) whose construction is improved here to seven tiles with orthogonal convexity.","marker":"[20]"}],"fun_headline_variants":["7 orthogonally convex polyominoes make tiling undecidable","Tiling undecidable for just 7 orthogonally convex polyominoes","No algorithm can decide tiling by 7 orthogonally convex polyominoes","Undecidable tiling with 7 orthogonally convex polyominoes","7 orthogonally convex tiles: tiling undecidable"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The reduction assumes that every tiling of the plane using the seven polyominoes forces all level-2 squares to lie on the common lattice generated by $i=(13,12)$ and $j=(-12,13)$, and all locators to form the rigid grid claimed in Section 4; if any tiling escaped this alignment, the dents and bumps could not be read as encoded Wang-tile edges.","fun_headline_variants_meta":{"raw":{"variants":["7 orthogonally convex polyominoes make tiling undecidable","Tiling undecidable for just 7 orthogonally convex polyominoes","No algorithm can decide tiling by 7 orthogonally convex polyominoes","Undecidable tiling with 7 orthogonally convex polyominoes","7 orthogonally convex tiles: tiling undecidable"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00168,"raw_usage":{"total_tokens":6606,"prompt_tokens":837,"completion_tokens":5769,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":453,"completion_tokens_details":{"reasoning_tokens":5666}},"tokens_in":453,"tokens_out":5769,"duration_ms":45886,"temperature":1.0,"reasoning_tokens":5666,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T00:44:55.419797+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a plane tiling of the seven polyominoes in which two level-2 squares belonging to different level-3 polyominoes are not aligned on the lattice generated by (13,12) and (-12,13), or in which the locators do not form the claimed grid; such a tiling would directly contradict Lemma 4 or the rigidity argument and would break the only-if direction of the reduction. A finite-patch search with a tiling solver for a violation of Lemma 3 (two adjacent tiny fillers) would be the most direct place to look first.","supporting_citations":[{"cited_title":"Berger, The undecidability of the domino problem, Memoirs of the American Mathematical Society, 66(1966), 1-72","cited_arxiv_id":null,"evidence_quote":"Proves Wang's domino problem undecidable, the source of undecidability into which the reduction feeds."},{"cited_title":"Wang, Proving theorems by pattern recognition-II, Bell System Technical Journal, 40(1961) 1-41","cited_arxiv_id":null,"evidence_quote":"Defines Wang tiles and the domino problem, the problem being reduced from."},{"cited_title":"Ollinger, Tiling the plane with a fixed number of polyominoes, In: A.H","cited_arxiv_id":null,"evidence_quote":"Supplies the fixed-tile-count reduction framework this paper adapts to orthogonally convex tiles."},{"cited_title":"Beauquier, M","cited_arxiv_id":null,"evidence_quote":"Characterizes when a single connected polyomino tiles the plane by translation; the paper uses it to show the tiny filler alone cannot tile."},{"cited_title":"Winslow, An optimal algorithm for tiling the plane with a translated polyomino, In: K","cited_arxiv_id":null,"evidence_quote":"Provides an optimal algorithm for single-polyomino translational tiling, cited alongside [1] for the same characterization."},{"cited_title":"Kim, Undecidability of tiling the plane with a set of 5 polyominoes, (2025), a manuscript","cited_arxiv_id":null,"evidence_quote":"Contributes the technique of merging two families of gap-filling tiles into one, which the paper uses to hold the tile count at seven."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The immediate predecessor result (undecidability with eight polyominoes) whose construction is improved here to seven tiles with orthogonal convexity."}],"review_version":1}