{"id":"92bbbe47-c37c-4962-9de6-c09784418325","arxiv_id":"2506.11628","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"Tiling the plane with two polygonal prototiles is undecidable, improving the known three-tile bound, and monotiling under local edge-to-edge matching rules is undecidable for the first time.","lead":"This paper proves that no algorithm can decide, given two polygon shapes, whether they can tile the whole plane by rotated and translated copies. It also proves the first undecidability result for a single tile whose placement is governed only by local edge-to-edge matching rules.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Gap-condition converse in §2.5 is asserted without proof; the AB-tiling-to-stick-tiling direction of Theorem 15 depends on it, so the central biconditional is not yet established.","rationale":"The paper aims to prove two-tile undecidability through a chain: Wang tiles to AB tiling, AB tiling to stick tiling with matching rules, and matching rules to two geometric tiles. For the central claim, every implication must hold in both directions. The weakest link is the unproved converse in §2.5, which the reader also identified. Lemmas 6 through 9 establish necessary conditions for a geometric weave tiling to yield a symbolic gap assignment, but the paper asserts sufficiency without proof. In the forward direction of the reduction (AB tiling exists implies stick tiling exists), the construction only produces a symbolic assignment satisfying the gap conditions; without the converse, no geometric tiling follows. This is distinct from the undecidability claim itself: it concerns the faithfulness of the schematic-to-tiling map. The same issue affects Theorem 2 and therefore Theorems 1 and 3. I agree with the reader that a conditional verdict is appropriate. I also checked the other load-bearing steps: Lemma 4's weave-forcing relies on extensive figure-based case analysis and is plausible but not fully formal, and Lemma 17's staple simulation contains a concrete false angle-sum enumeration, namely 7π/12+5π/6+7π/12=2π is omitted from the list of ways to reach exactly 2π. That second issue is a genuine defect in the staple-simulation proof and needs repair. Neither observation reveals a contradiction in the main construction, and the algebraic core of the encoding is detailed and explicit, so the correct verdict remains conditional pending completion and verification of the omitted and figure-dependent arguments.","tokens_in":20578,"tokens_out":8766,"duration_ms":84140,"concrete_test":"Build a small finite instance of the §2.5 construction (e.g., s=4, v=3, t=1 with the paper's Li, Ri, and Ii sets) and use an SMT/constraint solver to search over periodic assignments of states, left values, and right values satisfying the gap conditions. For each assignment, ask whether there exist block positions for every row: blocks of length n separated by gaps with the prescribed left/right lengths, adjacent rows overlapping by at least 1, and each gap end lying under a triangle/arrow mark of the correct position. A cyclic assignment that satisfies the algebraic gap conditions but admits no such block placement is a counterexample to the converse and breaks the AB-to-tiling direction. Conversely, if the sweep finds none, re-derive the omitted calculations of §2.5 as a full lemma, or formalize the schematic-to-tiling construction in a proof assistant, to close the gap.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 2.5 defines the gap conditions and then states: 'any of assignment of the states, left values, and right values to a diagonal lattice of gaps that satisfies the gap conditions corresponds to a valid schematic (and so to a valid tiling).' The justification is explicitly deferred: 'These calculations are essentially no different from the ones in the proofs of Lemmas 6 to 9, so we will not include them here.' This converse is load-bearing in the AB-to-stick direction of Theorem 15. Given an AB tiling, Lemmas 11 and 13 produce states and values satisfying the local algebraic gap conditions, but no geometric block row is constructed. A valid schematic requires each row to be a bi-infinite sequence of blocks of length n separated by gaps whose left/right lengths equal the assigned values, adjacent rows overlapping by at least one unit, and every gap end landing exactly on a triangle or arrow mark. The gap conditions constrain states, lengths, and value differences locally; they do not by themselves guarantee that row offsets can be chosen consistently around cycles, that the required overlaps are always positive, or that the unit segments align with the prescribed markings. If some satisfying assignment has no geometric realization, an AB tiling need not yield a stick tiling, and Theorem 2, and hence Theorem 1, would fail even though the algebraic core is internally consistent. This is not a cosmetic omission: it is the completeness half of the reduction. A separate concrete issue appears in Lemma 17, where the list of angle sums to 2π omits 7π/12+5π/6+7π/12; that second issue affects the staple simulation and should be repaired, but the §2.5 converse is the deeper gap.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper claims that the following problem is undecidable: given two polygonal prototiles, determine whether the plane can be tiled with rotated and translated copies of them. This would improve the recent three-tile undecidability result of Demaine and Langerman. The proof proceeds by first proving a stronger intermediate statement: with edge-to-edge matching rules, a single prototile has an undecidable tiling problem. The construction reduces from Wang tiling via AB tiling, encodes AB tilings as \"weave patterns\" of stick-shaped polyhexes, abstracts these tilings into row schematics with states and values governed by local \"gap conditions,\" and then uses a small staple tile to simulate the edge-to-edge matching rules geometrically. The paper also states consequences for translational tiling and sketches a three-polyomino analogue.","tokens_in":20923,"tokens_out":10217,"duration_ms":102403,"significance":"If the proofs are completed as claimed, Theorem 1 is a genuine quantitative improvement (from three to two polygonal prototiles) for a long-studied undecidability question in tiling theory, and Theorem 2 is the first undecidability result for monotiling under purely local edge-to-edge matching constraints. The reduction is self-contained: it is anchored in the independent undecidability of AB tiling, it defines all constants explicitly (such as d=12k and v=(2t+1)d), and it addresses both directions of the main biconditional. The schematic/gap-condition framework is a useful abstraction that could be reused. However, one load-bearing converse direction is currently asserted without proof, so the central result is not yet fully established.","major_comments":[{"comment":"The claim at the end of Section 2.5 that \"any assignment of the states, left values, and right values to a diagonal lattice of gaps that satisfies the gap conditions corresponds to a valid schematic (and so to a valid tiling)\" is asserted without proof; the text defers the verification with \"These calculations are essentially no different from the ones in the proofs of Lemmas 6 to 9, so we will not include them here.\" This is a load-bearing step, not a cosmetic omission: the AB-tiling-to-stick-tiling direction of Theorem 15 (Section 2.9) constructs only states and values via Lemmas 11 and 13 and then invokes this converse to obtain a geometric tiling. The gap conditions constrain the algebraic quantities locally, but they do not, as written, establish that row offsets can be chosen consistently around cycles, that adjacent rows overlap by at least one unit, or that every gap end lands on the prescribed triangle and arrow marks. Please supply the missing proof, for example by an inductive construction of the row offsets and a verification that the overlap and marking requirements follow from the value-difference constraints in Lemma 9.","section":"2.5"},{"comment":"The proof of Lemma 4 contains an unexpanded key step: after showing that every left-leaning stack has two stacks above and two below, it states \"It remains to check that the left-leaning stacks forms a grid. Specifically... But this is straightforward.\" This commutation property is part of the definition of a weave pattern and is what justifies the passage to the row-schematic representation used in Section 2.3 and throughout the reduction. Since the second direction of Theorem 15 starts from an arbitrary valid tiling and extracts a schematic, the grid property must be verified explicitly rather than deferred as straightforward. Please either provide the local case analysis or state and prove the missing lemma.","section":"2.1"}],"minor_comments":[{"comment":"There are several typos and grammatical slips that should be corrected: \"Any of assignment\" (Section 2.5), \"vise versa\" (Section 2.3), \"undecideable\" (Theorem 15), and \"polyonimo\" (Section 4).","section":"2.5"},{"comment":"In the proof of Theorem 15, the sentence \"the B tile with lower-left corner is the one represented by gap (e1 - sr, 2c + 1)\" is missing the coordinates of the lower-left corner; it should specify (2c+1, 2r+1) or the equivalent.","section":"2.9"},{"comment":"Lemma 16 is stated without proof; a short argument that a regular 12-gon cannot tile the plane on its own would make the staple construction self-contained.","section":"3"},{"comment":"The proof of Lemma 4 relies heavily on visual case analysis in Figures 6-18; a text enumeration of the forbidden local configurations would help verification and would avoid the need to infer cases from the figures.","section":"2.1"},{"comment":"The three-polyomino undecidability result is presented only as a sketch; the text should state explicitly which parts are complete and which remain to be supplied.","section":"4"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is original and the reduction is substantial. The main obstacle is the missing proof of the converse in Section 2.5; I would not reject on this basis, since the omitted step appears to be a long but routine verification. If the author supplies the missing lemma and addresses the Lemma 4 grid-check step, I would be willing to accept."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Jack Stade's paper claims the two-tile tiling problem is undecidable, improving Demaine and Langerman's three-tile result. The core construction is genuinely inventive: a single stick prototile with edge-to-edge matching rules that forces a 'weave pattern,' an abstraction to row schematics, and a bucket/state system that encodes AB tilings (hence Wang tilings). If the proof is completed, this is a real step forward and also gives the first monotiling undecidability with local matching rules.\n\nWhat's good: the reduction is self-contained and goes through a clean intermediate problem, AB tiling, which is convincingly shown undecidable. The algebraic machinery—states, values, gap conditions—is internally consistent, and the proved lemmas are derived carefully. The paper is also honest about what it leaves out.\n\nThe soft spots are real. Section 2.5 asserts the converse of the gap-condition characterization without proof: any assignment of states and values satisfying the local conditions yields a geometric schematic. That converse is load-bearing for the AB-to-stick direction of Theorem 15, because Lemmas 11 and 13 produce algebraic assignments, not tilings. The paper punts with 'essentially no different from Lemmas 6 to 9.' That may be true, but it is exactly what a referee needs to see demonstrated, especially since the local conditions don't obviously guarantee global row alignments, positive overlaps, or that gap ends land on the triangle marks. Until then, the biconditional is not established.\n\nThere is also a concrete bug in Lemma 17: the list of angle sums to 2π omits 7π/12 + 5π/6 + 7π/12. That combination is geometrically possible, so the staple-simulation proof is incomplete as written. It looks repairable, but it's a missing case.\n\nLemma 4's forcing argument relies heavily on figures and 'straightforward' claims; it is the kind of case analysis needing a more formal accounting, though nothing about it looks wrong.\n\nBottom line: this is a serious paper with a plausible but not yet complete proof. People working on tiling decidability will want to study it. It deserves a rigorous referee, and the author should be asked to supply the missing converse and fix the angle enumeration. I wouldn't cite it as a proven result yet, but for a reading group it's worth the time.","headline":"Plausible two-tile undecidability with a genuinely new construction, but the completeness direction rests on an unproven converse and Lemma 17 has a missing angle case; deserves serious refereeing, not acceptance yet.","tokens_in":21594,"tokens_out":2943,"would_cite":false,"duration_ms":27537,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["52C20","05B45"],"pacs":[],"model":"deepseek-v4-flash","headline":"Given two polygonal prototiles, deciding whether they tile the plane is undecidable, improving the previous three-tile bound.","keywords":["undecidability","tiling","prototiles","edge-to-edge matching rules","monotiling","Wang tiles","polyominoes","computational geometry"],"falsifier":"For a small Wang tile set, implement the reduction and check a finite patch: enumerate all gap-condition assignments on a finite diagonal lattice and test whether each can be aligned into a schematic; a single assignment that satisfies Lemmas 7-9 but cannot be realized geometrically would refute the completeness direction and force a repair of the reduction that the two-tile theorem depends on.","tokens_in":20277,"feed_emoji":"🧩","tokens_out":11525,"duration_ms":117398,"temperature":0.7,"pith_summary":"This paper tries to establish that the geometric tiling problem is undecidable even when the input consists of only two polygonal prototiles, improving a previously known bound of three tiles. It also proves a companion result: if edge-to-edge matching rules are allowed, one prototile already gives an undecidable tiling problem, the first such monotiling undecidability under only local matching constraints. The proof routes Wang tiling through an intermediate AB tiling problem, then into weave-pattern tilings by a single stick-shaped polyhex tile, and finally into two real polygonal tiles by adding a small staple tile that simulates the matching rules. If the proof is right, no algorithm can decide two-tile tilability, and the boundary between decidable and undecidable tile counts is pushed down as far as this method allows.","feed_headline":"Tiling is undecidable with just two polygon shapes","feed_subtitle":"A single stick-shaped tile with local matching rules encodes Wang tilings, dropping the known bound from three tiles to two.","key_machinery":"The central object is a stick prototile made of n hexagons, realizable as a polyhex, together with a list of forbidden edge pairings that force any tiling into a weave pattern: a diagonal grid of horizontal and slanted stacks of sticks. The argument's movable mechanism is the tiling schematic, in which each horizontal stack becomes a block, gaps between blocks carry left and right values, and the matching rules become arrow and triangle markings on block edges. The gap conditions, constraints on states, left and right values, and how they change across rows, make the schematic programmable: they simulate the AB tiling dynamics in the same way that rules on Wang tiles simulate a computation. The second key object is the staple tile, a small regular 12-gon; bumps and dents cut into the stick edges ensure that legal edge pairings leave holes the staple fills, while illegal pairings overlap bumps, converting matching rules into pure geometry.","core_discovery":"The central claim is Theorem 1: there is no algorithm that, given two polygonal prototiles, decides whether rotated and translated copies of them tile the plane. The theorem is proved through Theorem 2, which says the same problem is undecidable for a single prototile when edge-to-edge matching rules forbid certain edge pairs. The reduction chain is: Wang tiling reduces to AB tiling, a parity-constrained tiling by two families of 1x2 rectangles; AB tiling reduces to tilings by a stick of n hexagons that local matching rules force into a weave pattern; and a weave pattern is compressed into a schematic whose rows of blocks and gaps satisfy explicit gap conditions. The two-tile theorem follows by modifying the stick's edges with bumps and dents and adding a small staple tile so that every legitimate edge match leaves spaces exactly fillable by the staple, while forbidden matches create overlapping bumps. The author also notes the construction yields undecidability of translational 4-tiling and sketches how the same ideas give undecidability with three polyomino prototiles.","pith_inferences":["Editorial: the weave-pattern scaffolding treats the plane as a programmable lattice, so the same gap-condition machinery may transfer to other decision problems where a few geometric objects must simulate a computation, not just tiling.","Editorial: making the Section 2.5 converse fully explicit would turn the proof into a constructive compiler from Wang tile sets to concrete polygon coordinates, making the undecidability reduction directly testable on finite patches.","Editorial: if the three-polyomino sketch can be completed rigorously, the only remaining gap between decidable and undecidable polyomino tilability would be two polyominoes, close to the one-tile case that is still open."],"forward_implications":["Two polygonal prototiles are sufficient to make the plane-tiling decision problem undecidable, lowering the known tile count from three to two.","A single prototile with edge-to-edge matching rules has an undecidable tiling problem, so local matching constraints alone do not restore decidability to monotiling.","The construction uses four total tile orientations, so translational 4-tiling is undecidable; since translational monotiling is decidable, only the two- and three-tile translation cases remain open.","The same technique is sketched to give undecidability with three polyomino prototiles, improving the previous five-polyomino bound.","The reduction is robust to whether reflections are allowed, because the stick can be modified so reflected copies can never sit next to each other."],"supporting_citations":[{"why":"This supplies the undecidability of the Wang domino problem, the base problem the whole reduction chain starts from.","marker":"[1]"},{"why":"This gives the three-tile undecidability result that the paper improves and the staple-tile device that converts matching rules into geometry.","marker":"[2]"},{"why":"This shows that colored-edge matching rules can be simulated by purely geometric tiles, justifying the geometric encoding used here.","marker":"[4]"},{"why":"This records the open monotiling decidability question and the atlas-style monotiling undecidability that motivates restricting to local rules.","marker":"[5]"},{"why":"This provides the five-polyomino undecidability baseline that the paper's three-polyomino construction improves.","marker":"[8]"},{"why":"This gives the prior translational 8-tiling undecidability result that the paper's translational 4-tiling theorem improves.","marker":"[12]"}],"fun_headline_variants":["Two polygon tiles make tiling undecidable","Tiling with two prototiles is undecidable","Undecidable tiling with just two shapes","Two-tile tiling proved undecidable","Mono-tiling undecidable with edge rules"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof depends on an unproved converse in Section 2.5: that every assignment of states and values to the diagonal lattice of gaps satisfying the gap conditions actually gives a valid schematic and hence a real tiling; if that converse fails, the reduction from AB tilings to stick tilings is incomplete.","fun_headline_variants_meta":{"raw":{"variants":["Two polygon tiles make tiling undecidable","Tiling with two prototiles is undecidable","Undecidable tiling with just two shapes","Two-tile tiling proved undecidable","Mono-tiling undecidable with edge rules"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000169,"raw_usage":{"total_tokens":1212,"prompt_tokens":843,"completion_tokens":369,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":459,"completion_tokens_details":{"reasoning_tokens":295}},"tokens_in":459,"tokens_out":369,"duration_ms":4169,"temperature":1.0,"reasoning_tokens":295,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T04:07:21.024309+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"For a small Wang tile set, implement the reduction and check a finite patch: enumerate all gap-condition assignments on a finite diagonal lattice and test whether each can be aligned into a schematic; a single assignment that satisfies Lemmas 7-9 but cannot be realized geometrically would refute the completeness direction and force a repair of the reduction that the two-tile theorem depends on.","supporting_citations":[{"cited_title":"The undecidability of the domino problem","cited_arxiv_id":null,"evidence_quote":"This supplies the undecidability of the Wang domino problem, the base problem the whole reduction chain starts from."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"This shows that colored-edge matching rules can be simulated by purely geometric tiles, justifying the geometric encoding used here."},{"cited_title":"Open questions in tiling","cited_arxiv_id":null,"evidence_quote":"This records the open monotiling decidability question and the atlas-style monotiling undecidability that motivates restricting to local rules."},{"cited_title":"Tiling the plane with a fixed number of polyominoes","cited_arxiv_id":null,"evidence_quote":"This provides the five-polyomino undecidability baseline that the paper's three-polyomino construction improves."}],"review_version":1}