Claimed resolutions with unsettled evidence: Büchi, Dean (k=5), Pierce–Birkhoff

Three `research open` declarations now have public claimed resolutions. In each case I checked the
source's statement against the Lean declaration, and the answer is that they **do** line up. What
differs sharply between them is the **strength of evidence** that the claimed proof is correct.

I am **not** proposing a status change for any of these. The purpose here is to record the claims,
the exact statement match, and an honest evidence assessment, so the decision can be made against
whatever threshold the repository wants to apply. Each item has its own checkbox because they will
firm up on very different timescales.

---

## 1. Büchi's problem

- [ ] [`buchi_problem_M5`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/Wikipedia/Buchi.lean#L51-L55) and
[`buchi_problem`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/Wikipedia/Buchi.lean#L38-L42)

**Claim.** Stanley Yao Xiao, *Hilbert's tenth problem for systems of diagonal quadratic forms, and
Büchi's problem*, [arXiv:2412.16740](https://arxiv.org/abs/2412.16740), Theorem 1.3:

> Let $x_1^2, \cdots, x_5^2$ be integer squares with constant second difference equal to 2. Then
> there exists an integer $x_0$ such that $x_j^2 = (x_0+j)^2$ for $j = 1,2,3,4,5$.

**Statement match — checked.** `IsBuchi 5` says: for all `x a : ℤ`, if `(x+n)^2 + a` is a square
for `n = 0,…,4` then `a = 0`. Those five values automatically have constant second difference 2
(any monic quadratic does), so Xiao's hypothesis holds. His conclusion gives
`(x+n)^2 + a = (c+n)^2` for `n = 0,…,4` and some integer `c`; comparing at `n = 0` and `n = 1`
forces `c = x` and hence `a = 0`. No positivity or monotonicity hypothesis is needed, matching the
unrestricted `∀ x a : ℤ` in the file. Theorem 1.3 therefore implies `IsBuchi 5`, and
`buchi_problem` follows with `M = 5`.

**Evidence.** Weakest of the three. No formalisation. The manuscript has been public since
December 2024 (v1), with v2 in May 2025 and **v3 in June 2025**; there has been no further version
in roughly 21 months and I could not find a record of acceptance or of independent verification.

---

## 2. Dean's conjecture, the $k = 5$ case

- [ ] [`dean_conjecture.variants.five`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/Arxiv/2605.02731/DeanCycles.lean#L55-L59)
(and hence [`dean_conjecture`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/Arxiv/2605.02731/DeanCycles.lean#L45-L51))

**Claim.** Elias Botsford, *Cycles of length divisible by five in graphs of minimum degree five —
The k=5 case of Dean's conjecture*, Zenodo v1.0.1, 31 August 2026,
[doi:10.5281/zenodo.22182448](https://doi.org/10.5281/zenodo.22182448), Theorem 1.2:

> Every finite simple graph $G$ with $\delta(G) \ge 5$ contains a cycle $C$ such that
> $|C| \equiv 0 \pmod 5$.

**Statement match — checked.** The paper defines cycle length as the number of edges, which is
Mathlib's convention, so this is exactly `∀ V [Fintype V] (G : SimpleGraph V), 5 ≤ G.minDegree →
∃ m ∈ G.cycleLengths, 5 ∣ m`. Finiteness, simplicity and the minimum-degree hypothesis all
correspond directly.

**Evidence.** A Zenodo deposit, not a journal or arXiv submission. Nine finite configuration
propositions are computer-assisted, with verifier sources and certificates archived separately
([doi:10.5281/zenodo.22167084](https://doi.org/10.5281/zenodo.22167084)).
[MathWorld](https://mathworld.wolfram.com/DeansConjecture.html) describes it as a *claimed proof*
and reports that the 47 certificate runs were independently replayed **but that the reductions from
arbitrary graphs have not been independently verified**. MathDB still lists the problem as
open/unverified. There is no formalisation.

---

## 3. Pierce–Birkhoff conjecture (claimed **false**)

- [ ] [`pierce_birkhoff_conjecture`](https://github.com/google-deepmind/formal-conjectures/blob/2a0126f6ec4132a0acf3b9562cb2c1f4cfa4041c/FormalConjectures/Wikipedia/PierceBirkhoff.lean#L86-L90)

**Claim.** Zehua Lai, Lek-Heng Lim and Junyu Ren, *Pierce–Birkhoff conjecture is false*,
[arXiv:2609.10420](https://arxiv.org/abs/2609.10420), 9 September 2026.

**Statement match — this one needs care.** The paper's Theorem 7 is 30-dimensional and is stated
over a **partition** `ℝⁿ = Π₁ ∪ ⋯ ∪ Πᵣ` into semialgebraic sets. This file's
`IsPiecewiseMvPolynomial` instead requires a finite cover by **closed** semialgebraic sets, and
the paper does not address closedness anywhere. So the paper's headline theorem does **not**
literally refute the declaration as written.

The authors' Lean repository does, via a *different* example that does not appear in the paper. At
commit `8ded29e3`, `n=8_d=2_k=2/lean/PBCounterexample/Quadratic8Main.lean` proves

```lean
theorem whole_space_counterexample :
Continuous f ∧
(∃ P : FinitePolynomialSignPartition f 2 2, P.count = 137) ∧
(∃ C : FiniteClosedPolynomialCover f,
C.count = 17 ∧ ∀ i, (C.label i).totalDegree ≤ 2) ∧
¬ IsPolynomialLattice f
```

and their `FiniteClosedPolynomialCover` is field-for-field the same condition as this file's
`IsPiecewiseMvPolynomial`: `IsClosed` pieces, `IsSemialgebraic` pieces, union equal to
`Set.univ`, and `f` equal to a polynomial on each piece.

**One residual gap.** Their `IsPolynomialLattice f` asserts the existence of a finite lattice
expression evaluating to `f`, whereas this file's conclusion is the max-of-min normal form
`⨆ i, ⨅ j, eval x (g i j)`. Every finite lattice expression admits such a normal form, but that
step is formalised neither here nor there.

**Evidence.** Strongest formal backing of the three, weakest provenance. Their `n=8` development
(35 files) contains no `sorry`, no `axiom` and no `native_decide`, and ships a replay harness
whose logs record **negative controls** — a deliberately hidden axiom, a missing dependency, an
altered `propext` type and an `unsafe` declaration are each confirmed to be *caught* — with exit
code 0 on all stages. Against that: the preprint is **v1, posted two days before this issue**, with
no independent review, and the paper states the counterexample was found with a multi-agent,
multi-model AI harness.

---

### What I checked, and what I did not

I read the three sources and compared their statements to the Lean by hand; that part is mine. I
did **not** referee the mathematics, and I did **not** build or kernel-check any of the linked Lean
developments — the audit above is a source-level inspection plus the authors' own recorded
verification artefacts.

### Suggestion

Leave all three `research open` for now, and use this issue to track them. Pierce–Birkhoff is the
one most likely to resolve quickly in either direction. If the repository would accept a
`formal_proof using lean4` link to the `n=8` development while leaving the category open, that is
a middle option for that item alone.

*AI assistance: these three claims were surfaced by an OpenAI Codex agent during a repository-wide
sweep of open declarations. The statement matches, source checks and evidence assessment above were
carried out with Claude Opus 5.*

Start by reading the three referenced declarations in FormalConjectures/Wikipedia/Buchi.lean, Arxiv/2605.02731/DeanCycles.lean, and FormalConjectures/Wikipedia/PierceBirkhoff.lean, then compare them with the cited sources and, for Pierce–Birkhoff, inspect Quadratic8Main.lean at the stated commit. Done means each claim has a repository-supported evidence assessment and an agreed status decision.

Written by the indexing model from the issue text.