Bolzano: Case Studies in LLM-Assisted Mathematical Research

arXiv cs.CL Papers

Summary

Researchers from Charles University introduce Bolzano, an open-source multi-agent LLM system that orchestrates prover and verifier agents to assist with mathematical research, reporting new results on six problems where four reached publishable quality and three were produced essentially autonomously.

arXiv:2604.16989v1 Announce Type: new Abstract: We report new results on six problems in mathematics and theoretical computer science, produced with the assistance of Bolzano, an open-source multi-agent LLM system. Bolzano orchestrates rounds of interaction between parallel prover agents and a verifier agent while maintaining a persistent knowledge base that is carried across rounds. Classified using the significance-autonomy taxonomy of Feng et al., four of the six results reach the level of publishable research, and three of the six were produced essentially autonomously by Bolzano. Our results provide evidence that LLMs can contribute meaningfully to mathematical research, complementing recent reports by Bubeck et al., Woodruff et al., and others.
Original Article
View Cached Full Text

Cached at: 04/21/26, 07:05 AM

# Bolzano: Case Studies in LLM-Assisted Mathematical Research
Source: [https://arxiv.org/html/2604.16989](https://arxiv.org/html/2604.16989)
Jan Grebík1Pavel Hubáček1,2Martin Koutecký1Matěj Kripner3Václav Rozhoň1Robert Šámal1Adrián Zámečník11Computer Science Institute, Charles University2Institute of Mathematics, Czech Academy of Sciences3Institute of Formal and Applied Linguistics, Charles University

###### Abstract

We report new results on six problems in mathematics and theoretical computer science, produced with the assistance of Bolzano–an open\-source multi\-agent LLM system\. Bolzano orchestrates rounds of interaction between parallel prover agents and a verifier agent while maintaining a persistent knowledge base that is carried across rounds\. Classified using the significance–autonomy taxonomy of Feng et al\.\[[F\+26b](https://arxiv.org/html/2604.16989#bib.bibx21)\], four of the six results reach the level of publishable research, and three of the six were produced essentially autonomously by Bolzano\. Our results provide evidence that LLMs can contribute meaningfully to mathematical research, complementing recent reports by Bubeck et al\.\[[BCE\+25](https://arxiv.org/html/2604.16989#bib.bibx3)\], Woodruff et al\.\[[WCAJ\+26](https://arxiv.org/html/2604.16989#bib.bibx52)\], and others\.

## 1Introduction

The integration of large language models into mathematical research has moved rapidly from speculation to documented practice\. We highlight two recent reports that have established this as a real phenomenon \(see Related Work for many more results in this direction\):

- •Woodruff, Mirrokni et al\.\[[WCAJ\+26](https://arxiv.org/html/2604.16989#bib.bibx52)\]present a collection of case studies in which Google’s Gemini Deep Think solved open problems across mathematics, theoretical computer science, and physics\.
- •Bubeck et al\.\[[BCE\+25](https://arxiv.org/html/2604.16989#bib.bibx3)\]document experiments in which OpenAI’s GPT\-5 contributed to research in mathematics, physics, and computer science\.

This paper provides more evidence in this direction\. Bolzano\[[Bol25b](https://arxiv.org/html/2604.16989#bib.bibx10)\]is an open\-source AI system that assists with mathematical research and is available to interested researchers\. The system runs research on a problem using several rounds of interaction between several provers and a verifier\. Each prover and verifier is implemented by state\-of\-the\-art LLMs \(GPT, Gemini, Claude, or others\)\. Its architecture is described in[Section2](https://arxiv.org/html/2604.16989#S2)\. We use Bolzano to provide new results for six problems in mathematics and theoretical computer science\.

#### Strengths of Bolzano

Across our case studies, Bolzano was most useful as a generator of mathematically meaningful intermediate research moves: it was particularly good at finding counterexamples and obstructions, proposing concrete constructions and gadgets, or extending a known base case or simpler proof template to a more general statement\. This mirrors the findings in\[[WCAJ\+26](https://arxiv.org/html/2604.16989#bib.bibx52),[BCE\+25](https://arxiv.org/html/2604.16989#bib.bibx3)\]\. In one case, Bolzano autonomously provided a hardness proof and a polynomial\-time algorithm for a restricted class, and corrected a small error in the human\-provided problem formulation\.

#### Limitations

This work has several limitations\. First, we do not provide a thorough comparison between Bolzano and single\-session chatbot interactions; while such a comparison is feasible in principle, it is difficult to carry out rigorously in a case study with six problems, and the advantage of the multi\-agent architecture over direct use of the same underlying models remains unquantified\. Second, it is hard to cleanly disentangle the human and AI contributions; even selecting the right problem to work on is a nontrivial human input\.

#### Solved problems

We document six problems in mathematics and theoretical computer science that Bolzano has resolved or made progress on\. This was done either autonomously or through collaboration with domain\-expert mathematicians and computer scientists\. For each of the problems, we include discussion\. The corresponding formal results are proved either in the appendices of this paper or in separate papers\.

Table 1:Classification of our results by significance and autonomy, following the taxonomy proposed by Feng et al\.\[[F\+26b](https://arxiv.org/html/2604.16989#bib.bibx21)\]\. to landmark breakthrough\. Autonomy ranges from H \(primarily human, secondary AI input\) through C \(human–AI collaboration\) to A \(essentially autonomous\)\.1. 1\.Complexity theory:We construct an oracle separation showing that PWPP is not closed under adaptive Turing reductions \(Section[3\.1](https://arxiv.org/html/2604.16989#S3.SS1)\)\. The human input was the question, and after Bolzano returned a proof, a human researcher suggested to keep the main structure \(the same choice of problem showing that PWPP is not closed\) but try a different strategy for the analysis, after which Bolzano essentially finished the proof\.
2. 2\.Additive combinatorics:We provide an example of a tiling ofℝ2\\mathbb\{R\}^\{2\}by a single tile that shows a limit on the technique from a forthcoming paper\[[dDGGM26](https://arxiv.org/html/2604.16989#bib.bibx17)\]\(Section[3\.2](https://arxiv.org/html/2604.16989#S3.SS2)\)\.
3. 3\.Cryptography:We prove special soundness for multi\-polynomial, multi\-point KZG batching in the standard model \(Section[3\.3](https://arxiv.org/html/2604.16989#S3.SS3)\)\. The human researchers proposed a variant of the protocol and provided a simpler base\-case proof as context\. Bolzano found the full proof in six rounds, producing a lengthy but essentially complete formal argument\.
4. 4\.Data structures:We prove that two beyond worst\-case properties of heaps are equivalent \(Section[3\.4](https://arxiv.org/html/2604.16989#S3.SS4)\)\. This was first proven by a human researcher in a \(yet unpublished\) project\. Bolzano independently reproved the equivalence and independently came up with a stronger statement and its proof\.
5. 5\.Combinatorics:We disprove a conjecture on function\-preimage partitioning from the KAMAK 2020 workshop\[[Krá20](https://arxiv.org/html/2604.16989#bib.bibx38)\]\. Moreover, Bolzano establishes a corrected hypothesis and proves some bounds for it \(Section[3\.5](https://arxiv.org/html/2604.16989#S3.SS5)\)\.
6. 6\.Computational complexity:We determine the complexity of an optimization problem over the KKOS cultural dynamics model\[[KKOS16](https://arxiv.org/html/2604.16989#bib.bibx37)\]\(Section[3\.6](https://arxiv.org/html/2604.16989#S3.SS6)\)\. The decision version is NP\-complete on general graphs; on forests, we give a polynomial\-time algorithm\. Bolzano worked autonomously, also correcting a small error in the original problem formulation\.

In general, our experience parallels the findings of\[[WCAJ\+26](https://arxiv.org/html/2604.16989#bib.bibx52)\]and\[[BCE\+25](https://arxiv.org/html/2604.16989#bib.bibx3)\]in several respects\. LLMs excel at generating proof candidates, constructing counterexamples, and making cross\-domain connections\. In early 2026, human guidance remains relevant for problem selection, high\-level strategy, and verification\.

#### Related work

Recent work has begun to document the use of LLMs for mathematical and scientific research\. GPT\-5 has been shown to contribute to research in mathematics, physics, and other sciences, including solving open problems and improving constants\[[BCE\+25](https://arxiv.org/html/2604.16989#bib.bibx3)\]\. Similar results have been reported with Gemini\[[WCAJ\+26](https://arxiv.org/html/2604.16989#bib.bibx52)\]\. Aletheia\[[F\+26b](https://arxiv.org/html/2604.16989#bib.bibx21)\]is a mathematics research agent based on a Generator–Verifier–Reviser loop that autonomously solved research\-level problems, including 6 out of 10 problems in the First Proof challenge\[[FJhK\+26](https://arxiv.org/html/2604.16989#bib.bibx24)\]\. First Proof\[[ABH\+26](https://arxiv.org/html/2604.16989#bib.bibx1)\]is a benchmark of 10 research\-level problems from unpublished work of 11 mathematicians; OpenAI\[[Ope26](https://arxiv.org/html/2604.16989#bib.bibx45)\]reported at least 5 likely correct solutions\. AlphaEvolve\[[N\+25](https://arxiv.org/html/2604.16989#bib.bibx44)\]has been applied to 67 problems\[[GGSTW25](https://arxiv.org/html/2604.16989#bib.bibx26)\], mostly in constant optimization and construction search, with expert hints improving efficiency without clearly changing the ceiling of performance\. FunSearch\[[RPBN\+24](https://arxiv.org/html/2604.16989#bib.bibx48)\]pairs an LLM with an evaluator in an evolutionary loop and has produced new results in combinatorics and algorithms\.

Many systems pursue automated theorem proving with formal verification\. AlphaGeometry\[[TWL\+24](https://arxiv.org/html/2604.16989#bib.bibx49)\]solves olympiad geometry problems via a neuro\-symbolic engine\. Many recent systems target the Lean proof assistant, including AlphaProof\[[HMS\+25](https://arxiv.org/html/2604.16989#bib.bibx31)\], which achieves IMO medal\-level performance via reinforcement learning; Hilbert\[[V\+25](https://arxiv.org/html/2604.16989#bib.bibx51)\], which combines informal proof sketches with formal verification; Aleph Prover\[[Log25](https://arxiv.org/html/2604.16989#bib.bibx40)\], a formal theorem prover that leads PutnamBench; Ax\-Prover\[[B\+25](https://arxiv.org/html/2604.16989#bib.bibx2)\], which targets quantum physics and abstract algebra; and autoformalization of a 130,000\-line topology textbook at low cost\[[Urb26](https://arxiv.org/html/2604.16989#bib.bibx50)\]\. We view formal verification as complementary to our approach: Bolzano relies on informal proof generation followed by expert verification, which currently offers broader coverage but weaker guarantees\. A large\-scale evaluation of over 5,000 LLM\-generated proofs across 1,000 problems\[[D\+25](https://arxiv.org/html/2604.16989#bib.bibx16)\]finds substantially stronger performance in informal than in formal proof generation\.

Multi\-agent architectures for mathematical reasoning have been explored in several directions, including multiagent debate, step\-level verification, iterative self\-refinement, and LLM scaffolding for problem solving\[[DLT\+23](https://arxiv.org/html/2604.16989#bib.bibx18),[G\+25](https://arxiv.org/html/2604.16989#bib.bibx25),[HY25](https://arxiv.org/html/2604.16989#bib.bibx33),[MTG\+23](https://arxiv.org/html/2604.16989#bib.bibx43)\]\. In late 2025, open Erdős problems emerged as a testing ground for LLM mathematical capabilities, with models producing original proofs of previously unsolved problems\[[PSV26](https://arxiv.org/html/2604.16989#bib.bibx47),[F\+26a](https://arxiv.org/html/2604.16989#bib.bibx20)\]; however, the problems solved so far are generally amenable to straightforward techniques\[[F\+26a](https://arxiv.org/html/2604.16989#bib.bibx20)\]\.

#### Roadmap

[Section2](https://arxiv.org/html/2604.16989#S2)describes the architecture and design of Bolzano\.[Section3](https://arxiv.org/html/2604.16989#S3)presents each of the solved problems, including the problem statement, context, a discussion of the human–AI collaboration, and a link to the Bolzano transcript\. For problems whose proofs are not contained in a separate paper, the full proofs appear in the appendices\. All proofs have been verified by domain experts\.

## 2Bolzano

Bolzano is a research tool available at[https://bolzano\.app](https://bolzano.app/)\. It provides an automated pipeline consisting of*prover*,*verifier*, and*summarizer agents*designed to iteratively investigate mathematical research problems\. Throughout this section, by*agent*we mean a callable function that makes a preconfigured request to an LLM with a custom prompt specifying a research persona, tasks, and goals\.

#### Overall architecture

We call one iteration of the Bolzano pipeline a*research round*\. It involves runningnnparallel*prover agents*, followed by one*verifier agent*, and concluded by a*summarizer agent*\. Research rounds run sequentially; between rounds, the state of the investigation is preserved in three human\-readable files\.

#### Agents\.

The*prover agents*are tasked with coming up with proof ideas, finding counterexamples, proving special cases, identifying mistakes, and writing proofs\. The*verifier agent*checks the work of the provers—identifying errors and unjustified steps, combining ideas into viable solutions—and is the sole agent that decides what gets written into the knowledge base files\. The*summarizer agent*produces a concise summary of each research round for the user and for subsequent agents\.

#### Knowledge base files\.

In between research rounds, we maintain three files that serve as a persistent knowledge base\. The*notes*file aggregates insights, failed approaches, conjectures, and simplified proofs\. The*proofs*file maintains rigorous, fully detailed proofs\. The*output*file provides a short summary of the current status for the human researcher\. All agents read from these files, but only the verifier can write to them\.

#### Model diversity\.

Bolzano allows the user to select a different LLM for each prover agent\. Since models differ in training data, this seems to generate a wider variety of approaches\. This approach is also reported to counteract self\-preference bias\[[PBF24](https://arxiv.org/html/2604.16989#bib.bibx46)\]\.

#### Human guidance\.

Between research rounds, the user may provide additional instructions to steer the investigation\. In our experience, human guidance often leads to stronger results—for example, the PWPP result \([Section3\.1](https://arxiv.org/html/2604.16989#S3.SS1)\) was obtained after an expert advised Bolzano to try a different strategy\.

## 3Solved Problems

This section contains the six selected problems solved by Bolzano\. For each problem, we add discussion about what parts of the research pipeline have been done by a human, and which parts by Bolzano\. We always add a link to the Bolzano system containing the proof\. However, Bolzano\-generated proofs are not intended to be publication\-ready\. We thus always either add expert\-verified proof to appropriate appendix, or link to a paper containing the proof\.

### 3\.1Black\-Box Separation of Adaptive and Non\-Adaptive PWPP – Pavel Hubáček

The complexity class PWPP \(Polynomial Weak Pigeonhole Principle\)\[[Jeř16](https://arxiv.org/html/2604.16989#bib.bibx35)\]captures collision finding within TFNP\. Its canonical complete problemCollisionasks: given a shrinking circuitC:\{0,1\}n→\{0,1\}n−1C:\\\{0,1\\\}^\{n\}\\to\\\{0,1\\\}^\{n\-1\}, find distinctx1,x2∈\{0,1\}nx\_\{1\},x\_\{2\}\\in\\\{0,1\\\}^\{n\}such thatC​\(x1\)=C​\(x2\)C\(x\_\{1\}\)=C\(x\_\{2\}\)\. PWPP consists of all total search problems many\-one reducible toCollision\.

Jeřábek\[[Jeř16](https://arxiv.org/html/2604.16989#bib.bibx35)\]showed that PWPP is closed under*non\-adaptive*Turing reductions, i\.e\.P∥PWPP=PWPPP^\{\\\|\\mathrm\{PWPP\}\}=\\mathrm\{PWPP\}: solvingkkindependently prepared PWPP instances reduces to a single collision query\. A basic structural question for TFNP subclasses is whether they remain closed under*adaptive*Turing reductions, where later oracle queries may depend on earlier answers\[[BJ12](https://arxiv.org/html/2604.16989#bib.bibx8)\]\. For several classes \(e\.g\. PLS, PPA, PPAD\) adaptive and non\-adaptive oracle access coincide\[[BJ12](https://arxiv.org/html/2604.16989#bib.bibx8)\], while for the related class PPP \(Polynomial*strong*Pigeonhole Principle\), Fleming et al\.\[[FGPR24](https://arxiv.org/html/2604.16989#bib.bibx23)\]proved a black\-box separation showing it is not Turing\-closed\.

Together with Bolzano, in\[[Hub26](https://arxiv.org/html/2604.16989#bib.bibx32)\]we resolve the analogous question for PWPP in the black\-box setting by introducing a natural adaptive taskNestedCollision, suggested by Bolzano, which requires two dependent collision\-finding steps\.

After being given the problem, Bolzano produced the core construction and proof in four rounds of interaction\. While the initial proof had flaws, after being instructed to adopt a different high\-level strategy,111Concretely: “Discard the case analysis strategy\. Instead, prove thatΠ∉P​W​P​P𝒪\\Pi\\not\\in PWPP^\{\\mathcal\{O\}\}by establishing that, with overwhelming probability, the reduction circuit contains ”useless” collisions that do not reveal a solution toΠ\\Pi\.”Bolzano delivered a mostly complete formal proof in four additional rounds, with only minor typographical errors and no significant logical gaps\.

#### Formal results\.

The theorem proven in\[[Hub26](https://arxiv.org/html/2604.16989#bib.bibx32)\]is the following\.

###### Theorem 1\(Black\-box PWPP is not Turing\-closed\[[Hub26](https://arxiv.org/html/2604.16989#bib.bibx32)\]\)\.

In the decision\-tree model, the search problemNestedCollisionadmits no shallowCollision\-formulation\. Therefore, black\-boxPWPP\\mathrm\{PWPP\}is not closed under adaptive Turing reductions\.

The Bolzano research transcript is available at\[[Bol26d](https://arxiv.org/html/2604.16989#bib.bibx14)\]\. The complete proof appears in\[[Hub26](https://arxiv.org/html/2604.16989#bib.bibx32)\]\.

### 3\.2Structural Results on Multi\-Slope Tilings – Jan Grebík

#### Motivation and result

The problem originated in the study of*translational monotilings ofℝd\\mathbb\{R\}^\{d\}*, or less generallyℤd\\mathbb\{Z\}^\{d\}, where the setup is the following\. We are given a measurable setΩ⊆ℝd\\Omega\\subseteq\\mathbb\{R\}^\{d\}of finite positive Lebesgue measure and want to understand if there is a \(necessarily uniformly discrete\) set of translatesT⊆ℝdT\\subseteq\\mathbb\{R\}^\{d\}such that

Ω⊕T=ℝd,\\Omega\\oplus T=\\mathbb\{R\}^\{d\},whereΩ⊕T\\Omega\\oplus Tmeans that the collection of translates\{Ω\+t\}t∈T\\\{\\Omega\+t\\\}\_\{t\\in T\}are disjoint up to null sets and cover all ofℝd\\mathbb\{R\}^\{d\}\. In this case,TTis called a*tiling ofℝd\\mathbb\{R\}^\{d\}byΩ\\Omega*, andΩ\\Omegais called a*tile*\. The definitions for translational monotilings ofℤd\\mathbb\{Z\}^\{d\}are analogous\. Much of the recent development in the area\[[Bha20](https://arxiv.org/html/2604.16989#bib.bibx5),[GT21](https://arxiv.org/html/2604.16989#bib.bibx27),[GT24](https://arxiv.org/html/2604.16989#bib.bibx28),[GT25](https://arxiv.org/html/2604.16989#bib.bibx29)\]have been driven by the so\-called*periodic tiling conjecture*\.

###### Conjecture 2\(Periodic tiling conjecture \(PTC\),\[[LW96](https://arxiv.org/html/2604.16989#bib.bibx42)\]\)\.

LetΩ⊆ℝd\\Omega\\subseteq\\mathbb\{R\}^\{d\}be a tile\. Then there is a tilingTTofℝd\\mathbb\{R\}^\{d\}byΩ\\Omegathat is periodic, that is,\{γ∈ℝd:γ\+T=T\}\\\{\\gamma\\in\\mathbb\{R\}^\{d\}:\\gamma\+T=T\\\}contains a lattice\.

Unlike in the case of general tiling problems, where more tiles are allowed, PTC holds inℤ2\\mathbb\{Z\}^\{2\}which was proven by Bhattacharya\[[Bha20](https://arxiv.org/html/2604.16989#bib.bibx5)\]\. On the other hand Greenfeld and Tao\[[GT24](https://arxiv.org/html/2604.16989#bib.bibx28)\]showed that PTC fails inℤd\\mathbb\{Z\}^\{d\}\(and thusℝd\\mathbb\{R\}^\{d\}\) for large enoughdd\. Inℝ2\\mathbb\{R\}^\{2\}Kenyon\[[Ken92](https://arxiv.org/html/2604.16989#bib.bibx36)\]showed that PTC holds for tiles that are topological disks, but the general case is widely open\. Together with de Dios, Greenfeld and Madrid we investigated the case of tiles that are polygonal sets \(possibly disconnected with holes\) with edges being axes parallel that may have irrational lengths\. We obtain the following general statement, providing a weak form of PTC\.

###### Theorem 3\(\[[dDGGM26](https://arxiv.org/html/2604.16989#bib.bibx17)\]\)\.

LetΩ⊆ℝ2\\Omega\\subseteq\\mathbb\{R\}^\{2\}be an axes parallel polygonal tile\. Then there isk∈ℕk\\in\\mathbb\{N\}and a tilingT=T1⊔⋯⊔TkT=T\_\{1\}\\sqcup\\dots\\sqcup T\_\{k\}ofℝ2\\mathbb\{R\}^\{2\}byΩ\\Omegasuch that after possibly swapping the vertical and horizontal axes the following holds:

1. 1\.TiT\_\{i\}is periodic for every1≤i≤k1\\leq i\\leq k,
2. 2\.Ω⊕Ti\\Omega\\oplus T\_\{i\}is a union of cosets ofℝ​\(0,1\)\\mathbb\{R\}\(0,1\),
3. 3\.there isγ∈ℝ2∖\{0\}\\gamma\\in\\mathbb\{R\}^\{2\}\\setminus\\\{0\\\}such thatT\+γ=TT\+\\gamma=T, more specifically, ifk\>1k\>1, thenγ\\gammais of the formγ=\(0,α\)\\gamma=\(0,\\alpha\)for someα\>0\\alpha\>0\.

Note that ifk=1k=1\(or in the discrete caseℤ2\\mathbb\{Z\}^\{2\}\), then \(1\) above would already imply thatTTis periodic, thus establishing the PTC forΩ\\Omega\. Our current techniques do not seem to give any information about the possible relation betweenTiT\_\{i\}’s or the sets of the formΩ⊕Ti\\Omega\\oplus T\_\{i\}\. This leads to the question of whether there exist interesting tilings as in[Theorem3](https://arxiv.org/html/2604.16989#Thmtheorem3)\. Without any restriction, the answer to this question is trivial, as one might consider the lattice tiling ofℝ2\\mathbb\{R\}^\{2\}by a unit square\[0,1\]×\[0,1\]\[0,1\]\\times\[0,1\]and construct for anyk∈ℕk\\in\\mathbb\{N\}a tilingTTas above by shifting different columns\. In order to avoid this trivial case we need a definition\.

###### Definition 4\.

We say thatΩ⊆ℝ2\\Omega\\subseteq\\mathbb\{R\}^\{2\}*tiles a column*\(or is a*column tile*\), if there isS⊆ℝ​\(0,1\)S\\subseteq\\mathbb\{R\}\(0,1\)such thatΩ⊕S\\Omega\\oplus Sis a union of cosets ofℝ​\(0,1\)\\mathbb\{R\}\(0,1\)\.

Bolzano produced non\-column examples for Theorem[3](https://arxiv.org/html/2604.16989#Thmtheorem3), whereT=T1⊔T2T=T\_\{1\}\\sqcup T\_\{2\}and each part of the decomposition is periodic with different lattices\. This is a first step towards understanding additional flexibility that tilings ofℝ2\\mathbb\{R\}^\{2\}enjoy compared to tilings ofℤ2\\mathbb\{Z\}^\{2\}\.

###### Theorem 5\.

For every irrationalα∈\(2/3,1\)\\alpha\\in\(2/3,1\)there is an axis parallel polygonal tileΩα⊆ℝ2\\Omega\_\{\\alpha\}\\subseteq\\mathbb\{R\}^\{2\}that is not a column tile together with a tilingTα=T1,α⊔T2,αT\_\{\\alpha\}=T\_\{1,\\alpha\}\\sqcup T\_\{2,\\alpha\}ofℝ2\\mathbb\{R\}^\{2\}byΩα\\Omega\_\{\\alpha\}such that the following holds:

1. 1\.T1,αT\_\{1,\\alpha\}is\(2​ℤ\)×ℤ\(2\\mathbb\{Z\}\)\\times\\mathbb\{Z\}periodic,
2. 2\.T2,αT\_\{2,\\alpha\}is periodic with lattice\{\(2​k,k​α\+ℓ\):k,ℓ∈ℤ\}\\\{\(2k,k\\alpha\+\\ell\):k,\\ell\\in\\mathbb\{Z\}\\\},
3. 3\.Ωα⊕Ti,α\\Omega\_\{\\alpha\}\\oplus T\_\{i,\\alpha\}is a union of cosets ofℝ​\(0,1\)\\mathbb\{R\}\(0,1\)for1≤i≤21\\leq i\\leq 2,
4. 4\.TαT\_\{\\alpha\}is\(0,1\)\(0,1\)\-periodic\.

The proofs appear in[AppendixA](https://arxiv.org/html/2604.16989#A1)\. The Bolzano research transcript is available at\[[Bol26e](https://arxiv.org/html/2604.16989#bib.bibx15)\]\.

### 3\.3Special Soundness for Univariate KZG Batching – Pavel Hubáček

Polynomial Commitment Schemes \(PCS\) are a core building block of modern zero\-knowledge proofs \(zk\-SNARKs\)\. To minimize proof size and verification costs, practical systems often rely on batching techniques that allow a prover to aggregate evaluations of multiple polynomials at multiple points into a single proof\. For the popular univariate KZG commitment scheme\[[KZG10](https://arxiv.org/html/2604.16989#bib.bibx39)\], existing multi\-polynomial, multi\-point batching protocols \(e\.g\.,\[[BDFG20](https://arxiv.org/html/2604.16989#bib.bibx4)\]\) have predominantly been analyzed only in idealized settings, limiting the assurance for their practical deployments\. Proving their knowledge soundness in the standard model under falsifiable assumptions is a notoriously difficult task; the first prior standard\-model analysis was strictly limited to the simpler case of batching evaluations of many polynomials at a*single*evaluation point\[[LPS25](https://arxiv.org/html/2604.16989#bib.bibx41)\]\.

In the development of CHOPIN\[[BHKM26](https://arxiv.org/html/2604.16989#bib.bibx7)\], an optimal pairing\-based multilinear PCS, we required a fully rigorous standard\-model security proof for multi\-polynomial, multi\-point batching that was not known\. The human researchers proposed a variant of the KZG batch proof from\[[BDFG20](https://arxiv.org/html/2604.16989#bib.bibx4)\]to simplify the task of proving its*special soundness in the standard model*, the core task towards a complete proof of knowledge soundness of the scheme\. However, the human researchers did not have any rigorous proof\.

Together with Bolzano, we resolved this gap\. To assist the system, the input also contained a proof of the more basic theorem establishing the special soundness for batching KZG evaluation proofs for many polynomials at a single evaluation point from\[[LPS25](https://arxiv.org/html/2604.16989#bib.bibx41)\], streamlined by the human researchers\. After being given the problem, Bolzano found the proof of special soundness for the proposed variant of univariate KZG batching in six rounds of interaction\. The proof was lengthy and technical, but, besides minor edits in notation and presentation, it was complete and formal as verified by the authors\.

#### Formal results\.

The lemma proven in\[[BHKM26](https://arxiv.org/html/2604.16989#bib.bibx7)\]is the following\.

###### Lemma 7\(Special soundness of multi\-polynomial, multi\-point KZG batching\[[BHKM26](https://arxiv.org/html/2604.16989#bib.bibx7), Lemma 3\]\)\.

Letm,M,M′∈poly​\(λ\)m,M,M^\{\\prime\}\\in\\mathrm\{poly\}\(\\lambda\)\. LetT=⋃t=1mStT=\\bigcup\_\{t=1\}^\{m\}S\_\{t\}and letL=\|T\|\+ML=\|T\|\+M\. Assume that KZG for degree less thanMMhasMM\-special soundness in the following sense\. From any set ofM′≥MM^\{\\prime\}\\geq Maccepting KZG opening transcripts for the same commitmentCCatM′M^\{\\prime\}distinct pointsa1,…,aM′a\_\{1\},\\dots,a\_\{M^\{\\prime\}\}withaj≠τa\_\{j\}\\neq\\tau, one can extract a polynomialp∈𝔽​\[X\]<Mp\\in\\mathbb\{F\}\[X\]^\{<M\}such thatC=\[p​\(τ\)\]1C=\[p\(\\tau\)\]\_\{1\}andp​\(aj\)=yjp\(a\_\{j\}\)=y\_\{j\}for allj∈\[M′\]j\\in\[M^\{\\prime\}\]\. Then there exists an extractor that, given as input any product\-structured accepting\(m,L\)\(m,L\)\-tree𝒯=\(𝗍𝗋i​j\)i∈\[m\],j∈\[L\]\\mathcal\{T\}=\(\\mathsf\{tr\}\_\{ij\}\)\_\{i\\in\[m\],\\,j\\in\[L\]\}for the batch evaluation protocol of Figure 7 of\[[BHKM26](https://arxiv.org/html/2604.16989#bib.bibx7)\], outputs polynomialsp1,…,pm∈𝔽​\[X\]<Mp\_\{1\},\\dots,p\_\{m\}\\in\\mathbb\{F\}\[X\]^\{<M\}such thatCt=\[pt​\(τ\)\]1C\_\{t\}=\[p\_\{t\}\(\\tau\)\]\_\{1\}for allt∈\[m\]t\\in\[m\]andpt​\(z\)=ηzp\_\{t\}\(z\)=\\eta\_\{z\}for allt∈\[m\]t\\in\[m\]and allz∈Stz\\in S\_\{t\}\. Equivalently, the batch evaluation protocol is\(m,L\)\(m,L\)\-special sound with respect to product\-structured accepting transcript trees\.

The Bolzano research transcript is available at\[[Bol26b](https://arxiv.org/html/2604.16989#bib.bibx12)\]\. The complete proof appears in\[[BHKM26](https://arxiv.org/html/2604.16989#bib.bibx7)\]\.

### 3\.4Equivalence of Weak and Strong Working Set Properties for Heaps – Václav Rozhoň

The setting for this subsection is the beyond worst\-case theory of data structures, in particular heaps\. Two plausible definitions of a beyond worst\-case heap occur in the literature – the strong working set property from\[[Iac00](https://arxiv.org/html/2604.16989#bib.bibx34)\]and the weak working set property from\[[Elm06](https://arxiv.org/html/2604.16989#bib.bibx19)\]\. The strong working set property in particular has been crucial in a recent line of research\[[HHR\+23](https://arxiv.org/html/2604.16989#bib.bibx30),[Iac00](https://arxiv.org/html/2604.16989#bib.bibx34)\]\.

It was long assumed that the strong working set property was strictly stronger than the weak one\. Surprisingly, they turn out to be equivalent\. This was first proven by a human expert, but when given this task, Bolzano independently came up with a different proof and suggested a quantitative strengthening[Equation1](https://arxiv.org/html/2604.16989#S3.E1)that was not apparent from the original proof\. The strengthening gives an even tighter picture of how close the two definitions are\.

#### Formal results

Consider heaps that support the operationsInsertandExtractMin\. We study two notions of locality\-sensitive cost for such data structures\.

###### Definition 8\(Weak working set property\)\.

A heap satisfies the*weak working set property*if, for any sequence ofmmoperations, the total cost of serving them isO​\(m\+∑xlog⁡\(tx′−tx\+1\)\)O\(m\+\\sum\_\{x\}\\log\(t^\{\\prime\}\_\{x\}\-t\_\{x\}\+1\)\), where the sum is over all extracted elementsxx,txt\_\{x\}is the insertion time ofxx, andtx′t^\{\\prime\}\_\{x\}is the extraction time ofxx\.

###### Definition 9\(Strong working set property\)\.

A heap satisfies the*strong working set property*if, for any sequence ofmmoperations, the total cost of serving them isO​\(m\+∑xmaxtx≤t<tx′⁡log⁡\(\|Wt,x\|\+1\)\)O\(m\+\\sum\_\{x\}\\max\_\{t\_\{x\}\\leq t<t^\{\\prime\}\_\{x\}\}\\log\(\|W\_\{t,x\}\|\+1\)\), whereWt,xW\_\{t,x\}is the set of all elements that have been inserted after timetxt\_\{x\}and are still present at timett\.

###### Theorem 10\.

A heap has the weak working set property if and only if it has the strong one\. In fact, the following holds for anyε\>0\\varepsilon\>0\.

∑xlog⁡Lx≤\(1\+ε\)​∑xlog⁡Kx\+O​\(m/ε\)\\displaystyle\\sum\_\{x\}\\log L\_\{x\}\\leq\(1\+\\varepsilon\)\\sum\_\{x\}\\log K\_\{x\}\+O\(m/\\varepsilon\)\(1\)whereLx=tx′−tx\+1L\_\{x\}=t^\{\\prime\}\_\{x\}\-t\_\{x\}\+1is the lifetime of elementxxandKx=maxtx≤t<tx′⁡\(\|Wt,x\|\+1\)K\_\{x\}=\\max\_\{t\_\{x\}\\leq t<t^\{\\prime\}\_\{x\}\}\(\|W\_\{t,x\}\|\+1\)is its strong working set cost\.

The theorem is proven in[AppendixB](https://arxiv.org/html/2604.16989#A2)\. The Bolzano research transcript is available at\[[Bol25a](https://arxiv.org/html/2604.16989#bib.bibx9)\]\.

### 3\.5Partitioning under Function Preimage Constraints – Robert Šámal

KAMAK is a Czech problem\-solving workshop where participants propose and collect open problems in combinatorics and discrete mathematics\. The present problem appears as Problem 1 in the collection from the 2020 edition\[[Krá20](https://arxiv.org/html/2604.16989#bib.bibx38)\]\. The problems are suggested by the participants and are of various difficulty, but always meant as potentially interesting research problems\.

Consider setsEEandFF, together with functionsf1,…,fk:E→Ff\_\{1\},\\dots,f\_\{k\}:E\\to Fsatisfying*pointwise distinctness*, meaning that

fi​\(x\)≠fj​\(x\)for every​x∈E​and every​i≠j\.f\_\{i\}\(x\)\\neq f\_\{j\}\(x\)\\qquad\\text\{for every \}x\\in E\\text\{ and every \}i\\neq j\.Conjecture suggested by C\. Feghali asked whether a condition on fibre sizes forces a certain bounded partition\. \(Pointwise distinctness is obviously necessary\.\) The casek=2k=2was known and had applications in digraph coloring\[[BHB06](https://arxiv.org/html/2604.16989#bib.bibx6)\]\.

###### Conjecture 11\(Original conjecture; the casek=2k=2is known\)\.

If for everyz∈Fz\\in Fthere existst∈\{1,…,k\}t\\in\\\{1,\\dots,k\\\}with\|ft−1​\(z\)\|≤n\|f\_\{t\}^\{\-1\}\(z\)\|\\leq n, thenEEcan be partitioned into2​n\+12n\+1partsE1,…,E2​n\+1E\_\{1\},\\dots,E\_\{2n\+1\}such that

fp​\(Ei\)∩fq​\(Ei\)=∅for every​i​and every​p<q\.f\_\{p\}\(E\_\{i\}\)\\cap f\_\{q\}\(E\_\{i\}\)=\\emptyset\\qquad\\text\{for every \}i\\text\{ and every \}p<q\.

A convenient way to view the problem is through the*conflict graph*on vertex setEE, in which distinctx,y∈Ex,y\\in Eare adjacent wheneverfp​\(x\)=fq​\(y\)f\_\{p\}\(x\)=f\_\{q\}\(y\)for somep≠qp\\neq q\. Then a partition with the required disjointness property is exactly a proper coloring of this graph\. Bolzano’s first contribution was to observe that fork≥3k\\geq 3the original hypothesis can be satisfied vacuously: a dummy function may have empty fibers and thus the remaining functions are not controlled\.

This leads to the following negative result\.

###### Theorem 12\(Counterexample to the original conjecture\)\.

For everyn≥1n\\geq 1and everyM≥1M\\geq 1, there exist setsE,FE,Fand functionsf1,f2,f3:E→Ff\_\{1\},f\_\{2\},f\_\{3\}:E\\to Fsuch that:

1. 1\.fi​\(x\)≠fj​\(x\)f\_\{i\}\(x\)\\neq f\_\{j\}\(x\)for allx∈Ex\\in Eand alli≠ji\\neq j;
2. 2\.for everyz∈Fz\\in Fthere existst∈\{1,2,3\}t\\in\\\{1,2,3\\\}with\|ft−1​\(z\)\|≤n\|f\_\{t\}^\{\-1\}\(z\)\|\\leq n;
3. 3\.every partition ofEEsatisfying fp​\(Ei\)∩fq​\(Ei\)=∅for all​i​and all​p<qf\_\{p\}\(E\_\{i\}\)\\cap f\_\{q\}\(E\_\{i\}\)=\\emptyset\\qquad\\text\{for all \}i\\text\{ and all \}p<qrequires more thanMMparts\.

The construction realizes the conflict graph as a shift graph, whose chromatic number is unbounded\. The full proof appears in Appendix[C](https://arxiv.org/html/2604.16989#A3)\.

The counterexample suggests that the right assumption is not to control single fibers, but to control them*pairwise*\. This leads to the following notion,*also suggested by Bolzano\.*

###### Definition 13\(Pairwisenn\-boundedness\)\.

The functionsf1,…,fk:E→Ff\_\{1\},\\dots,f\_\{k\}:E\\to Fare*pairwisenn\-bounded*if for everyz∈Fz\\in Fand every pairp≠qp\\neq q,

min⁡\(\|fp−1​\(z\)\|,\|fq−1​\(z\)\|\)≤n\.\\min\\bigl\(\|f\_\{p\}^\{\-1\}\(z\)\|,\\;\|f\_\{q\}^\{\-1\}\(z\)\|\\bigr\)\\leq n\.

Under this stronger hypothesis one gets a positive result\.

###### Theorem 14\(Pairwisenn\-boundedness implies bounded partition\)\.

Assume pointwise distinctness and pairwisenn\-boundedness\. ThenEEcan be partitioned into2​n​k​\(k−1\)\+12nk\(k\-1\)\+1partsE1,…,E2​n​k​\(k−1\)\+1E\_\{1\},\\dots,E\_\{2nk\(k\-1\)\+1\}such that

fp​\(Ei\)∩fq​\(Ei\)=∅for every​i​and every​p<q\.f\_\{p\}\(E\_\{i\}\)\\cap f\_\{q\}\(E\_\{i\}\)=\\emptyset\\qquad\\text\{for every \}i\\text\{ and every \}p<q\.

The proof orients each conflict toward the endpoint whose side of the witnessing equality comes from a small fiber, thereby obtaining a bounded\-indegree orientation of the conflict graph\. This implies bounded degeneracy and hence bounded chromatic number\. Appendix[C](https://arxiv.org/html/2604.16989#A3)contains the full proof, together with a stronger bound under uniformnn\-boundedness and complementary lower\-bound constructions\.

The Bolzano research transcript is available at\[[Bol26c](https://arxiv.org/html/2604.16989#bib.bibx13)\]\.

### 3\.6Complexity of Optimization in KKOS Cultural Dynamics – Martin Koutecký

Kempe, Kleinberg, Oren, and Slivkins\[[KKOS16](https://arxiv.org/html/2604.16989#bib.bibx37)\]introduced a model of cultural dynamics in which agents on a social network update their opinions to reduce disagreement with neighbors\. In their*local model*, the equilibrium condition requires that neighboring agents in the support of a distribution experience equal “mass” – that is, the total weight in their closed neighborhood is the same\.

It is natural \(especially motivated by bribery\-type viewpoints, see\[[FGKT22](https://arxiv.org/html/2604.16989#bib.bibx22)\]\) to consider the problem of finding a closest equilibriumxxto a given \(arbitrary\) distributionyy\. Formally, given an undirected graphG=\(V,E\)G=\(V,E\)with adjacency matrixA′A^\{\\prime\}, setA=A′\+IA=A^\{\\prime\}\+I\(adding self\-loops\), and given an initial distributiony∈ℝ≥0Vy\\in\\mathbb\{R\}\_\{\\geq 0\}^\{V\}with‖y‖1=1\\\|y\\\|\_\{1\}=1and a cost vectorc∈ℝ≥0Vc\\in\\mathbb\{R\}\_\{\\geq 0\}^\{V\}, the task is to find a distributionx∈ℝ≥0Vx\\in\\mathbb\{R\}\_\{\\geq 0\}^\{V\}with∑vxv=1\\sum\_\{v\}x\_\{v\}=1minimizing∑vcv​\|xv−yv\|\\sum\_\{v\}c\_\{v\}\|x\_\{v\}\-y\_\{v\}\|subject to the constraint that for every edgeu​v∈Euv\\in E, ifxu,xv\>0x\_\{u\},x\_\{v\}\>0then\(A​x\)u=\(A​x\)v\(Ax\)\_\{u\}=\(Ax\)\_\{v\}\.

Bolzano worked on this problem autonomously over three rounds\. In Round 1, Bolzano found a clean NP\-hardness proof via a reduction fromClique: adding a universal vertex forces any feasible support to be a clique, and theℓ1\\ell\_\{1\}cost becomes monotone in the clique size\. In Round 2, Bolzano established membership in NP \(via an LP\-based polynomial certificate\), corrected a small error in the original problem formulation,222The task statement asserted that for a fixed supportSS, one can compute a cost\-minimizing vector by linear programming\. This is not true in the straightforward LP formulation because the exact\-support constraint involves strict inequalities, so the feasible region can be open\. Bolzano provided a counterexample and a correct reformulation using a max\-margin LP\.and proved structural results for chordal graphs and forests\. In Round 3, Bolzano designed a polynomial\-timeO​\(n2\)O\(n^\{2\}\)algorithm for forests via dynamic programming on dissociation sets\.

#### Formal results\.

###### Theorem 15\(NP\-completeness\)\.

Under the standard binary encoding of rational inputs, the decision version of the KKOS optimization problem is NP\-complete\. NP\-hardness holds even with unit costs, positive rationalyy, and a universal vertex\. The optimization problem is NP\-hard\.

###### Proposition 16\(Forest characterization\)\.

On a forest, the feasible supports are exactly the dissociation sets, i\.e\., the vertex setsSSsuch thatG​\[S\]G\[S\]has maximum degree at most11\.

###### Theorem 17\(Polynomial\-time algorithm for forests\)\.

IfGGis a forest, the optimization problem can be solved inO​\(n2\)O\(n^\{2\}\)time\. The forest\-restricted decision problem is inPP\.

The proofs appear in[AppendixD](https://arxiv.org/html/2604.16989#A4)\. The Bolzano research transcript is available at\[[Bol26a](https://arxiv.org/html/2604.16989#bib.bibx11)\]\.

## Acknowledgements

We thank Tomáš Gavenčiak and Vojtěch Rozhoň for helpful discussions and for their contributions to the development of the Bolzano system\. JG, VR, and AZ were supported by the Czech Science Foundation \(GA ČR\), project No\. 26\-23599M\. RŠ was supported by grant no\.25\-16627S from the Czech Science Foundation \(GAČR\)\. MK was supported by grant no\.25\-17221S from the Czech Science Foundation \(GAČR\)\.

## References

- \[ABH\+26\]Mohammed Abouzaid, Andrew J\. Blumberg, Martin Hairer, Joe Kileel, Tamara G\. Kolda, Paul D\. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, and Lauren Williams\.First Proof, 2026\.
- \[B\+25\]Benjamin Breen et al\.Ax\-Prover: A deep reasoning agentic framework for theorem proving in mathematics and quantum physics, 2025\.
- \[BCE\+25\]Sébastien Bubeck, Christian Coester, Ronen Eldan, Timothy Gowers, Yin Tat Lee, Alexandru Lupsasca, Mehtaab Sawhney, Robert Scherrer, Mark Sellke, Brian K\. Spears, Derya Unutmaz, Kevin Weil, Steven Yin, and Nikita Zhivotovskiy\.Early science acceleration experiments with GPT\-5, 2025\.
- \[BDFG20\]Dan Boneh, Justin Drake, Ben Fisch, and Ariel Gabizon\.Efficient polynomial commitment schemes for multiple points and polynomials\.IACR Cryptol\. ePrint Arch\., page 81, 2020\.
- \[Bha20\]Siddhartha Bhattacharya\.Periodicity and decidability of tilings ofℤ2\\mathbb\{Z\}^\{2\}\.American Journal of Mathematics, 142\(1\):255–266, 2020\.
- \[BHB06\]S\. Bessy, F\. Havet, and E\. Birmelé\.Arc\-chromatic number of digraphs in which every vertex has bounded outdegree or bounded indegree\.J\. Graph Theory, 53\(4\):315–332, December 2006\.
- \[BHKM26\]Juraj Belohorec, Pavel Hubáček, Aleksi Kalsta, and Kristýna Mašková\.CHOPIN: Optimal pairing\-based multilinear polynomial commitments from bivariate KZG\.IACR Cryptol\. ePrint Arch\., page 480, 2026\.[https://eprint\.iacr\.org/archive/2026/480/20260308:102759](https://eprint.iacr.org/archive/2026/480/20260308:102759)\.
- \[BJ12\]Samuel R\. Buss and Alan S\. Johnson\.Propositional proofs and reductions between NP search problems\.Annals of Pure and Applied Logic, 163\(9\):1163–1182, 2012\.
- \[Bol25a\]Bolzano transcript: Heap equivalence\.[https://bolzano\.app/heap\-equivalence](https://bolzano.app/heap-equivalence), 2025\.
- \[Bol25b\]Bolzano Team\.Bolzano\.[https://bolzano\.app/](https://bolzano.app/), 2025\.
- \[Bol26a\]Bolzano transcript: KKOS optimization\.[https://bolzano\.app/kkos\-optimization](https://bolzano.app/kkos-optimization), 2026\.
- \[Bol26b\]Bolzano transcript: KZG batching\.[https://bolzano\.app/kzg\-batching](https://bolzano.app/kzg-batching), 2026\.
- \[Bol26c\]Bolzano transcript: Function\-preimage partitioning\.[https://bolzano\.app/function\-preimage\-partitioning](https://bolzano.app/function-preimage-partitioning), 2026\.
- \[Bol26d\]Bolzano transcript: PWPP separation\.[https://bolzano\.app/pwpp\-separation](https://bolzano.app/pwpp-separation), 2026\.
- \[Bol26e\]Bolzano transcript: Multi\-slope tilings\.[https://bolzano\.app/multi\-slope\-tilings](https://bolzano.app/multi-slope-tilings), 2026\.
- \[D\+25\]Jasper Dekoninck et al\.The Open Proof Corpus: A large\-scale study of LLM\-generated mathematical proofs, 2025\.
- \[dDGGM26\]Jaume de Dios Pont, Jan Grebík, Rachel Greenfeld, and José Madrid\.Translational tilings by axes\-parallel polygonal sets\.Work in progress, 2026\.
- \[DLT\+23\]Yilun Du, Shuang Li, Antonio Torralba, Joshua B\. Tenenbaum, and Igor Mordatch\.Improving factuality and reasoning in language models through multiagent debate, 2023\.
- \[Elm06\]Amr Elmasry\.A priority queue with the working\-set property\.Int\. J\. Found\. Comput\. Sci\., 17\(6\):1455–1466, 2006\.
- \[F\+26a\]Tony Feng et al\.Semi\-autonomous mathematics discovery with Gemini: A case study on the Erdős problems, 2026\.
- \[F\+26b\]Tony Feng et al\.Towards autonomous mathematics research, 2026\.
- \[FGKT22\]Piotr Faliszewski, Rica Gonen, Martin Koutecký, and Nimrod Talmon\.Opinion diffusion and campaigning on society graphs\.J\. Log\. Comput\., 32\(6\):1162–1194, 2022\.
- \[FGPR24\]Noah Fleming, Stefan Grosser, Toniann Pitassi, and Robert Robere\.Black\-box PPP is not Turing\-closed\.InProceedings of the 56th Annual ACM Symposium on Theory of Computing \(STOC\), pages 1405–1414, 2024\.
- \[FJhK\+26\]Tony Feng, Junehyuk Jung, Sang hyun Kim, Carlo Pagano, et al\.Aletheia tackles FirstProof autonomously, 2026\.
- \[G\+25\]Jiaxing Guo et al\.Right is not enough: The pitfalls of outcome supervision in training LLMs for math reasoning, 2025\.
- \[GGSTW25\]Bogdan Georgiev, Javier Gómez\-Serrano, Terence Tao, and Adam Zsolt Wagner\.Mathematical exploration and discovery at scale, 2025\.
- \[GT21\]Rachel Greenfeld and Terence Tao\.The Structure of Translational Tilings inℤd\\mathbb\{Z\}^\{d\}\.Discrete Analysis, 2021\.
- \[GT24\]Rachel Greenfeld and Terence Tao\.A counterexample to the periodic tiling conjecture\.Annals of Mathematics, 200\(1\):301–363, 2024\.
- \[GT25\]Rachel Greenfeld and Terence Tao\.Undecidability of translational monotilings\.J\. Eur\. Math\. Soc\., 2025\.
- \[HHR\+23\]Bernhard Haeupler, Richard Hladík, Václav Rozhoň, Robert Tarjan, and Jakub Tětek\.Universal optimality of Dijkstra via beyond\-worst\-case heaps, 2023\.
- \[HMS\+25\]Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z\. Horváth, et al\.Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature, 2025\.
- \[Hub26\]Pavel Hubáček\.Black\-box PWPP is not Turing closed\.CoRR, abs/2602\.23809, 2026\.[https://doi\.org/10\.48550/arXiv\.2602\.23809](https://doi.org/10.48550/arXiv.2602.23809)\.
- \[HY25\]Hao Huang and Lin F\. Yang\.Winning gold at IMO 2025 with a model\-agnostic verification\-and\-refinement pipeline, 2025\.
- \[Iac00\]John Iacono\.Improved upper bounds for pairing heaps\.InScandinavian Workshop on Algorithm Theory, pages 32–45\. Springer, 2000\.
- \[Jeř16\]Emil Jeřábek\.Integer factoring and modular square roots\.Journal of Computer and System Sciences, 82\(2\):380–394, 2016\.
- \[Ken92\]Richard Kenyon\.Rigidity of planar tilings\.Inventiones Mathematicae, 107\(3\):637–651, 1992\.
- \[KKOS16\]David Kempe, Jon M\. Kleinberg, Sigal Oren, and Aleksandrs Slivkins\.Selection and influence in cultural dynamics\.Netw\. Sci\., 4\(1\):1–27, 2016\.
- \[Krá20\]Karel Král\.Open problems\.[https://kam\.mff\.cuni\.cz/~kamak/static/problems/2020\.pdf](https://kam.mff.cuni.cz/~kamak/static/problems/2020.pdf), 2020\.KAMAK Problem Solving Workshop\.
- \[KZG10\]Aniket Kate, Gregory M\. Zaverucha, and Ian Goldberg\.Constant\-size commitments to polynomials and their applications\.In Masayuki Abe, editor,Advances in Cryptology \- ASIACRYPT 2010 \- 16th International Conference on the Theory and Application of Cryptology and Information Security, Singapore, December 5\-9, 2010\. Proceedings, volume 6477 ofLecture Notes in Computer Science, pages 177–194\. Springer, 2010\.
- \[Log25\]Logical Intelligence\.Aleph Prover, 2025\.[https://logicalintelligence\.com/aleph\-prover\.html](https://logicalintelligence.com/aleph-prover.html)\.
- \[LPS25\]Helger Lipmaa, Roberto Parisella, and Janno Siim\.On knowledge\-soundness of Plonk in ROM from falsifiable assumptions\.In Yael Tauman Kalai and Seny F\. Kamara, editors,Advances in Cryptology \- CRYPTO 2025 \- 45th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 17\-21, 2025, Proceedings, Part VII, volume 16006 ofLecture Notes in Computer Science, pages 362–395\. Springer, 2025\.
- \[LW96\]Jeffrey C\. Lagarias and Yang Wang\.Tiling the line with translates of one tile\.Inventiones Mathematicae, 124\(1–3\):341–365, 1996\.
- \[MTG\+23\]Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, et al\.Self\-refine: Iterative refinement with self\-feedback\.arXiv preprint arXiv:2303\.17651, 2023\.
- \[N\+25\]Alexander Novikov et al\.AlphaEvolve: A coding agent for scientific and algorithmic discovery, 2025\.
- \[Ope26\]OpenAI\.Our First Proof submissions\.[https://openai\.com/index/first\-proof\-submissions/](https://openai.com/index/first-proof-submissions/), 2026\.
- \[PBF24\]Arjun Panickssery, Samuel R\. Bowman, and Shi Feng\.LLM evaluators recognize and favor their own generations, 2024\.
- \[PSV26\]Moe Putterman, Mehtaab Sawhney, and Gregory Valiant\.On infinite sets with no 3 on a line, 2026\.
- \[RPBN\+24\]Bernardino Romera\-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M\. Pawan Kumar, Emilien Dupont, Francisco J\. R\. Ruiz, Jordan S\. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi\.Mathematical discoveries from program search with large language models\.Nature, 625\(7995\):468–475, 2024\.
- \[TWL\+24\]Trieu H\. Trinh, Yuhuai Wu, Quoc V\. Le, He He, and Thang Luong\.Solving olympiad geometry without human demonstrations\.Nature, 625\(7995\):476–482, 2024\.
- \[Urb26\]Josef Urban\.130k lines of formal topology in two weeks: Simple and cheap autoformalization for everyone?, 2026\.
- \[V\+25\]Sumanth Varambally et al\.Hilbert: Recursively building formal proofs with informal reasoning, 2025\.
- \[WCAJ\+26\]David P\. Woodruff, Vincent Cohen\-Addad, Lalit Jain, Jieming Mao, Song Zuo, et al\.Accelerating scientific research with Gemini: Case studies and common techniques, 2026\.

## Appendix AStructural Results on Multi\-Slope Tilings

This appendix contains the proofs of[Theorem5](https://arxiv.org/html/2604.16989#Thmtheorem5)from[Section3\.2](https://arxiv.org/html/2604.16989#S3.SS2)\.

The periodicity in[Theorem3](https://arxiv.org/html/2604.16989#Thmtheorem3)allows to simplify the problem by working in the groupG=ℤ×𝕋G=\\mathbb\{Z\}\\times\\mathbb\{T\}, where𝕋:=ℝ/ℤ\\mathbb\{T\}:=\\mathbb\{R\}/\\mathbb\{Z\}, with counting measure onℤ\\mathbb\{Z\}and normalized Lebesgue measureμ\\muonℝ/ℤ\\mathbb\{R\}/\\mathbb\{Z\}\. Addition is componentwise, that is,\(m,θ\)\+\(n,φ\)=\(m\+n,θ\+φ\)\(m,\\theta\)\+\(n,\\varphi\)=\(m\+n,\\,\\theta\+\\varphi\)\. All equalities, coverings, and disjointness statements are understood a\.e\. with respect to the product measure\.

In this setup, we work with measurable setsA⊂GA\\subset Gof the formA=⋃i=1ℓ\{ni\}×IiA=\\bigcup\_\{i=1\}^\{\\ell\}\\\{n\_\{i\}\\\}\\times I\_\{i\}withni∈ℤn\_\{i\}\\in\\mathbb\{Z\}distinct and eachIi⊂𝕋I\_\{i\}\\subset\\mathbb\{T\}a half\-open interval\. The*integer support*ofAAissupp⁡\(A\):=\{ni:1≤i≤ℓ\}\\operatorname\{supp\}\(A\):=\\\{n\_\{i\}:1\\leq i\\leq\\ell\\\}, and the*fiber*atnnisAn:=\{t∈𝕋:\(n,t\)∈A\}A\_\{n\}:=\\\{t\\in\\mathbb\{T\}:\(n,t\)\\in A\\\}\. A setT⊂GT\\subset Gis a*tiling ofGGbyAA*ifA\+T=GA\+T=Gand the translates\{A\+t\}t∈T\\\{A\+t\\\}\_\{t\\in T\}are pairwise disjoint up to null sets\. This is denoted asA⊕T=GA\\oplus T=G\. IfA⊕T=GA\\oplus T=G, thenAAis called a*tile*\.

Analogously to Definition[4](https://arxiv.org/html/2604.16989#Thmtheorem4), a setA⊆GA\\subseteq Gis a*column tile*if there exist finite setsC⊂ℤC\\subset\\mathbb\{Z\}andΛ⊂𝕋\\Lambda\\subset\\mathbb\{T\}such thatA⊂C×𝕋A\\subset C\\times\\mathbb\{T\}and the vertical translates\{A\+\(0,λ\):λ∈Λ\}\\\{A\+\(0,\\lambda\):\\lambda\\in\\Lambda\\\}tileC×𝕋C\\times\\mathbb\{T\}\.

### A\.1Auxiliary claims

###### Lemma 19\(Multi\-coset affine arithmetic\-splitting criterion\)\.

Letq≥1q\\geq 1, andH⊂q​ℤH\\subset q\\mathbb\{Z\}be a finite set of distinct integers\. LetJh⊂𝕋J\_\{h\}\\subset\\mathbb\{T\}be measurable for eachh∈Hh\\in H, andβr,αr∈𝕋\\beta\_\{r\},\\alpha\_\{r\}\\in\\mathbb\{T\}for each0≤r≤q−10\\leq r\\leq q\-1\. Define

A:=⋃h∈H\(\{h\}×Jh\)⊂G​and​Tr:=\{\(q​k\+r,βr\+k​αr\):k∈ℤ\}⊂G​for each​0≤r≤q−1\.A:=\\bigcup\_\{h\\in H\}\(\\\{h\\\}\\times J\_\{h\}\)\\subset G\\text\{ and \}T\_\{r\}:=\\\{\(qk\+r,\\beta\_\{r\}\+k\\alpha\_\{r\}\):k\\in\\mathbb\{Z\}\\\}\\subset G\\text\{ for each \}0\\leq r\\leq q\-1\.Then the following are equivalent:

1. 1\.A⊕T=GA\\oplus T=GwhereT=⋃r=0q−1TrT=\\bigcup\_\{r=0\}^\{q\-1\}T\_\{r\},
2. 2\.for everyr∈Rr\\in R, one has the circle partition identity ⨆h∈H\(Jh−hq​αr\)=𝕋a\.e\.\\bigsqcup\_\{h\\in H\}\\Bigl\(J\_\{h\}\-\\frac\{h\}\{q\}\\alpha\_\{r\}\\Bigr\)=\\mathbb\{T\}\\quad\\text\{a\.e\.\}

###### Proof\.

First observe that if1≤r≤q−11\\leq r\\leq q\-1andt=\(q​k\+r,βr\+k​αr\)∈Trt=\(qk\+r,\\beta\_\{r\}\+k\\alpha\_\{r\}\)\\in T\_\{r\}, thenA\+t⊆\(q​ℤ\+r\)×𝕋A\+t\\subseteq\(q\\mathbb\{Z\}\+r\)\\times\\mathbb\{T\}\. Hence, it is enough to understand each fixed1≤r≤q−11\\leq r\\leq q\-1separately\.

Form∈ℤm\\in\\mathbb\{Z\}, define the set

Fr,m=\{θ∈𝕋:\(r\+q​m,θ\)∈A\+Tr\}\.F\_\{r,m\}=\\\{\\theta\\in\\mathbb\{T\}:\(r\+qm,\\theta\)\\in A\+T\_\{r\}\\\}\.A point\(r\+q​m,θ\)\(r\+qm,\\theta\)lies inA\+\(q​k\+r,βr\+k​αr\)A\+\(qk\+r,\\beta\_\{r\}\+k\\alpha\_\{r\}\)for somek∈ℤk\\in\\mathbb\{Z\}if and only if there existsh∈Hh\\in Hsuch that

- •q​\(m−k\)=hq\(m\-k\)=h, and
- •θ∈Jh\+βr\+k​αr\\theta\\in J\_\{h\}\+\\beta\_\{r\}\+k\\alpha\_\{r\}\.

Becauseh∈q​ℤh\\in q\\mathbb\{Z\}, the above equation has the unique solutionk=m−hqk=m\-\\frac\{h\}\{q\}\. Substituting this into the vertical condition givesθ∈\(Jh−hq​αr\)\+βr\+m​αr\\theta\\in\\Bigl\(J\_\{h\}\-\\frac\{h\}\{q\}\\alpha\_\{r\}\\Bigr\)\+\\beta\_\{r\}\+m\\alpha\_\{r\}\. This gives

Fr,m=\(⋃h∈H\(Jh−hq​αr\)\)\+βr\+m​αr\.F\_\{r,m\}=\\left\(\\bigcup\_\{h\\in H\}\\Bigl\(J\_\{h\}\-\\frac\{h\}\{q\}\\alpha\_\{r\}\\Bigr\)\\right\)\+\\beta\_\{r\}\+m\\alpha\_\{r\}\.\(2\)Now we are ready to show the equivalence\.

\(2\)⇒\(1\)\(2\)\\Rightarrow\(1\)\. Let1≤r≤q−11\\leq r\\leq q\-1andm∈ℤm\\in\\mathbb\{Z\}\. Since translation on𝕋\\mathbb\{T\}preserves Lebesgue measure and preserves pairwise disjointness a\.e\., the assumed partition identity impliesFr,m=𝕋F\_\{r,m\}=\\mathbb\{T\}a\.e\., and the pieces contributing to \([2](https://arxiv.org/html/2604.16989#A1.E2)\) are pairwise disjoint a\.e\. Asm∈ℤm\\in\\mathbb\{Z\}was arbitrary, we get thatA⊕Tr=\(q​ℤ\+r\)×𝕋A\\oplus T\_\{r\}=\(q\\mathbb\{Z\}\+r\)\\times\\mathbb\{T\}\. This proves \(1\) by the remark in the beginning of this proof\.

\(1\)⇒\(2\)\(1\)\\Rightarrow\(2\)\. By the remark in the beginning of the proof and the assumption, we have that \([2](https://arxiv.org/html/2604.16989#A1.E2)\) reads as

𝕋=Fr,0=\(⨆h∈H\(Jh−hq​αr\)\)\+βr\.\\mathbb\{T\}=F\_\{r,0\}=\\left\(\\bigsqcup\_\{h\\in H\}\\Bigl\(J\_\{h\}\-\\frac\{h\}\{q\}\\alpha\_\{r\}\\Bigr\)\\right\)\+\\beta\_\{r\}\.for every1≤r≤q−11\\leq r\\leq q\-1andm=0m=0\. Shifting by−βr\-\\beta\_\{r\}gives \(2\)\. ∎

###### Proposition 20\(Fiberwise criterion for column tiles\)\.

LetA=⋃i=1ℓ\{ni\}×Ii⊆ℤ×𝕋A=\\bigcup\_\{i=1\}^\{\\ell\}\\\{n\_\{i\}\\\}\\times I\_\{i\}\\subseteq\\mathbb\{Z\}\\times\\mathbb\{T\}be a column tile\. Then there isk∈ℕk\\in\\mathbb\{N\}such that

μ​\(Ani\)=1/k\\mu\\left\(A\_\{n\_\{i\}\}\\right\)=1/kfor every1≤i≤ℓ1\\leq i\\leq\\ell\.

###### Proof\.

By the definition, there areC⊂ℤC\\subset\\mathbb\{Z\}and a finite nonempty setΛ⊂𝕋\\Lambda\\subset\\mathbb\{T\}such that the translates\{A\+\(0,λ\):λ∈Λ\}\\\{A\+\(0,\\lambda\):\\lambda\\in\\Lambda\\\}are pairwise disjoint a\.e\., and⨆λ∈Λ\(A\+\(0,λ\)\)=C×𝕋\\bigsqcup\_\{\\lambda\\in\\Lambda\}\(A\+\(0,\\lambda\)\)=C\\times\\mathbb\{T\}\.

For each1≤i≤ℓ1\\leq i\\leq\\ell, observe that𝕋=⨆λ∈ΛAni\+λ\\mathbb\{T\}=\\bigsqcup\_\{\\lambda\\in\\Lambda\}A\_\{n\_\{i\}\}\+\\lambda\. Therefore

1=μ​\(𝕋\)=∑λ∈Λμ​\(Ani\+λ\)=\|Λ\|​μ​\(Ani\)1=\\mu\(\\mathbb\{T\}\)=\\sum\_\{\\lambda\\in\\Lambda\}\\mu\(A\_\{n\_\{i\}\}\+\\lambda\)=\|\\Lambda\|\\mu\(A\_\{n\_\{i\}\}\)as Lebesgue measure is translation\-invariant\. ∎

### A\.2Explicit construction

Choose an irrationalε∈\(0,1/3\)\\varepsilon\\in\(0,1/3\)and define:

- •α=1−ε\\alpha=1\-\\varepsilon,
- •I0:=\[ε,2​ε\)I\_\{0\}:=\[\\varepsilon,2\\varepsilon\),I2:=\[2​ε,1\)I\_\{2\}:=\[2\\varepsilon,1\),I4:=\[0,ε\)I\_\{4\}:=\[0,\\varepsilon\),
- •Aα=\(\{0\}×I0\)∪\(\{2\}×I2\)∪\(\{4\}×I4\)⊂ℤ×𝕋A\_\{\\alpha\}=\(\\\{0\\\}\\times I\_\{0\}\)\\cup\(\\\{2\\\}\\times I\_\{2\}\)\\cup\(\\\{4\\\}\\times I\_\{4\}\)\\subset\\mathbb\{Z\}\\times\\mathbb\{T\},
- •S1,α:=\{\(2​k,0\):k∈ℤ\}S\_\{1,\\alpha\}:=\\\{\(2k,0\):k\\in\\mathbb\{Z\}\\\}andS2,α:=\{\(2​k\+1,k​α\):k∈ℤ\}\.S\_\{2,\\alpha\}:=\\\{\(2k\+1,k\\alpha\):k\\in\\mathbb\{Z\}\\\}\.

We show thatAα⊕Sα=GA\_\{\\alpha\}\\oplus S\_\{\\alpha\}=GwhereSα=S1,α⊔S2,αS\_\{\\alpha\}=S\_\{1,\\alpha\}\\sqcup S\_\{2,\\alpha\}\. We verify \(2\) in Lemma[A\.1](https://arxiv.org/html/2604.16989#A1.SS1)withq=2q=2,β0=β1=0\\beta\_\{0\}=\\beta\_\{1\}=0,α0=0\\alpha\_\{0\}=0andα1=α\\alpha\_\{1\}=\\alpha\. Forr=0r=0, we have

⨆2​i∈\{0,2,4\}I2​i=\[ε,2​ε\)⊔\[2​ε,1\)⊔\[0,ε\)=𝕋,\\bigsqcup\_\{2i\\in\\\{0,2,4\\\}\}I\_\{2i\}=\[\\varepsilon,2\\varepsilon\)\\sqcup\[2\\varepsilon,1\)\\sqcup\[0,\\varepsilon\)=\\mathbb\{T\},and forr=1r=1, we have

⨆2​i∈\{0,2,4\}\(I2​i−i​α\)=\[ε,2​ε\)⊔\(\[2​ε,1\)−\(1−ϵ\)\)⊔\(\[0,ε\)−2​\(1−ϵ\)\)=\[ε,2ε\)⊔\(\[0,ϵ\)⊔\[3ϵ,1\)\)⊔\(\[2ϵ,3ε\)=𝕋,\\begin\{split\}\\bigsqcup\_\{2i\\in\\\{0,2,4\\\}\}\\Bigl\(I\_\{2i\}\-i\\alpha\\Bigr\)=&\\ \[\\varepsilon,2\\varepsilon\)\\sqcup\(\[2\\varepsilon,1\)\-\(1\-\\epsilon\)\)\\sqcup\(\[0,\\varepsilon\)\-2\(1\-\\epsilon\)\)\\\\ =&\\ \[\\varepsilon,2\\varepsilon\)\\sqcup\(\[0,\\epsilon\)\\sqcup\[3\\epsilon,1\)\)\\sqcup\(\[2\\epsilon,3\\varepsilon\)\\\\ =&\\ \\mathbb\{T\},\\end\{split\}where\[2​ε,1\)−\(1−ϵ\)=\[0,ϵ\)⊔\[3​ϵ,1\)\[2\\varepsilon,1\)\-\(1\-\\epsilon\)=\[0,\\epsilon\)\\sqcup\[3\\epsilon,1\)follows from the assumption thatϵ∈\(0,1/3\)\\epsilon\\in\(0,1/3\)\.

Observe that, by Proposition[20](https://arxiv.org/html/2604.16989#Thmtheorem20),AAis not a column tile asμ​\(A∩\(\{0\}×𝕋\)\)\\mu\(A\\cap\(\\\{0\\\}\\times\\mathbb\{T\}\)\)is not rational\.

### A\.3Proof of Theorem[5](https://arxiv.org/html/2604.16989#Thmtheorem5)

Given an irrationalα∈\(2/3,1\)\\alpha\\in\(2/3,1\), consider the tileAα⊆ℤ×𝕋A\_\{\\alpha\}\\subseteq\\mathbb\{Z\}\\times\\mathbb\{T\}described above, and define

Ωα=\{\(n,x\)\+\(t,0\):x,t∈\[0,1\)​and​\(n,x\)∈Aα\}⊆ℝ2\.\\Omega\_\{\\alpha\}=\\\{\(n,x\)\+\(t,0\):x,t\\in\[0,1\)\\text\{ and \}\(n,x\)\\in A\_\{\\alpha\}\\\}\\subseteq\\mathbb\{R\}^\{2\}\.It follows from the properties ofAαA\_\{\\alpha\}andSαS\_\{\\alpha\}thatΩα\\Omega\_\{\\alpha\}does not tile a column, and thatTα=T1,α⊔T2,αT\_\{\\alpha\}=T\_\{1,\\alpha\}\\sqcup T\_\{2,\\alpha\}, whereT1,α=\(2​ℤ\)×ℤT\_\{1,\\alpha\}=\(2\\mathbb\{Z\}\)\\times\\mathbb\{Z\}andT2,α=\{\(2​k,k​α\+ℓ\):k,ℓ∈ℤ\}T\_\{2,\\alpha\}=\\\{\(2k,k\\alpha\+\\ell\):k,\\ell\\in\\mathbb\{Z\}\\\}, have all the desired properties\.

## Appendix BEquivalence of Weak and Strong Working Set Properties

In this appendix we prove the equivalence between the weak and strong working set properties stated in[Section3\.4](https://arxiv.org/html/2604.16989#S3.SS4)\. In fact, we prove the stronger quantitative estimate

∑xlog⁡Lx≤\(1\+ε\)​∑xlog⁡Kx\+O​\(m/ε\),\\sum\_\{x\}\\log L\_\{x\}\\;\\leq\\;\(1\+\\varepsilon\)\\sum\_\{x\}\\log K\_\{x\}\+O\(m/\\varepsilon\),\(3\)valid for everyε\>0\\varepsilon\>0, where the sum ranges over all extracted elements\.

The easy point is thatKx≤LxK\_\{x\}\\leq L\_\{x\}for every elementxx, so the strong working set bound always implies the weak one\. The substance is the converse direction: although an individual lifetimeLxL\_\{x\}can be much larger than the corresponding strong parameterKxK\_\{x\}, this can only happen for relatively few elements at the same time\. The proof makes this precise via a packing argument: at any timett, there cannot be many live elements with small strong parameter\. Grouping elements according to the size ofKxK\_\{x\}, this packing bound yields an upper bound on the total lifetime within each group, and Jensen’s inequality then controls the total contribution oflog⁡\(Lx/Kx\)\\log\(L\_\{x\}/K\_\{x\}\)\.

#### Setup\.

Consider any sequence ofmmheap operations, each eitherInsertof a fresh element orExtractMinremoving a present element\. Elements are distinct even if keys coincide\. For each elementxxthat is eventually extracted, lettxt\_\{x\}be its insertion time,tx′t^\{\\prime\}\_\{x\}its extraction time, and define its*lifetime*

Lx:=tx′−tx\+1\.L\_\{x\}:=t^\{\\prime\}\_\{x\}\-t\_\{x\}\+1\.For each timettwithtx≤t<tx′t\_\{x\}\\leq t<t^\{\\prime\}\_\{x\}, letWt,xW\_\{t,x\}be the set of all elements inserted after timetxt\_\{x\}that are still present immediately after operationtt\. We also define

Kx:=maxtx≤t<tx′⁡\(\|Wt,x\|\+1\)\.K\_\{x\}:=\\max\_\{t\_\{x\}\\leq t<t^\{\\prime\}\_\{x\}\}\\bigl\(\|W\_\{t,x\}\|\+1\\bigr\)\.ThusLxL\_\{x\}is the weak working set parameter andKxK\_\{x\}is the strong one\.

For a timett, letA​\(t\)A\(t\)denote the set of elements present immediately after operationtt\. All logarithms are base22\.

###### Lemma 21\.

For every extracted elementxx, we haveKx≤LxK\_\{x\}\\leq L\_\{x\}\.

###### Proof\.

Fixttwithtx≤t<tx′t\_\{x\}\\leq t<t^\{\\prime\}\_\{x\}\. Every element ofWt,xW\_\{t,x\}was inserted after timetxt\_\{x\}and no later than timett, so\|Wt,x\|≤t−tx\|W\_\{t,x\}\|\\leq t\-t\_\{x\}\. Hence

\|Wt,x\|\+1≤\(t−tx\)\+1≤\(tx′−tx\)\+1=Lx\.\|W\_\{t,x\}\|\+1\\leq\(t\-t\_\{x\}\)\+1\\leq\(t^\{\\prime\}\_\{x\}\-t\_\{x\}\)\+1=L\_\{x\}\.Taking the maximum over all admissiblettgivesKx≤LxK\_\{x\}\\leq L\_\{x\}\. ∎

The next lemma is the key combinatorial input\. It says that elements with small strong parameter cannot overlap too much in time\.

###### Lemma 22\(Packing lemma\)\.

Fix a timettand an integerk≥1k\\geq 1\. Then at mostkkelementsx∈A​\(t\)x\\in A\(t\)satisfyKx≤kK\_\{x\}\\leq k\.

###### Proof\.

Suppose for contradiction that there arek\+1k\+1such elements alive after operationtt\. Letxxbe the oldest among them, i\.e\. the one with minimum insertion time\. Then the otherkkelements were all inserted afterxxand are all present at timett, hence they all belong toWt,xW\_\{t,x\}\. Therefore

\|Wt,x\|≥k,soKx≥\|Wt,x\|\+1≥k\+1,\|W\_\{t,x\}\|\\geq k,\\qquad\\text\{so\}\\qquad K\_\{x\}\\geq\|W\_\{t,x\}\|\+1\\geq k\+1,contradictingKx≤kK\_\{x\}\\leq k\. ∎

We now prove the quantitative comparison \([3](https://arxiv.org/html/2604.16989#A2.E3)\)\.

###### Theorem 23\.

For everyε\>0\\varepsilon\>0and every operation sequence of lengthmm,

∑xlog⁡Lx≤\(1\+ε\)​∑xlog⁡Kx\+O​\(m/ε\),\\sum\_\{x\}\\log L\_\{x\}\\;\\leq\\;\(1\+\\varepsilon\)\\sum\_\{x\}\\log K\_\{x\}\+O\(m/\\varepsilon\),where the sum ranges over all extracted elementsxx\.

###### Proof\.

Fixε\>0\\varepsilon\>0\. We may assumeε≤1\\varepsilon\\leq 1, since otherwise the claim is weaker than the caseε=1\\varepsilon=1\. Let

b:=⌈1ε⌉,b:=\\left\\lceil\\frac\{1\}\{\\varepsilon\}\\right\\rceil,so that1/b≤ε1/b\\leq\\varepsilonandb=O​\(1/ε\)b=O\(1/\\varepsilon\)\.

We partition the extracted elements into coarse levels according to the size ofKxK\_\{x\}: for each integerj≥0j\\geq 0, let

Xj:=\{x:2b​j≤Kx<2b​\(j\+1\)\},Nj:=\|Xj\|\.X\_\{j\}:=\\\{x:2^\{bj\}\\leq K\_\{x\}<2^\{b\(j\+1\)\}\\\},\\qquad N\_\{j\}:=\|X\_\{j\}\|\.
We first bound the total lifetime inside one level\. Since an elementxxis alive after exactly the timest=tx,tx\+1,…,tx′−1t=t\_\{x\},t\_\{x\}\+1,\\dots,t^\{\\prime\}\_\{x\}\-1, it contributesLx−1L\_\{x\}\-1to∑t𝟏x∈A​\(t\)\\sum\_\{t\}\\mathbf\{1\}\_\{x\\in A\(t\)\}\. Therefore

∑x∈Xj\(Lx−1\)=∑t=1m\|Xj∩A​\(t\)\|\.\\sum\_\{x\\in X\_\{j\}\}\(L\_\{x\}\-1\)=\\sum\_\{t=1\}^\{m\}\|X\_\{j\}\\cap A\(t\)\|\.Now ifx∈Xjx\\in X\_\{j\}, thenKx<2b​\(j\+1\)K\_\{x\}<2^\{b\(j\+1\)\}, henceKx≤2b​\(j\+1\)−1K\_\{x\}\\leq 2^\{b\(j\+1\)\}\-1\. Applying[AppendixB](https://arxiv.org/html/2604.16989#A2.SS0.SSS0.Px1)withk=2b​\(j\+1\)−1k=2^\{b\(j\+1\)\}\-1, we get

\|Xj∩A​\(t\)\|≤2b​\(j\+1\)−1≤2b​\(j\+1\)for every​t\.\|X\_\{j\}\\cap A\(t\)\|\\leq 2^\{b\(j\+1\)\}\-1\\leq 2^\{b\(j\+1\)\}\\qquad\\text\{for every \}t\.Summing overttyields

∑x∈Xj\(Lx−1\)≤m⋅2b​\(j\+1\),\\sum\_\{x\\in X\_\{j\}\}\(L\_\{x\}\-1\)\\leq m\\cdot 2^\{b\(j\+1\)\},and hence

∑x∈XjLx≤m⋅2b​\(j\+1\)\+Nj≤2​m⋅2b​\(j\+1\)\.\\sum\_\{x\\in X\_\{j\}\}L\_\{x\}\\leq m\\cdot 2^\{b\(j\+1\)\}\+N\_\{j\}\\leq 2m\\cdot 2^\{b\(j\+1\)\}\.\(4\)
We now estimate the excess

G:=∑xlog⁡\(LxKx\)\.G:=\\sum\_\{x\}\\log\\\!\\left\(\\frac\{L\_\{x\}\}\{K\_\{x\}\}\\right\)\.Forx∈Xjx\\in X\_\{j\}we haveKx≥2b​jK\_\{x\}\\geq 2^\{bj\}, and therefore

log⁡\(LxKx\)≤log⁡\(Lx2b​j\)\.\\log\\\!\\left\(\\frac\{L\_\{x\}\}\{K\_\{x\}\}\\right\)\\leq\\log\\\!\\left\(\\frac\{L\_\{x\}\}\{2^\{bj\}\}\\right\)\.Setyx:=Lx/2b​jy\_\{x\}:=L\_\{x\}/2^\{bj\}\. By[AppendixB](https://arxiv.org/html/2604.16989#A2.SS0.SSS0.Px1), we haveyx≥1y\_\{x\}\\geq 1\. Also, by \([4](https://arxiv.org/html/2604.16989#A2.E4)\),

∑x∈Xjyx=∑x∈XjLx2b​j≤2​m⋅2b​\(j\+1\)2b​j=2​m⋅2b\.\\sum\_\{x\\in X\_\{j\}\}y\_\{x\}=\\sum\_\{x\\in X\_\{j\}\}\\frac\{L\_\{x\}\}\{2^\{bj\}\}\\leq\\frac\{2m\\cdot 2^\{b\(j\+1\)\}\}\{2^\{bj\}\}=2m\\cdot 2^\{b\}\.Sincelog\\logis concave, Jensen’s inequality gives

∑x∈Xjlog⁡\(LxKx\)≤∑x∈Xjlog⁡yx≤Nj​log⁡\(2​m⋅2bNj\)\.\\sum\_\{x\\in X\_\{j\}\}\\log\\\!\\left\(\\frac\{L\_\{x\}\}\{K\_\{x\}\}\\right\)\\leq\\sum\_\{x\\in X\_\{j\}\}\\log y\_\{x\}\\leq N\_\{j\}\\log\\\!\\left\(\\frac\{2m\\cdot 2^\{b\}\}\{N\_\{j\}\}\\right\)\.Summing over all levels,

G≤∑jNj​log⁡\(2​m⋅2bNj\)\.G\\leq\\sum\_\{j\}N\_\{j\}\\log\\\!\\left\(\\frac\{2m\\cdot 2^\{b\}\}\{N\_\{j\}\}\\right\)\.
Letn:=∑jNjn:=\\sum\_\{j\}N\_\{j\}be the number of extracted elements, and letpj:=Nj/np\_\{j\}:=N\_\{j\}/n\. Then

G≤n​log⁡\(2​m⋅2bn\)\+n​H​\(p\),G\\leq n\\log\\\!\\left\(\\frac\{2m\\cdot 2^\{b\}\}\{n\}\\right\)\+nH\(p\),whereH​\(p\):=−∑jpj​log⁡pjH\(p\):=\-\\sum\_\{j\}p\_\{j\}\\log p\_\{j\}is the entropy of the distribution\(pj\)j\(p\_\{j\}\)\_\{j\}\.

We bound the two terms separately\.

For the first term,

n​log⁡\(2​m⋅2bn\)=n​\(b\+1\)\+n​log⁡\(m/n\)\.n\\log\\\!\\left\(\\frac\{2m\\cdot 2^\{b\}\}\{n\}\\right\)=n\(b\+1\)\+n\\log\(m/n\)\.Sincen≤mn\\leq m, the first summand is at mostm​\(b\+1\)m\(b\+1\)\. For the second, using the elementary inequalitylog⁡z≤\(z−1\)/ln⁡2\\log z\\leq\(z\-1\)/\\ln 2forz≥1z\\geq 1, we get

n​log⁡\(m/n\)≤mln⁡2\.n\\log\(m/n\)\\leq\\frac\{m\}\{\\ln 2\}\.Hence

n​log⁡\(2​m⋅2bn\)=O​\(m​b\)\.n\\log\\\!\\left\(\\frac\{2m\\cdot 2^\{b\}\}\{n\}\\right\)=O\(mb\)\.\(5\)
For the entropy term, compareppwith the geometric distributionqj:=2−\(j\+1\)q\_\{j\}:=2^\{\-\(j\+1\)\}on\{0,1,2,…\}\\\{0,1,2,\\dots\\\}\. Nonnegativity of relative entropy gives

H​\(p\)≤−∑jpj​log⁡qj=∑jpj​\(j\+1\)=1\+∑jpj​j,H\(p\)\\leq\-\\sum\_\{j\}p\_\{j\}\\log q\_\{j\}=\\sum\_\{j\}p\_\{j\}\(j\+1\)=1\+\\sum\_\{j\}p\_\{j\}j,and thus

n​H​\(p\)≤n\+∑jNj​j\.nH\(p\)\\leq n\+\\sum\_\{j\}N\_\{j\}j\.Now ifx∈Xjx\\in X\_\{j\}, thenKx≥2b​jK\_\{x\}\\geq 2^\{bj\}, solog⁡Kx≥b​j\\log K\_\{x\}\\geq bj, i\.e\.

j≤log⁡Kxb\.j\\leq\\frac\{\\log K\_\{x\}\}\{b\}\.Therefore

∑jNj​j=∑xj​\(x\)≤1b​∑xlog⁡Kx,\\sum\_\{j\}N\_\{j\}j=\\sum\_\{x\}j\(x\)\\leq\\frac\{1\}\{b\}\\sum\_\{x\}\\log K\_\{x\},wherej​\(x\)j\(x\)denotes the unique level index such thatx∈Xj​\(x\)x\\in X\_\{j\(x\)\}\. Since alson≤mn\\leq m, we obtain

n​H​\(p\)≤m\+1b​∑xlog⁡Kx\.nH\(p\)\\leq m\+\\frac\{1\}\{b\}\\sum\_\{x\}\\log K\_\{x\}\.\(6\)
Combining \([5](https://arxiv.org/html/2604.16989#A2.E5)\) and \([6](https://arxiv.org/html/2604.16989#A2.E6)\), we conclude that

G≤O​\(m​b\)\+1b​∑xlog⁡Kx\.G\\leq O\(mb\)\+\\frac\{1\}\{b\}\\sum\_\{x\}\\log K\_\{x\}\.Using1/b≤ε1/b\\leq\\varepsilonandb=O​\(1/ε\)b=O\(1/\\varepsilon\), this becomes

G≤ε​∑xlog⁡Kx\+O​\(m/ε\)\.G\\leq\\varepsilon\\sum\_\{x\}\\log K\_\{x\}\+O\(m/\\varepsilon\)\.Finally,

∑xlog⁡Lx=∑xlog⁡Kx\+G≤\(1\+ε\)​∑xlog⁡Kx\+O​\(m/ε\),\\sum\_\{x\}\\log L\_\{x\}=\\sum\_\{x\}\\log K\_\{x\}\+G\\leq\(1\+\\varepsilon\)\\sum\_\{x\}\\log K\_\{x\}\+O\(m/\\varepsilon\),as claimed\. ∎

As an immediate consequence, the weak and strong working set properties are equivalent\.

###### Corollary 24\.

A heap satisfies the weak working set property if and only if it satisfies the strong working set property\.

###### Proof\.

If a heap satisfies the weak working set property, then its total cost on every operation sequence is

O​\(m\+∑xlog⁡Lx\)\.O\\\!\\left\(m\+\\sum\_\{x\}\\log L\_\{x\}\\right\)\.Applying[Theorem23](https://arxiv.org/html/2604.16989#Thmtheorem23)with any fixedε\\varepsilon\(sayε=1\\varepsilon=1\), we get

∑xlog⁡Lx=O​\(m\+∑xlog⁡Kx\),\\sum\_\{x\}\\log L\_\{x\}=O\\\!\\left\(m\+\\sum\_\{x\}\\log K\_\{x\}\\right\),and therefore the total cost is

O​\(m\+∑xlog⁡Kx\),O\\\!\\left\(m\+\\sum\_\{x\}\\log K\_\{x\}\\right\),which is exactly the strong working set property\.

Conversely, if a heap satisfies the strong working set property, then by[AppendixB](https://arxiv.org/html/2604.16989#A2.SS0.SSS0.Px1)we haveKx≤LxK\_\{x\}\\leq L\_\{x\}for every extracted elementxx, hence

∑xlog⁡Kx≤∑xlog⁡Lx\.\\sum\_\{x\}\\log K\_\{x\}\\leq\\sum\_\{x\}\\log L\_\{x\}\.So a bound of the form

O​\(m\+∑xlog⁡Kx\)O\\\!\\left\(m\+\\sum\_\{x\}\\log K\_\{x\}\\right\)immediately implies

O​\(m\+∑xlog⁡Lx\),O\\\!\\left\(m\+\\sum\_\{x\}\\log L\_\{x\}\\right\),which is the weak working set property\. ∎

## Appendix CPartitioning under Function Preimage Constraints

In this appendix we prove the two main results stated in[Section3\.5](https://arxiv.org/html/2604.16989#S3.SS5): the counterexample to the original conjecture \([Theorem12](https://arxiv.org/html/2604.16989#Thmtheorem12)\) and the positive partition theorem under the stronger pairwise boundedness hypothesis \([Theorem14](https://arxiv.org/html/2604.16989#Thmtheorem14)\)\. We also record two complementary observations: under the stronger assumption of uniformnn\-boundedness the constant improves from2​n​k​\(k−1\)\+12nk\(k\-1\)\+1ton​k​\(k−1\)\+1nk\(k\-1\)\+1, and even under pairwisenn\-boundedness one cannot hope for a bound smaller than2​k−12k\-1in general\.

The natural language for the problem is graph coloring\. The following reformulation will be used throughout\.

###### Lemma 25\(Conflict graph reformulation\)\.

LetEEandFFbe sets, and letf1,…,fk:E→Ff\_\{1\},\\dots,f\_\{k\}:E\\to Fsatisfyfi​\(x\)≠fj​\(x\)f\_\{i\}\(x\)\\neq f\_\{j\}\(x\)for everyx∈Ex\\in Eand everyi≠ji\\neq j\. Define the*conflict graph*GGon vertex setEEby declaring distinctx,y∈Ex,y\\in Eadjacent whenever

fp​\(x\)=fq​\(y\)for some​p≠q\.f\_\{p\}\(x\)=f\_\{q\}\(y\)\\qquad\\text\{for some \}p\\neq q\.Then for every integerm≥1m\\geq 1, the following are equivalent:

1. 1\.EEadmits a partitionE=E1⊔⋯⊔EmE=E\_\{1\}\\sqcup\\cdots\\sqcup E\_\{m\}such that fp​\(Ei\)∩fq​\(Ei\)=∅for every​i​and every​p<q;f\_\{p\}\(E\_\{i\}\)\\cap f\_\{q\}\(E\_\{i\}\)=\\emptyset\\qquad\\text\{for every \}i\\text\{ and every \}p<q;
2. 2\.the graphGGis properlymm\-colorable\.

###### Proof\.

Suppose first thatE=E1⊔⋯⊔EmE=E\_\{1\}\\sqcup\\cdots\\sqcup E\_\{m\}is such a partition\. If two distinct verticesx,y∈Eix,y\\in E\_\{i\}were adjacent inGG, then for somep≠qp\\neq qwe would havefp​\(x\)=fq​\(y\)f\_\{p\}\(x\)=f\_\{q\}\(y\), and hencefp​\(Ei\)∩fq​\(Ei\)≠∅f\_\{p\}\(E\_\{i\}\)\\cap f\_\{q\}\(E\_\{i\}\)\\neq\\emptyset, a contradiction\. Thus everyEiE\_\{i\}is an independent set, so the partition defines a propermm\-coloring ofGG\.

Conversely, suppose thatc:E→\{1,…,m\}c:E\\to\\\{1,\\dots,m\\\}is a propermm\-coloring ofGG, and letEi:=c−1​\(i\)E\_\{i\}:=c^\{\-1\}\(i\)\. If for someiiand somep≠qp\\neq qthe setsfp​\(Ei\)f\_\{p\}\(E\_\{i\}\)andfq​\(Ei\)f\_\{q\}\(E\_\{i\}\)were not disjoint, we could choosex,y∈Eix,y\\in E\_\{i\}withfp​\(x\)=fq​\(y\)f\_\{p\}\(x\)=f\_\{q\}\(y\)\. Thenx≠yx\\neq yby assumptions, soxxandyywould be adjacent inGG, contradicting the fact thatEiE\_\{i\}is a color class\. ∎

### C\.1A counterexample to the original conjecture

We now prove[Theorem12](https://arxiv.org/html/2604.16989#Thmtheorem12)\. The mechanism behind the counterexample is simple: while fork=2k=2the assumption implies that the maximum degree in the conflict graph is at most2​n2n, fork≥3k\\geq 3, the original assumption can be satisfied vacuously by means of a “dummy” function with many empty fibers, while the remaining two functions create a highly chromatic conflict graph\.

###### Proof of[Theorem12](https://arxiv.org/html/2604.16989#Thmtheorem12)\.

Fixn≥1n\\geq 1andM≥1M\\geq 1\. Letm\>2Mm\>2^\{M\}, and define

E:=\{\(i,j\):1≤i<j≤m\},F:=\{0,1,…,m\}\.E:=\\\{\(i,j\):1\\leq i<j\\leq m\\\},\\qquad F:=\\\{0,1,\\dots,m\\\}\.Define three functions onEEby

f1​\(i,j\):=i,f2​\(i,j\):=j,f3​\(i,j\):=0\.f\_\{1\}\(i,j\):=i,\\qquad f\_\{2\}\(i,j\):=j,\\qquad f\_\{3\}\(i,j\):=0\.
The pointwise distinctness condition holds: for every\(i,j\)∈E\(i,j\)\\in Ewe havei<ji<jand0∉\{1,…,m\}0\\notin\\\{1,\\dots,m\\\}, so the three valuesf1​\(i,j\),f2​\(i,j\),f3​\(i,j\)f\_\{1\}\(i,j\),f\_\{2\}\(i,j\),f\_\{3\}\(i,j\)are pairwise distinct\.

The fiber size condition is also satisfied\. Indeed, ifz∈\{1,…,m\}z\\in\\\{1,\\dots,m\\\}, thenf3−1​\(z\)=∅f\_\{3\}^\{\-1\}\(z\)=\\emptyset, while forz=0z=0we havef1−1​\(0\)=∅f\_\{1\}^\{\-1\}\(0\)=\\emptyset\. Thus for everyz∈Fz\\in Fthere exists somet∈\{1,2,3\}t\\in\\\{1,2,3\\\}with\|ft−1​\(z\)\|=0≤n\|f\_\{t\}^\{\-1\}\(z\)\|=0\\leq n\.

It remains to analyze the conflict graphGG\. Sincef3f\_\{3\}takes only the value0, while neitherf1f\_\{1\}norf2f\_\{2\}ever takes the value0, no edge ofGGis witnessed by an equality involvingf3f\_\{3\}\. Thus two distinct vertices\(i,j\)\(i,j\)and\(i′,j′\)\(i^\{\\prime\},j^\{\\prime\}\)are adjacent if and only if either

f2​\(i,j\)=f1​\(i′,j′\)⟺j=i′,f\_\{2\}\(i,j\)=f\_\{1\}\(i^\{\\prime\},j^\{\\prime\}\)\\quad\\Longleftrightarrow\\quad j=i^\{\\prime\},or

f1​\(i,j\)=f2​\(i′,j′\)⟺i=j′\.f\_\{1\}\(i,j\)=f\_\{2\}\(i^\{\\prime\},j^\{\\prime\}\)\\quad\\Longleftrightarrow\\quad i=j^\{\\prime\}\.This graph is known as the shift graphSmS\_\{m\}\. It is well\-known, thatχ​\(Sm\)\>M\\chi\(S\_\{m\}\)\>M; we include a simple proof to keep the treatment self\-contained\.

Letccbe any proper coloring ofSmS\_\{m\}usingrrcolors\. For eachj∈\{1,…,m\}j\\in\\\{1,\\dots,m\\\}define

Aj:=\{ℓ:there exists​i<j​with​c​\(i,j\)=ℓ\}\.A\_\{j\}:=\\\{\\ell:\\text\{ there exists \}i<j\\text\{ with \}c\(i,j\)=\\ell\\\}\.We claim that the setsA1,…,AmA\_\{1\},\\dots,A\_\{m\}are pairwise distinct subsets of\{1,…,r\}\\\{1,\\dots,r\\\}\. Indeed, take1≤j<k≤m1\\leq j<k\\leq m, and letℓ:=c​\(j,k\)\\ell:=c\(j,k\)\. Thenℓ∈Ak\\ell\\in A\_\{k\}by definition\. If alsoℓ∈Aj\\ell\\in A\_\{j\}, then there existsi<ji<jwithc​\(i,j\)=ℓc\(i,j\)=\\ell\. But in the shift graph the vertices\(i,j\)\(i,j\)and\(j,k\)\(j,k\)are adjacent, since their second and first coordinates coincide, a contradiction, asccis a coloring\. Henceℓ∉Aj\\ell\\notin A\_\{j\}, soAj≠AkA\_\{j\}\\neq A\_\{k\}\.

Thus we havemmdistinct subsets of anrr\-element set, which impliesm≤2rm\\leq 2^\{r\}\. Sincem\>2Mm\>2^\{M\}, we conclude thatr\>Mr\>M\. Thereforeχ​\(Sm\)\>M\\chi\(S\_\{m\}\)\>M, and hence the conflict graphGGis notMM\-colorable\. By[AppendixC](https://arxiv.org/html/2604.16989#A3), any partition satisfying the required disjointness condition must use more thanMMparts\. ∎

The same construction immediately rules out the original conjecture for all larger values ofkk\.

###### Corollary 26\.

For everyk≥3k\\geq 3, the original conjecture fails\.

###### Proof\.

Starting from the construction above forf1,f2,f3f\_\{1\},f\_\{2\},f\_\{3\}, add functionsf4,…,fkf\_\{4\},\\dots,f\_\{k\}whose ranges are disjoint from one another and from the range off1,f2,f3f\_\{1\},f\_\{2\},f\_\{3\}\. This preserves pointwise distinctness and does not remove any edges from the conflict graph, so the graph still contains the shift graphSmS\_\{m\}and therefore has arbitrarily large chromatic number\. ∎

### C\.2The strengthened hypothesis

The counterexample shows that the original assumption is too weak because it constrains only individual fibers\. A natural fix is to require smallness*pairwise*across the functions involved in a potential conflict\. We now prove[Theorem14](https://arxiv.org/html/2604.16989#Thmtheorem14)\.

###### Proof of[Theorem14](https://arxiv.org/html/2604.16989#Thmtheorem14)\.

LetGGbe the conflict graph from[AppendixC](https://arxiv.org/html/2604.16989#A3); we orient its edges so that every vertex has bounded indegree\. Consider an edgex​yxyofGG\. By definition, there exist indicesp≠qp\\neq qsuch that

fp\(x\)=fq\(y\)=:z\.f\_\{p\}\(x\)=f\_\{q\}\(y\)=:z\.By pairwisenn\-boundedness,

min⁡\(\|fp−1​\(z\)\|,\|fq−1​\(z\)\|\)≤n\.\\min\\bigl\(\|f\_\{p\}^\{\-1\}\(z\)\|,\\;\|f\_\{q\}^\{\-1\}\(z\)\|\\bigr\)\\leq n\.If\|fp−1​\(z\)\|≤n\|f\_\{p\}^\{\-1\}\(z\)\|\\leq n, orient the edge fromxxtoyy; otherwise orient it fromyytoxx\. \(If both inequalities hold, choose either orientation\.\) We claim that every vertex has indegree at mostd:=n​k​\(k−1\)d:=nk\(k\-1\)\. Fix a vertexy∈Ey\\in E\. For an incoming edgex→yx\\to y, there exist indicesp≠qp\\neq qsuch that

fp​\(x\)=fq​\(y\)and\|fp−1​\(fq​\(y\)\)\|≤n\.f\_\{p\}\(x\)=f\_\{q\}\(y\)\\qquad\\text\{and\}\\qquad\|f\_\{p\}^\{\-1\}\(f\_\{q\}\(y\)\)\|\\leq n\.For anyy∈Ey\\in E, the number of such triples\(p,q,x\)\(p,q,x\)is at mostk​\(k−1\)​nk\(k\-1\)n, thusindeg⁡\(y\)≤k​\(k−1\)​n=d\\operatorname\{indeg\}\(y\)\\leq k\(k\-1\)n=d\.

Now any induced subgraphHHofGGhas at mostd​\|V​\(H\)\|d\|V\(H\)\|edges \(counting arcs by their tails\), thus average degree at most2​d2d\. Therefore,GGis2​d2d\-degenerate and therefore\(2​d\+1\)\(2d\+1\)\-colorable, so

χ​\(G\)≤2​n​k​\(k−1\)\+1\.\\chi\(G\)\\leq 2nk\(k\-1\)\+1\.The desired partition now follows from[AppendixC](https://arxiv.org/html/2604.16989#A3)\. ∎

Under even stronger hypothesis that every fiber of every function has size at mostnn, one gets a better constant, because then the conflict graph has maximum degree \(rather than merely maximum indegree\) bounded bydd\.

###### Theorem 27\(Uniformnn\-boundedness\)\.

Assume pointwise distinctness and suppose that

\|fi−1​\(z\)\|≤nfor every​i∈\{1,…,k\}​and every​z∈F\.\|f\_\{i\}^\{\-1\}\(z\)\|\\leq n\\qquad\\text\{for every \}i\\in\\\{1,\\dots,k\\\}\\text\{ and every \}z\\in F\.ThenEEcan be partitioned inton​k​\(k−1\)\+1nk\(k\-1\)\+1parts with the required disjointness property\.

###### Proof\.

LetGGbe the conflict graph\. Fix a vertexy∈Ey\\in E\. For each ordered pair\(p,q\)\(p,q\)withp≠qp\\neq q, define

Np,q​\(y\):=\{x∈E∖\{y\}:fp​\(x\)=fq​\(y\)\}\.N\_\{p,q\}\(y\):=\\\{x\\in E\\setminus\\\{y\\\}:f\_\{p\}\(x\)=f\_\{q\}\(y\)\\\}\.Then\|Np,q​\(y\)\|≤\|fp−1​\(fq​\(y\)\)\|≤n\|N\_\{p,q\}\(y\)\|\\leq\|f\_\{p\}^\{\-1\}\(f\_\{q\}\(y\)\)\|\\leq n\. Since every neighbor ofyybelongs to at least one such set,

degG⁡\(y\)≤∑p≠q\|Np,q​\(y\)\|≤n​k​\(k−1\)\.\\deg\_\{G\}\(y\)\\leq\\sum\_\{p\\neq q\}\|N\_\{p,q\}\(y\)\|\\leq nk\(k\-1\)\.ThusΔ​\(G\)≤n​k​\(k−1\)\\Delta\(G\)\\leq nk\(k\-1\), and thereforeGGis\(n​k​\(k−1\)\+1\)\(nk\(k\-1\)\+1\)\-colorable\. The claim follows from[AppendixC](https://arxiv.org/html/2604.16989#A3)\. ∎

### C\.3Lower bounds

The upper bounds above are not tight in general, but even under pairwisenn\-boundedness one cannot hope for a bound independent ofkk\.

###### Proposition 28\.

For everyk≥2k\\geq 2and everyn≥1n\\geq 1, there exist examples satisfying pairwisenn\-boundedness for which at least2​k−12k\-1parts are required\.

###### Proof\.

LetE=F=ℤ2​k−1E=F=\\mathbb\{Z\}\_\{2k\-1\}and define fori=1,…,ki=1,\\dots,k

fi​\(x\):=x\+i\.f\_\{i\}\(x\):=x\+i\.Eachfif\_\{i\}is a bijection, so in particular all fibers have size1≤n1\\leq n\. Hence the instance satisfies the stronger uniformnn\-boundedness condition\.

We claim that the conflict graph is the complete graphK2​k−1K\_\{2k\-1\}\. Indeed, letx≠yx\\neq yand writeδ:=y−x∈ℤ2​k−1∖\{0\}\\delta:=y\-x\\in\\mathbb\{Z\}\_\{2k\-1\}\\setminus\\\{0\\\}\. The set of ordered differences\{p−q:p≠q\}=\{−\(k−1\),…,−1,1,…,k−1\}\\\{p\-q:p\\neq q\\\}=\\\{\-\(k\-1\),\\dots,\-1,1,\\dots,k\-1\\\}coincides with all nonzero residues modulo2​k−12k\-1\. Hence there existp≠qp\\neq qwithp−q=δp\-q=\\delta, which is equivalent to

fp​\(x\)=x\+p=y\+q=fq​\(y\)\.f\_\{p\}\(x\)=x\+p=y\+q=f\_\{q\}\(y\)\.Thus every two distinct vertices are adjacent\. Therefore the conflict graph isK2​k−1K\_\{2k\-1\}and requires2​k−12k\-1colors\. ∎

## Appendix DComplexity of Optimization in KKOS Cultural Dynamics

In this appendix we prove the results stated in[Section3\.6](https://arxiv.org/html/2604.16989#S3.SS6)\. We first establish NP\-hardness of the decision problem via a reduction fromClique, then prove membership in NP under rational input encoding, yielding NP\-completeness\. Finally, we characterize feasible supports on forests and give a polynomial\-time algorithm\.

Throughout,G=\(V,E\)G=\(V,E\)is an undirected graph,A′A^\{\\prime\}is its adjacency matrix,A=A′\+IA=A^\{\\prime\}\+I\(self\-loops added\),y∈ℝ≥0Vy\\in\\mathbb\{R\}\_\{\\geq 0\}^\{V\}is a distribution with‖y‖1=1\\\|y\\\|\_\{1\}=1, andc∈ℝ≥0Vc\\in\\mathbb\{R\}\_\{\\geq 0\}^\{V\}is a cost vector\. A distributionx∈ℝ≥0Vx\\in\\mathbb\{R\}\_\{\\geq 0\}^\{V\}with∑vxv=1\\sum\_\{v\}x\_\{v\}=1is*feasible*if for every edgeu​v∈Euv\\in E, wheneverxu,xv\>0x\_\{u\},x\_\{v\}\>0one has\(A​x\)u=\(A​x\)v\(Ax\)\_\{u\}=\(Ax\)\_\{v\}\. We writesupp⁡\(x\)=\{v:xv\>0\}\\operatorname\{supp\}\(x\)=\\\{v:x\_\{v\}\>0\\\}and call\(A​x\)v\(Ax\)\_\{v\}the*mass*at vertexvv\.

### D\.1NP\-hardness

###### Lemma 29\(Universal vertex forces clique support\)\.

LetGGbe a graph with a universal vertexzz\. Ifxxis a feasible distribution withz∈supp⁡\(x\)z\\in\\operatorname\{supp\}\(x\), thenG​\[supp⁡\(x\)\]G\[\\operatorname\{supp\}\(x\)\]is a clique\.

###### Proof\.

LetS=supp⁡\(x\)S=\\operatorname\{supp\}\(x\)\. Fix anyu∈Su\\in Swithu≠zu\\neq z\. Sincezzis universal,z​u∈Ezu\\in E\. Becausexz,xu\>0x\_\{z\},x\_\{u\}\>0, feasibility gives\(A​x\)u=\(A​x\)z\(Ax\)\_\{u\}=\(Ax\)\_\{z\}\. Nowzzis adjacent to every vertex ofSS, andAAincludes self\-loops, so\(A​x\)z=∑v∈Sxv=1\(Ax\)\_\{z\}=\\sum\_\{v\\in S\}x\_\{v\}=1\. Hence\(A​x\)u=1\(Ax\)\_\{u\}=1\. But\(A​x\)u=∑v∈S∩NG​\[u\]xv\(Ax\)\_\{u\}=\\sum\_\{v\\in S\\cap N\_\{G\}\[u\]\}x\_\{v\}, and everyxvx\_\{v\}withv∈Sv\\in Sis positive\. This sum equals1=∑v∈Sxv1=\\sum\_\{v\\in S\}x\_\{v\}only ifS⊆NG​\[u\]S\\subseteq N\_\{G\}\[u\]\. Since this holds for everyu∈Su\\in S, the support induces a clique\. ∎

###### Lemma 30\(ℓ1\\ell\_\{1\}cost lower bound\)\.

Assumeci=1c\_\{i\}=1for allii\. LetS⊆VS\\subseteq V, and letxxbe any distribution withsupp⁡\(x\)⊆S\\operatorname\{supp\}\(x\)\\subseteq S\. Then‖x−y‖1≥2​\(1−y​\(S\)\)\\\|x\-y\\\|\_\{1\}\\geq 2\(1\-y\(S\)\), wherey​\(S\)=∑i∈Syiy\(S\)=\\sum\_\{i\\in S\}y\_\{i\}\.

###### Proof\.

Becausexi=0x\_\{i\}=0fori∉Si\\notin S,∑i∉S\|xi−yi\|=∑i∉Syi=1−y​\(S\)\\sum\_\{i\\notin S\}\|x\_\{i\}\-y\_\{i\}\|=\\sum\_\{i\\notin S\}y\_\{i\}=1\-y\(S\)\. Also,∑i∈Sxi=1\\sum\_\{i\\in S\}x\_\{i\}=1and∑i∈Syi=y​\(S\)\\sum\_\{i\\in S\}y\_\{i\}=y\(S\), so∑i∈S\(xi−yi\)=1−y​\(S\)\\sum\_\{i\\in S\}\(x\_\{i\}\-y\_\{i\}\)=1\-y\(S\)\. By the triangle inequality,∑i∈S\|xi−yi\|≥1−y​\(S\)\\sum\_\{i\\in S\}\|x\_\{i\}\-y\_\{i\}\|\\geq 1\-y\(S\)\. Adding gives‖x−y‖1≥2​\(1−y​\(S\)\)\\\|x\-y\\\|\_\{1\}\\geq 2\(1\-y\(S\)\)\. ∎

###### Theorem 31\(NP\-hardness\)\.

The decision problem—givenGG, rationaly,cy,c, and rational thresholdBB, decide whether a feasible distributionxxwith∑vcv​\|xv−yv\|≤B\\sum\_\{v\}c\_\{v\}\|x\_\{v\}\-y\_\{v\}\|\\leq Bexists—is NP\-hard\. Hardness holds even withci=1c\_\{i\}=1for allii, positive rationalyy, andGGhaving a universal vertex\.

###### Proof\.

We reduce fromClique\. Let\(H,k\)\(H,k\)be an instance withH=\(U,F\)H=\(U,F\)andm=\|U\|m=\|U\|\. ConstructGGby adding a universal vertexzzadjacent to all ofUU\. Setci=1c\_\{i\}=1for allii,yz=2/3y\_\{z\}=2/3,yu=1/\(3​m\)y\_\{u\}=1/\(3m\)for eachu∈Uu\\in U, and thresholdTk=2/3−2​k/\(3​m\)T\_\{k\}=2/3\-2k/\(3m\)\.

*Forward\.*IfHHhas a cliqueCCof sizekk, setS=\{z\}∪CS=\\\{z\\\}\\cup C\. ThenG​\[S\]G\[S\]is a clique, so any distribution onSSis feasible\. Definexu=1/\(3​m\)x\_\{u\}=1/\(3m\)foru∈Cu\\in C,xu=0x\_\{u\}=0foru∈U∖Cu\\in U\\setminus C,xz=1−k/\(3​m\)x\_\{z\}=1\-k/\(3m\)\. Its cost is2​\(m−k\)/\(3​m\)=Tk2\(m\-k\)/\(3m\)=T\_\{k\}\.

*Backward\.*Supposexxis feasible with cost≤Tk\\leq T\_\{k\}\. Ifxz=0x\_\{z\}=0, thezz\-coordinate contributes2/32/3and∑u∈U\|xu−yu\|≥2/3\\sum\_\{u\\in U\}\|x\_\{u\}\-y\_\{u\}\|\\geq 2/3\(since∑uxu=1\\sum\_\{u\}x\_\{u\}=1while∑uyu=1/3\\sum\_\{u\}y\_\{u\}=1/3\), giving cost≥4/3\>Tk\\geq 4/3\>T\_\{k\}, a contradiction\. Soz∈supp⁡\(x\)z\\in\\operatorname\{supp\}\(x\), and by[SectionD\.1](https://arxiv.org/html/2604.16989#A4.SS1),supp⁡\(x\)=\{z\}∪C\\operatorname\{supp\}\(x\)=\\\{z\\\}\\cup Cfor a cliqueCCinHHof sizett\. By[SectionD\.1](https://arxiv.org/html/2604.16989#A4.SS1), the cost is≥2/3−2​t/\(3​m\)\\geq 2/3\-2t/\(3m\), sot≥kt\\geq k\. ∎

### D\.2Membership in NP

###### Theorem 32\(NP\-membership\)\.

Under the standard binary encoding of rational input, the decision problem belongs to NP\.

###### Proof\.

Let the instance be a yes\-instance, with feasible distributionxxandS=supp⁡\(x\)S=\\operatorname\{supp\}\(x\)\. Consider the linear programP​\(S\)P\(S\)with variablesu∈ℝVu\\in\\mathbb\{R\}^\{V\},t∈ℝVt\\in\\mathbb\{R\}^\{V\},δ∈ℝ\\delta\\in\\mathbb\{R\}:

ui=0\\displaystyle u\_\{i\}=0for​i∉S,\\displaystyle\\text\{for \}i\\notin S,ui≥δ\\displaystyle u\_\{i\}\\geq\\deltafor​i∈S,\\displaystyle\\text\{for \}i\\in S,0≤ui≤1\\displaystyle 0\\leq u\_\{i\}\\leq 1for all​i,∑iui=1,\\displaystyle\\text\{for all \}i,\\qquad\\textstyle\\sum\_\{i\}u\_\{i\}=1,\(A​u\)a=\(A​u\)b\\displaystyle\(Au\)\_\{a\}=\(Au\)\_\{b\}for every edge​a​b​with​a,b∈S,\\displaystyle\\text\{for every edge \}ab\\text\{ with \}a,b\\in S,ti≥ui−yi,ti≥yi−ui\\displaystyle t\_\{i\}\\geq u\_\{i\}\-y\_\{i\},\\;t\_\{i\}\\geq y\_\{i\}\-u\_\{i\}for all​i,0≤ti≤1,\\displaystyle\\text\{for all \}i,\\qquad 0\\leq t\_\{i\}\\leq 1,∑ici​ti≤B,\\displaystyle\\textstyle\\sum\_\{i\}c\_\{i\}t\_\{i\}\\leq B,0≤δ≤1\.\\displaystyle\\qquad 0\\leq\\delta\\leq 1\.Maximizeδ\\delta\. The point\(u,t,δ\)=\(x,\|x−y\|,mini∈S⁡xi\)\(u,t,\\delta\)=\(x,\|x\-y\|,\\min\_\{i\\in S\}x\_\{i\}\)is feasible withδ\>0\\delta\>0, so the optimum is positive\.

All coefficients are rational\. An optimal basic feasible solution has coordinates whose length is polynomial in the input, so there exists an optimal solution\(u∗,t∗,δ∗\)\(u^\{\*\},t^\{\*\},\\delta^\{\*\}\)withδ∗\>0\\delta^\{\*\}\>0,supp⁡\(u∗\)=S\\operatorname\{supp\}\(u^\{\*\}\)=S, and polynomial encoding length\. Sinceu∗u^\{\*\}satisfies all constraints, it is a feasible distribution with cost≤B\\leq B\. Thus every yes\-instance has a polynomial\-size rational certificate, verifiable in polynomial time\. ∎

### D\.3Structural characterization

###### Lemma 33\(Dominated neighborhoods obstruct feasibility\)\.

LetHHbe a graph\. If there is an edgeu​v∈E​\(H\)uv\\in E\(H\)withNH​\[u\]⊊NH​\[v\]N\_\{H\}\[u\]\\subsetneq N\_\{H\}\[v\], then no strictly positive vectorx∈ℝ\>0V​\(H\)x\\in\\mathbb\{R\}\_\{\>0\}^\{V\(H\)\}can satisfy\(A​x\)u=\(A​x\)v\(Ax\)\_\{u\}=\(Ax\)\_\{v\}for all edges\.

###### Proof\.

We have\(A​x\)v−\(A​x\)u=∑w∈NH​\[v\]∖NH​\[u\]xw\>0\(Ax\)\_\{v\}\-\(Ax\)\_\{u\}=\\sum\_\{w\\in N\_\{H\}\[v\]\\setminus N\_\{H\}\[u\]\}x\_\{w\}\>0, sinceNH​\[v\]∖NH​\[u\]≠∅N\_\{H\}\[v\]\\setminus N\_\{H\}\[u\]\\neq\\emptysetandxw\>0x\_\{w\}\>0for allww\. ∎

###### Proposition 34\(Chordal feasible supports are disjoint unions of cliques\)\.

LetGGbe a chordal graph\. IfS⊆VS\\subseteq Vis a feasible support, then every connected component ofG​\[S\]G\[S\]is a clique\.

###### Proof\.

LetHHbe a connected component ofG​\[S\]G\[S\]\. SinceGGis chordal,HHis chordal\. Restricting a feasible distribution to the vertices ofHHgives a strictly positive vector satisfying the mass\-equality constraints onHH\.

IfHHis not a clique, thenHHhas a simplicial vertexssthat is not universal \(every chordal graph has a simplicial vertex, and a non\-clique has one that is not adjacent to all others\)\. Pick any neighborvvofssinHH\. Sincessis simplicial,NH​\(s\)N\_\{H\}\(s\)is a clique, so every neighbor ofssis also a neighbor ofvv\. ThusNH​\[s\]⊆NH​\[v\]N\_\{H\}\[s\]\\subseteq N\_\{H\}\[v\], and sincessis not universal,NH​\[s\]⊊NH​\[v\]N\_\{H\}\[s\]\\subsetneq N\_\{H\}\[v\]\. By[SectionD\.3](https://arxiv.org/html/2604.16989#A4.SS3), no strictly positive feasible vector exists onHH, a contradiction\. ∎

###### Proposition 35\(Feasible supports on forests are dissociation sets\)\.

LetGGbe a forest andS⊆VS\\subseteq Vnonempty\. Then there exists a feasible distribution with support exactlySSif and only ifG​\[S\]G\[S\]has maximum degree at most11\.

###### Proof\.

\(⇒\)\(\\Rightarrow\)Supposexxis feasible withsupp⁡\(x\)=S\\operatorname\{supp\}\(x\)=S\. LetH=G​\[S\]H=G\[S\]\. IfHHhas a component with≥3\\geq 3vertices, letuube a leaf andvvits unique neighbor in that component\. Thenvvhas another neighbor in the component, soNH​\[u\]⊊NH​\[v\]N\_\{H\}\[u\]\\subsetneq N\_\{H\}\[v\]\. Since\(A​x\)w=∑t∈NH​\[w\]xt\(Ax\)\_\{w\}=\\sum\_\{t\\in N\_\{H\}\[w\]\}x\_\{t\}forw∈Sw\\in S\(vertices outsideSScarry zero mass\),[SectionD\.3](https://arxiv.org/html/2604.16989#A4.SS3)gives a contradiction\.

\(⇐\)\(\\Leftarrow\)IfΔ​\(H\)≤1\\Delta\(H\)\\leq 1, setxi=1/\|S\|x\_\{i\}=1/\|S\|fori∈Si\\in S,xi=0x\_\{i\}=0otherwise\. Every support edgeu​vuvis an isolatedK2K\_\{2\}inHH, soNH​\[u\]=NH​\[v\]=\{u,v\}N\_\{H\}\[u\]=N\_\{H\}\[v\]=\\\{u,v\\\}and\(A​x\)u=\(A​x\)v=2/\|S\|\(Ax\)\_\{u\}=\(Ax\)\_\{v\}=2/\|S\|\. ∎

### D\.4Polynomial\-time algorithm for forests

###### Lemma 36\(Closed\-form cost for fixed support\)\.

LetS⊆VS\\subseteq Vbe nonempty\. Among all distributions supported withinSS, the minimumℓ1\\ell\_\{1\}\-cost is

F​\(S\)=∑i∉Sci​yi\+\(1−y​\(S\)\)​mini∈S⁡ci\.F\(S\)=\\sum\_\{i\\notin S\}c\_\{i\}y\_\{i\}\+\(1\-y\(S\)\)\\min\_\{i\\in S\}c\_\{i\}\.

*Note:*the least\-cost distribution above may*not*be an equilibrium\.

###### Proof\.

Letm=1−y​\(S\)m=1\-y\(S\)andc∗=mini∈S⁡cic\_\{\*\}=\\min\_\{i\\in S\}c\_\{i\}\. For any distributionxxsupported withinSS, we havexi=0x\_\{i\}=0for everyi∉Si\\notin S, so∑i∉Sci​\|xi−yi\|=∑i∉Sci​yi\\sum\_\{i\\notin S\}c\_\{i\}\|x\_\{i\}\-y\_\{i\}\|=\\sum\_\{i\\notin S\}c\_\{i\}y\_\{i\}\. For the in\-SSpart, settingdi=xi−yid\_\{i\}=x\_\{i\}\-y\_\{i\}, we have∑i∈Sdi=m\\sum\_\{i\\in S\}d\_\{i\}=m, so∑i∈Sci​\|di\|≥c∗​∑i∈S\|di\|≥c∗​m\\sum\_\{i\\in S\}c\_\{i\}\|d\_\{i\}\|\\geq c\_\{\*\}\\sum\_\{i\\in S\}\|d\_\{i\}\|\\geq c\_\{\*\}m\.

To attain equality, pickr∈Sr\\in Swithcr=c∗c\_\{r\}=c\_\{\*\}and setxi=yix\_\{i\}=y\_\{i\}fori∈S∖\{r\}i\\in S\\setminus\\\{r\\\},xr=yr\+mx\_\{r\}=y\_\{r\}\+m\. ∎

###### Theorem 37\(Polynomial\-time algorithm for forests\)\.

IfGGis a forest, the optimization problem is solvable inO​\(n2\)O\(n^\{2\}\)time\. The decision problem on forests is therefore inPP\.

###### Proof\.

*Step 1: reduction to dissociation sets\.*By[Proposition35](https://arxiv.org/html/2604.16989#Thmtheorem35), the feasible supports are exactly the nonempty dissociation sets \(vertex setsSSwithΔ​\(G​\[S\]\)≤1\\Delta\(G\[S\]\)\\leq 1\)\. Since dissociation sets are hereditary,OPT=min⁡\{F​\(S\):∅≠S⊆V,Δ​\(G​\[S\]\)≤1\}\\operatorname\{OPT\}=\\min\\\{F\(S\):\\emptyset\\neq S\\subseteq V,\\;\\Delta\(G\[S\]\)\\leq 1\\\}\.

*Step 2: anchor at a minimum\-cost vertex\.*SetK=∑i∈Vci​yiK=\\sum\_\{i\\in V\}c\_\{i\}y\_\{i\}\. For eachr∈Vr\\in V, letVr=\{i∈V:ci≥cr\}V\_\{r\}=\\\{i\\in V:c\_\{i\}\\geq c\_\{r\}\\\}, letGr=G​\[Vr\]G\_\{r\}=G\[V\_\{r\}\], and assign weightwi\(r\)=\(ci\+cr\)​yiw\_\{i\}^\{\(r\)\}=\(c\_\{i\}\+c\_\{r\}\)y\_\{i\}to eachi∈Vri\\in V\_\{r\}\. LetMrM\_\{r\}be the maximum total weight of a dissociation set inGrG\_\{r\}containingrr\.

Using[SectionD\.4](https://arxiv.org/html/2604.16989#A4.SS4), for any nonempty dissociation setSSwith anchorr∈Sr\\in Sminimizingcic\_\{i\}overSS:F​\(S\)=K\+cr−∑i∈Swi\(r\)≥K\+cr−MrF\(S\)=K\+c\_\{r\}\-\\sum\_\{i\\in S\}w\_\{i\}^\{\(r\)\}\\geq K\+c\_\{r\}\-M\_\{r\}\. Conversely, the dissociation set achievingMrM\_\{r\}givesF​\(Sr\)=K\+cr−MrF\(S\_\{r\}\)=K\+c\_\{r\}\-M\_\{r\}\. HenceOPT=minr∈V⁡\(K\+cr−Mr\)\\operatorname\{OPT\}=\\min\_\{r\\in V\}\(K\+c\_\{r\}\-M\_\{r\}\)\.

*Step 3: dynamic programming\.*EachGrG\_\{r\}is a forest\. In the component containingrr, root the tree atrr\. For each vertexvvin a rooted subtree, define:

- •PvP\_\{v\}: max weight of a dissociation set in the subtree ofvvwithv∉Sv\\notin S,
- •QvQ\_\{v\}: max weight withv∈Sv\\in Sand no child ofvvinSS,
- •RvR\_\{v\}: max weight withv∈Sv\\in Sand exactly one child ofvvinSS\.

Base case \(leaf\):Pv=0P\_\{v\}=0,Qv=w​\(v\)Q\_\{v\}=w\(v\),Rv=−∞R\_\{v\}=\-\\infty\. For childrenu1,…,utu\_\{1\},\\ldots,u\_\{t\}:

Pv\\displaystyle P\_\{v\}=∑j=1tmax⁡\{Puj,Quj,Ruj\},\\displaystyle=\\textstyle\\sum\_\{j=1\}^\{t\}\\max\\\{P\_\{u\_\{j\}\},Q\_\{u\_\{j\}\},R\_\{u\_\{j\}\}\\\},Qv\\displaystyle Q\_\{v\}=w​\(v\)\+∑j=1tPuj,\\displaystyle=w\(v\)\+\\textstyle\\sum\_\{j=1\}^\{t\}P\_\{u\_\{j\}\},Rv\\displaystyle R\_\{v\}=w​\(v\)\+∑j=1tPuj\+max1≤j≤t⁡\(Quj−Puj\)\.\\displaystyle=w\(v\)\+\\textstyle\\sum\_\{j=1\}^\{t\}P\_\{u\_\{j\}\}\+\\max\_\{1\\leq j\\leq t\}\(Q\_\{u\_\{j\}\}\-P\_\{u\_\{j\}\}\)\.\(TheRvR\_\{v\}formula uses the observation that selecting childuju\_\{j\}addsQuj−PujQ\_\{u\_\{j\}\}\-P\_\{u\_\{j\}\}over the baseline\. Ifv∈Sv\\in Sand childuj∈Su\_\{j\}\\in S, thenuju\_\{j\}cannot have a selected child, souju\_\{j\}must be in stateQQ\.\)

For the root component,MrM\_\{r\}usesmax⁡\{Qr,Rr\}\\max\\\{Q\_\{r\},R\_\{r\}\\\}\(the root must be selected\)\. For other components, addmax⁡\{Pρ,Qρ,Rρ\}\\max\\\{P\_\{\\rho\},Q\_\{\\rho\},R\_\{\\rho\}\\\}at each rootρ\\rho\. EachMrM\_\{r\}is computed inO​\(n\)O\(n\)time; iterating over all anchors takesO​\(n2\)O\(n^\{2\}\)\.

Once a minimizing anchor and optimal dissociation setSrS\_\{r\}are found, the optimal distribution isxi=0x\_\{i\}=0fori∉Sri\\notin S\_\{r\},xi=yix\_\{i\}=y\_\{i\}fori∈Sr∖\{r\}i\\in S\_\{r\}\\setminus\\\{r\\\},xr=yr\+1−y​\(Sr\)x\_\{r\}=y\_\{r\}\+1\-y\(S\_\{r\}\)\. ∎

Similar Articles

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

arXiv cs.AI

Introduces ProofCouncil, an LLM-based agent with an author-critic architecture that autonomously solves open mathematical problems. It achieved the best performance in the FirstProof challenge, solving 6 of 10 problems correctly, and shows promise on a broader set of 30 open problems.

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

arXiv cs.AI

LEAP is an agentic framework that enables general-purpose LLMs to achieve state-of-the-art performance in formal theorem proving in Lean, solving all 12 problems from the 2025 Putnam Competition and boosting formal solve rates from below 10% to 70% on a new benchmark (Lean-IMO-Bench), surpassing specialized systems.