---

Claim. The particular question of Problem 769, whether $c(n)\gg n^n$, is answered no. The Lean 4 theorem Erdos769.erdos769_lower_bound_false, in Research/Solution.lean of the starfleet/erdos-769 folder of the williamjblair/lean-proofs repository, proves ¬ Erdos769LowerBound, where the development's Erdos769LowerBound says that there are positive integers $A$, $B$ and $N$ with $A\,n^n\le B\,c$ whenever $n\ge N$ and $c$ is the cutoff of dimension $n$: the least $c$ such that every $k\ge c$ is the tile count of an exact decomposition of the unit $n$-cube into axis-parallel homothetic cubes, in the development's half-open model. The route, as the development's files and the Star Fleet Math report describe it: for odd $n\ge201$ every $k\ge n\,2^n\lceil 49n/100\rceil^n+2$ is such a tile count, by regular grid tilings, the substitution that replaces one cube by $m^n$ cubes, and a Bézout conductor bound for the resulting increments modulo $2^n-1$; this threshold is $o(n^n)$, so $c(n)/n^n\to0$ along the odd dimensions and no absolute constant bounds $c(n)/n^n$ below. The hosting repository's index credits the proof to Colin Snyder of Star Fleet Math (starfleetmath.com), whose site describes Star Fleet as an AI system of agent harnesses each running a GPT-5.6 instance; that is the AI system named here, and the development names no informal author, so it is an independent proof rather than a formalization of either forum claim. The Star Fleet Math site distributes the development as the archive linked above and carries its report (the record link), dated 2026-07-14, when the site's own automated referee accepted it, the date this page carries; the Internet Archive's first capture of starfleetmath.com, at 2026-07-15 00:25 UTC, already lists the result, and the lean-proofs repository hosted a copy on 2026-07-23. The result is not on the site's proof-claims tab.

Covers. The bound $c(n)=o(n^n)$ along the odd integers, hence a negative answer to the question whether $c(n)\gg n^n$ holds uniformly in $n$. It does not give the order of $c(n)$, says nothing about $c(n)$ for even $n$, in particular nothing about the case $n+1$ prime in which Erdős expected $c(n)>n^n$, and the problem's request for good bounds is not settled by it; the catalog's own variant erdos_769.variants.growth_rate, asking whether $\log c(n)/(n\log n)$ has a limit, stays tagged open. The same negative answer, by written arguments with sharper thresholds, is claimed on Zeng's page (listed ten days after the date of the Star Fleet Math entry) and Korsky's page; the three are independent, and none is known to cite another.

Depends on. No page of this wiki.

Standing. Claimed. The hosting repository's index records that its continuous integration builds the file against the pinned Mathlib and that #print axioms of the headline theorem reports only propext, Classical.choice and Quot.sound; the Star Fleet Math report says the same of a build on separate hardware. The formal-conjectures statement of the problem (the second record link, pinned at the catalog's commit of 2026-09-18) has linked Research/Solution.lean at the pinned revision as its formal_proof since 2026-08-07, tagging erdos_769 as research solved with the answer false, and the community database lists the problem as formalized. Nothing was built, replayed or audited here, no write-up accompanies the development, and the fidelity of IsCutoff and Erdos769LowerBound to the problem's wording was not examined by this corpus, so the page lists no formalized evidence. The site's label is OPEN (page last edited 1 October 2025) and its page does not credit the result; no journal record, arXiv posting or outside review of the development is known.