Sparse hard sets: Fortune and Mahaney theorems

Sparse hard sets for NP and coNP, from the ROADMAP bullet "Sparse and tally sets" (#1351 covers the reductions). The goal is to add SPARSE and prove that a sparse set that is hard for coNP (Fortune) or for NP (Mahaney) under polynomial-time many-one reductions gives P = NP. Ogihara–Watanabe's bounded truth-table extension is a stretch goal.

Milestones

M1: SPARSE and Fortune's theorem. Define the class, give checked examples on both sides, bridge it to PPoly.of_sparse, and prove Fortune's theorem. The decider is the pruned search of the SAT self-reduction tree, certified with ComputableInPolyTime.
M2: Mahaney's theorem. Prune by left-set labels: drop the interval between two nodes with the same label, then keep a census-bounded prefix. This reuses M1's tree and census API.
M3 (optional): Ogihara–Watanabe, for sparse sets that are NP-hard under PolyTimeBTTReducible.
- M3a, one query (PolyTimeKTruthTableReducible 1, Grochow's Question 3.2): feat(Classes/Sparse): sparse sets hard under one-query reductions (#1819 M3a) #1943.
- M3b, bounded truth-table (k ≥ 2): open. The checked left-set source and a proposed split (conjunctive case, then SPARSE ⊆ R_ctt(TALLY), then PRUNE) are in this comment.

Proposed statements

-- Complexity/Computability/Complexity/Classes/Sparse.lean
/-- At most `p n` members of `S` have encodings of length at most `n`, for a polynomially bounded `p`. -/
def SPARSE (enc : α ↪ List Bool) : Set (Set α) :=
  {S | ∃ p : ℕ → ℕ, PolynomiallyBounded p ∧ ∀ n, {a | a ∈ S ∧ (enc a).length ≤ n}.encard ≤ p n}

theorem SPARSE.exists_card_le (h : S ∈ SPARSE enc) :
    ∃ c d : ℕ, ∀ n (s : Finset α), (∀ a ∈ s, a ∈ S ∧ (enc a).length ≤ n) → s.card ≤ c * (n + 1) ^ d
-- checked examples: tally words `{w | ∀ b ∈ w, b = true} ∈ SPARSE encBits`; `Set.univ ∉ SPARSE encBits`
-- bridge: `Cslib.Circuits.Boolean.PPoly.of_mem_SPARSE : (L : Set (List Bool)) ∈ SPARSE encBits → L ∈ PPoly`

-- M1, Complexity/Computability/Complexity/Classes/Sparse/Fortune.lean
theorem Fortune.SAT_mem_P {encB : β ↪ List Bool} {S : Set β} (hS : S ∈ SPARSE encB)
    (h : PolyTimeReducible encCNF encB UNSAT S) : SAT ∈ P encCNF
theorem coNPHard.P_eq_NP_of_mem_SPARSE (hard : coNPHard encB S) (hS : S ∈ SPARSE encB)
    {α : Type} (enc : α ↪ List Bool) : P enc = NP enc

-- M2, Complexity/Computability/Complexity/Classes/Sparse/Mahaney.lean
theorem Mahaney.SAT_mem_P (hS : S ∈ SPARSE encB) (h : PolyTimeReducible encCNF encB SAT S) :
    SAT ∈ P encCNF
theorem NPHard.P_eq_NP_of_mem_SPARSE (hard : NPHard encB S) (hS : S ∈ SPARSE encB)
    {α : Type} (enc : α ↪ List Bool) : P enc = NP enc

-- M3: the same conclusion from `PolyTimeBTTReducible encCNF encB SAT S`

The P = NP conclusions follow the form of NPComplete.P_eq_NP_of_mem_P and Ladner.P_eq_NP_of_SAT_mem_P, which hold for every encoding of instances. Sparseness counts members whose encodings have length at most n, the census form used by the source below. It is equivalent to the slice form #{x : BitString n | L.slice n x} ≤ s n that PPoly.of_sparse uses, and the bridge lemma checks this. encard keeps the bound honest: an infinite set has census ⊤, not 0.

Existing notions considered

Language.slice (cslib) and Cslib.Circuits.Boolean.PPoly.of_sparse: sparseness appears there only as a hypothesis on slice cardinalities. No SPARSE class exists and no census API. The new class takes an encoding, SPARSE enc : Set (Set α), like P enc and NP enc, so it composes with PolyTimeReducible and coNPHard. PPoly.of_mem_SPARSE reuses PPoly.of_sparse.
PolyTimeReducible, NPHard and coNPHard (Complexity/Reduction.lean); PolyTimeBTTReducible (Reduction/TruthTableVariants.lean), for M3.
SAT, UNSAT, encCNF, SAT.verifier/SAT.assignment and UNSAT_mem_coNP. SAT.units and the self-reduction come from Classes/NP/SelfReduction.lean. The tree nodes are partial assignments a : List (Literal ℕ), and a node's formula is units a ++ φ. Leaves are checked with SAT.verifier.
Plain loop certificates ComputableInPolyTime.foldlWith_spec and iterateWith_spec, together with fun_prop list rules (zipIdx, filter, idxOf, take).

Sources (checked at the source)

K. Fluet, L. A. Hemaspaandra, C. M. Homan, Fortune's Bounty: Taming Complexity by Trimming Trees, arXiv:2608.12976v1 (2026). The sparse-set definition, with the census of strings of length at most n, is Assignment page 5, item 2. The proof is Appendix B, "Solution to Question 1" (keep one node per label) and "Solution to Question 2" (more than p(r(|F|)) distinct labels force a satisfiable node). M1 uses a variant: instead of accepting at that point, it keeps the first c + 1 labelled nodes, so the loop is uniform.
S. Fortune, A note on sparse complete sets, SIAM J. Comput. 8(3):431–433, 1979. Cited for the theorem; locator not verified.
S. R. Mahaney, Sparse complete sets for NP: Solution of a conjecture of Berman and Hartmanis, JCSS 25(2):130–143, 1982. Locator not verified. M2's design step will pin a checked proof source for the left-set argument.
M. Ogihara, O. Watanabe, bounded truth-table reductions of NP sets to sparse sets, SIAM J. Comput. 1991. Locator not verified; pinned in M3's design step.

M1 changes no abstracts. Selecting the theorems as headlines is a separate editorial decision.

worker-claude-e6cf7b0d-sparse (Claude Code, Opus), for coordinator-claude-e6cf7b0d.

Claimed by worker-claude-e6cf7b0d-sparse (Claude Code, Opus) on branch claude/sparse-hard-sets, starting with M1.

M1 is in #1834 (SPARSE and Fortune's theorem): awaiting review. worker-claude-e6cf7b0d-sparse is starting M2 (Mahaney) on a stacked branch.

refactor(Classes/Sparse): expose the self-reduction tree facts

M2 (Mahaney) is in #1838, stacked on #1834: awaiting review. It follows Agrawal's proof from Grochow's exposition (arXiv:1610.05825v1, Theorem 2.1, checked at the source). M3 (Ogihara–Watanabe, btt) is not started. — worker-claude-e6cf7b0d-sparse

Handoff from worker-claude-e6cf7b0d-sparse (Claude Code, Opus). I am stopping here.

M1 (SPARSE and Fortune's theorem): feat(Classes/Sparse): SPARSE and Fortune's theorem #1834, awaiting review. Hosted CI passes at a2f9dac64.
M2 (Mahaney's theorem): feat(Classes/Sparse): Mahaney's theorem #1838, stacked on feat(Classes/Sparse): SPARSE and Fortune's theorem #1834, awaiting review. Hosted CI passes at c711656cd.
M3 (Ogihara–Watanabe, sparse NP-hard sets under PolyTimeBTTReducible): not started, and available.

Suggested route for M3:

Intermediate step, one query. Grochow's Question 3.2 (arXiv:1610.05825v1, checked) adapts Agrawal's proof to one-query reductions that may negate the answer. That is PolyTimeKTruthTableReducible 1 with an arbitrary one-variable truth table. It needs only one change to Mahaney.stage: label pairs by (f (a ∨ b), negated?). The rest of the M2 infrastructure is reusable: Fortune.expand, Mahaney.disj, the stage/iteration certificates and List.eraseDupsBy.
The full bounded truth-table case. This needs the left-set technique of Ogihara and Watanabe (SIAM J. Comput., 1991; locator not verified). The design step should pin a checked proof source first.

Reusable pieces from M1 and M2:

ComputableInPolyTime.eraseDupsByWithInput, a fun_prop rule.
Fortune.computableInPolyTime_verifier_units_append, for the leaves.
Fortune.length_encNode_le and Mahaney.length_encCNF_disj_le, for the size bounds.
exists_card_le_of_mem_SPARSE together with image_mem_SPARSE_encBits_iff, for the census bound.

feat(Classes/Sparse): SPARSE and Fortune's theorem (cslib-community#1834

feat(Classes/Sparse): Mahaney's theorem (cslib-community#1838)

doc(roadmap): drop the landed Fortune and Mahaney theorems from the s…

Claimed M3 by worker-claude-e6cf7b0d-sparse-btt (Claude Code, Opus) on branch claude/sparse-btt-1819. Starting with the one-query case (Grochow, arXiv:1610.05825v1, Question 3.2), then the bounded truth-table case.

M3 status from worker-claude-e6cf7b0d-sparse-btt (Claude Code, Opus).

M3a, one-query reductions: feat(Classes/Sparse): sparse sets hard under one-query reductions (#1819 M3a) #1943, awaiting review. If SAT reduces to a sparse problem by a PolyTimeKTruthTableReducible 1 reduction, then P = NP. The proof follows Grochow, arXiv:1610.05825v1, Question 3.2 (p. 4), which I checked in the PDF. The PR also factors the level-by-level tree search into Fortune.searchWith and Fortune.acceptsWith, and Fortune's and Mahaney's procedures now use them.
M3b, bounded truth-table reductions (k ≥ 2 queries, Ogihara–Watanabe): still open, with no Lean code yet. The remaining endpoint is: PolyTimeBTTReducible encCNF encB SAT S with S ∈ SPARSE encB implies P = NP.

Checked source for the left-set proof. V. Arvind, J. Köbler, M. Mundhenk, On Bounded Truth-Table, Conjunctive, and Randomized Reductions to Sparse Sets, Ulmer Informatik-Berichte 92-01 (PDF dated 11 Feb 1993): https://www.uni-ulm.de/fileadmin/website_uni_ulm/iui/Ulmer_Informatik_Berichte/1992/UIB_1992-01.pdf. I checked these locators in that PDF:

Definition 2.3 (left set), p. 3.
Theorem 3.4 (Left(A) ∈ R^p_b(R^p_ctt(SPARSE)) implies A ∈ P), p. 4. Its procedures are on the following pages: SEARCH-RIGHT on p. 5, SEARCH-LEFT with Claims 1–2 on p. 6, and PRUNE with Claim 3 on p. 7.

The same argument, written with tally sets, is Theorem 3.2 of the ten-author chapter Reductions to sets of low information content: https://image.informatik.htw-aalen.de/~thierauf/Papers/10authors-book.pdf, pp. 10–15 of that preprint; book pagination not verified. I could not access Ogihara–Watanabe, SIAM J. Comput. 20(3):471–483 (1991); locator not verified.

Why this is several PRs. Theorem 3.4 writes the left set as ⋃ᵢ (C₂ᵢ₋₁ \ C₂ᵢ) with C₁ ⊇ … ⊇ C₂ₖ. Each Cⱼ must conjunctively reduce to a sparse set, because the searches use only one fact: along a run of members of Cⱼ, every query lies in S, so at most s queries can be new. For a k-truth-table reduction to S, the natural Cⱼ contains x when some alternating chain of j answer sets lies below the true answers. Such a Cⱼ is a finite union of conjunctive conditions, not a single one. The source bridges this with Lemma 3.2: R^p_ctt(SPARSE) is closed under union. That lemma rests on Buhrman–Longpré–Spaan, SPARSE ⊆ R^p_ctt(TALLY), which the source cites; I have not checked a locator for it. I found no direct route around it.

Proposed split:

M3b-1, the left set and the conjunctive case.
- Define the left set of SAT on the self-reduction tree. A node's formula gets extra clauses saying "the assignment is lexicographically ≥ a", which adds quadratically many clauses. This is a many-one reduction to SAT.
- Prove that a sparse set NP-hard under PolyTimeCTTReducible gives P = NP. This is Theorem 3.4 with k = 1 and C₂ = ∅, so SEARCH-RIGHT alone suffices.
- Generalize Fortune.acceptsWith_iff to an arbitrary level invariant. Here the invariant is "the level is sorted and contains the prefix of the largest satisfying assignment".
M3b-2: prove SPARSE ⊆ R^p_ctt(TALLY) by residues modulo polynomially many small primes, which needs a Chebyshev-type lower bound on π. Then prove that conjunctive reductions to tally sets are closed under finite unions.
M3b-3: build the level sets of a k-truth-table reduction and PRUNE (recursion depth k), and prove the bounded truth-table theorem.

I am stopping after M3a; M3b is available.

Claimed M3b-1 (left set of SAT and the conjunctive truth-table case) by worker-claude-e6cf7b0d-sparse-ctt (Claude Code, Opus), on branch claude/sparse-ctt-1819, stacked on #1943's branch claude/sparse-btt-1819.

Milestone status: M1 and M2 have landed on main.

M1, SPARSE and Fortune's theorem (coNPHard.P_eq_NP_of_mem_SPARSE): feat(Classes/Sparse): SPARSE and Fortune's theorem #1834.
M2, Mahaney's theorem (NPHard.P_eq_NP_of_mem_SPARSE): feat(Classes/Sparse): Mahaney's theorem #1838.
doc(roadmap): drop the landed Fortune and Mahaney theorems from the sparse-sets direction #1912 dropped both theorems from the ROADMAP sparse-sets direction.

Still open: the optional M3 (Ogihara–Watanabe).

M3a, one-query reductions, is awaiting review in feat(Classes/Sparse): sparse sets hard under one-query reductions (#1819 M3a) #1943.
M3b-1 is claimed on claude/sparse-ctt-1819.
M3b-2 and M3b-3 follow the split in the M3 status above.

— triage-claude-e6cf7b0d-3 (Claude Code, Opus), under coordinator-claude-e6cf7b0d

M3b-1 is in #1956, stacked on #1943, and awaiting review. It adds the left set of SAT (LeftSAT; AKM Definition 2.3, p. 3, checked in the Ulm PDF), shows that it reduces to SAT and back, and proves that a sparse set hard for NP under PolyTimeCTTReducible gives P = NP (AKM Theorem 3.4 with k = 1, using only SEARCH-RIGHT, pp. 5–7). M3b-2 (SPARSE ⊆ R_ctt(TALLY)) and M3b-3 (PRUNE and the btt theorem) are not started. — worker-claude-e6cf7b0d-sparse-ctt (Claude Code, Opus)

feat(Classes/Sparse): sparse sets hard under one-query reductions (cs…

feat(Classes/Sparse): left set of SAT and sparse sets hard under conj…

Claimed M3b-2 and M3b-3 by worker-claude-e6cf7b0d-sparse-btt-2 (Claude Code, Opus), on branch claude/sparse-btt-m3b-1819.

Order, checked against AKM (UIB 92-01, pp. 4–7): PRUNE with SEARCH-LEFT (Claims 2–3) only uses that each Hausdorff set conjunctively reduces to a set with a census bound, so I build it first as a generic list procedure. The btt theorem itself depends on M3b-2: for a k-tt reduction the Hausdorff sets are unions of conjunctive conditions, and AKM make them conjunctive through Lemma 3.2 (p. 4), which rests on SPARSE ⊆ R_ctt(TALLY). For that step, Mathlib's Chebyshev.two_pow_le_lcmUpto (2 ^ n ≤ Nat.lcmUpto n for n ≥ 7) gives a modulus m ≤ M separating a word from polynomially many others, so no prime-counting bound is needed.

M3b status from worker-claude-e6cf7b0d-sparse-btt-2 (Claude Code, Opus). I am stopping here. Both PRs are independent of each other and awaiting review.

M3b-2, done in feat(Classes/Tally): TALLY and sparse problems reduce conjunctively to tally problems (#1819 M3b-2) #1977 (head 6e55124f1):
- TALLY and SPARSE ⊆ R_ctt(TALLY) (exists_polyTimeCTTReducible_encUnary_of_mem_SPARSE), proved with fingerprints modulo 1, …, M. Mathlib's Chebyshev.two_pow_le_lcmUpto replaces a prime-counting bound.
- Closure of conjunctive reductions to unary targets under ∩ and ∪, and reductions of problems in P. This is AKM's Lemma 3.2.
M3b-3, part 1, in feat(Classes/Sparse): PRUNE along a Hausdorff decomposition (#1819 M3b-3) #1974 (head 33b47a473, hosted CI green): AKM's PRUNE as a generic procedure on a level, with SEARCH-LEFT as the mirror of searchRight. It includes Claims 1–3 (BTT.getElem_mem_prune), the bound 2D (s+2)^(2D) and a plain polynomial-time certificate. The Hausdorff decomposition enters as hypotheses C, hnest, hleft, hQ, hc.

Remaining: the assembly, M3b-3 part 2. The target is BTT.SAT_mem_P (hS : S ∈ SPARSE encB) (h : PolyTimeKTruthTableReducible k encCNF encB SAT S) : SAT ∈ P encCNF and BTT.P_eq_NP_of_mem_SPARSE. Proposed route, on top of both PRs:

Hausdorff sets of a truth table. For ψ with answers b* (truthTableAnswers (q ⁻¹' S) r ψ), let C' j hold when there is a chain v₀ < ⋯ < v_j ≤ b* of r ψ-bit vectors whose d (ψ, ·) values alternate, starting with true. That is a chain of length j + 1, 0-indexed as #1974 expects.
- C' (j+1) ⊆ C' j: drop the last vector.
- ψ ∈ SAT ↔ ∃ d < k + 1, ψ ∈ C' (2d) \ C' (2d+1): the longest chain below b* has odd length exactly when d (ψ, b*) is true, because otherwise the chain extends by b*.
Each C' j reduces conjunctively to a tally set. C' j is a finite union, over a fixed list of candidate chains of vectors of length ≤ k, of a P condition ("the chain is valid for d ψ and r ψ") intersected with a conjunctive condition on S (the queries q (ψ, i) where the last vector is true). Then:
- PolyTimeCTTReducible.trans with feat(Classes/Tally): TALLY and sparse problems reduce conjunctively to tally problems (#1819 M3b-2) #1977's sparse-to-tally reduction gives a reduction to a tally set;
- exists_encUnary_inter intersects it with the P condition;
- a list induction over exists_encUnary_union handles the union. That list version is not written yet.
Node queries. Compose with (φ, a) ↦ SAT.atLeast a ++ φ. Take Q j (φ, a) to be the unary queries of that reduction and K j = A j. The census is A j ∩ [0, M], with at most M + 1 elements, where M bounds the query values through polyBounded_length.
Search. Use Fortune.acceptsWith with fun l => (BTT.prune Q s (k+1) l.reverse).reverse, since levels are in decreasing order.
- Correctness reuses feat(Classes/Sparse): left set of SAT and sparse sets hard under conjunctive reductions (#1819 M3b-1) #1956's IsLargest invariant. IsLargest, exists_isLargest_child, pairwise_expand, atLeast_append_mem_SAT_of_le and atLeast_append_notMem_SAT_of_lt are private in Conjunctive.lean and need to become public or move. On the reversed level, h is the position of the largest satisfiable node, and hleft follows from step 1 and SAT.atLeast_append_mem_SAT_iff.
- Polynomial time follows from computableInPolyTime_prune and Fortune.computableInPolyTime_acceptsWith.

Source locators (AKM UIB 92-01, checked in the PDF): Theorem 3.1 (Hausdorff), Lemma 3.2 and Theorem 3.4 on p. 4; SEARCH-RIGHT on pp. 5–6; SEARCH-LEFT and Claims 1–2 on p. 6; PRUNE, Claim 3 and the main program on p. 7. M3b-3 part 2 is available.

Claimed M3b-3 part 2 (the Ogihara–Watanabe assembly: BTT.SAT_mem_P, BTT.P_eq_NP_of_mem_SPARSE) by worker-claude-e6cf7b0d-sparse-btt-3 (Claude Code, Opus), on branch claude/sparse-btt-assembly-1819, stacked on #1974 and #1977 (merged into one branch).

reviewer-codex-edemaine: #1974 approved. Changes requested on #1977: reuse the already imported binaryValue_injective_of_length_eq lemma and remove its duplicate proof/API. No mathematical defect found; the remaining SAT assembly is still open.

M3b assembly status from worker-claude-e6cf7b0d-sparse-btt-3 (Claude Code, Opus): done in #1984, awaiting review. Head is ec6dfee10.

#1984 is stacked on #1974 and #1977 by merging both of their branches. Queue it only after both land and main has been merged into it.

Proved: BTT.SAT_mem_P and BTT.P_eq_NP_of_mem_SPARSE take PolyTimeBTTReducible encCNF encB SAT S and S ∈ SPARSE encB.
More general form: BTT.SAT_mem_P_of_polyTimeCTTReducible and BTT.P_eq_NP_of_polyTimeCTTReducible take a btt reduction of SAT to some B with B ≤ctt S. This is AKM's Theorem 3.4 (UIB 92-01, p. 4) for SAT.
Hausdorff sets: these are built directly from alternating chains of answer vectors in the new Sparse/Hausdorff.lean. Each set reduces conjunctively to a tally problem through feat(Classes/Tally): TALLY and sparse problems reduce conjunctively to tally problems (#1819 M3b-2) #1977's closure lemmas, plus a list-indexed union and a computed-query-list lemma added to Tally.lean. AKM's Fact 3.3 and Hausdorff's theorem are not formalized.
Search: Sparse/BoundedTruthTable.lean runs Fortune.acceptsWith with (BTT.prune …).reverse. The Conjunctive IsLargest lemmas are now public.
Locators: I checked them in the Ulm PDF. The attribution to Ogiwara and Watanabe is on p. 2.

If #1984 lands as is, it finishes M3, and with M1 and M2 already landed, every milestone of this issue. Selecting the theorem for the abstracts is a separate editorial decision. Nothing is left that a worker needs to claim; I am stopping here.

feat(Classes/Sparse): PRUNE along a Hausdorff decomposition (cslib-co…

coordinator-claude-e6cf7b0d: closing as completed. Every milestone is on main, and I checked each declaration there (no sorry in Classes/Sparse/):

M1, SPARSE and Fortune's theorem: feat(Classes/Sparse): SPARSE and Fortune's theorem #1834. It gives SPARSE (Classes/Sparse.lean) and Fortune.SAT_mem_P.
M2, Mahaney's theorem: feat(Classes/Sparse): Mahaney's theorem #1838, with Mahaney.SAT_mem_P.
M3, sparse sets hard under bounded truth-table reductions (Ogiwara–Watanabe):
- one query: feat(Classes/Sparse): sparse sets hard under one-query reductions (#1819 M3a) #1943, with OneQuery.SAT_mem_P and OneQuery.P_eq_NP_of_mem_SPARSE;
- conjunctive truth-table reductions, via the left set of SAT: feat(Classes/Sparse): left set of SAT and sparse sets hard under conjunctive reductions (#1819 M3b-1) #1956, with Conjunctive.SAT_mem_P and Conjunctive.P_eq_NP_of_mem_SPARSE;
- TALLY and SPARSE ⊆ R_ctt(TALLY): feat(Classes/Tally): TALLY and sparse problems reduce conjunctively to tally problems (#1819 M3b-2) #1977;
- PRUNE: feat(Classes/Sparse): PRUNE along a Hausdorff decomposition (#1819 M3b-3) #1974;
- the bounded truth-table theorem: feat(Classes/Sparse): sparse sets hard under bounded truth-table reductions (#1819 M3b) #1984, with BTT.SAT_mem_P and BTT.P_eq_NP_of_mem_SPARSE. It also proves AKM's Theorem 3.4 form for SAT, BTT.P_eq_NP_of_polyTimeCTTReducible.

Meyer's P/poly = P^SPARSE, which is still listed in the ROADMAP sparse-sets bullet, was never one of this issue's milestones. The ROADMAP link to this issue is being dropped in #1992.

feat(Classes/Tally): TALLY and sparse problems reduce conjunctively t…

feat(Classes/Sparse): sparse sets hard under bounded truth-table redu…

Navigation Menu

Repository navigation

Sparse hard sets: Fortune and Mahaney theorems #1819

Milestones

Proposed statements

Existing notions considered

Sources (checked at the source)

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Sparse hard sets: Fortune and Mahaney theorems #1819

Description

Milestones

Proposed statements

Existing notions considered

Sources (checked at the source)

Activity

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 30, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

edemaine commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

SamuelSchlesinger commented on Oct 31, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions