Formal target: Corpus.WikipediaBuchi.buchi_problem_M5
**Büchi's problem (first open case, $M = 5$)**: For all integers $x$ and $a$, if $(x+n)^2 + a$ is a perfect square for $n = 0, 1, 2, 3, 4$, then $a = 0$.
Exact formal statement
Corpus.WikipediaBuchi.IsBuchi 5This target is a formal statement, not a proof of the problem.
Environment availability: available.