google-deepmind / google-deepmind/formal-conjectures
A Bounded Capacity Generalization of the Classic n-Queens Problem
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 327
Description
### What is the conjecture
We introduce a generalization of the classic $n$-queens problem, parameterized by a capacity bound $0 \le c \le n$. The puzzle requires placing exactly $n . c$ coins on an $n \times n$ board such that no row, column, or diagonal contains more than $c$ coins. When $c=1$, this reduces precisely to the canonical $n$-queens formulation. We formulate this problem mathematically and present extensive empirical evidence verifying the conjecture up to $n = 1500$. Using a highly optimized local search framework based on the min-conflicts heuristic, we observe smooth polynomial execution scaling and a structural transition from highly geometric permutation-like arrangements at low $c$ to maximum-entropy, uniform distribution profiles (``noisy TV screen'') in the dense middle-spectrum where $c \approx n/2$. This smooth behavior strongly suggests that the solution space remains dense and free of hard phase transitions across all valid parameter ranges.
### AMS categories
ams-05
### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else
### Lean code
```lean
namespace Mathoverflow513435
@[category research open, AMS 5]
theorem n_c_coins_placement_conjecture : answer(sorry) ↔
∀ᵉ (n : ℕ) (c : ℕ) (hn : n ≥ 4) (hc : c ≤ n),
∃ (board : Matrix (Fin n) (Fin n) ℕ),
let rc (i : Fin n) :=
∑ j : Fin n, board i j
let cc (i : Fin n) :=
∑ j : Fin n, board j i
let ddc (k : ℕ) :=
∑ i : Fin n, ∑ j : Fin n, (if i + j = k then board i j else 0)
let udc (k : ℤ) :=
∑ i : Fin n, ∑ j : Fin n, (if i - j = k then board i j else 0)
let bc :=
∑ i : Fin n, ∑ j : Fin n, board i j
-- Only zero or one coins at a position are allowed
(∀ i j : Fin n, 0 ≤ board i j ∧ board i j ≤ 1) ∧
-- Each row count is less than or equal to `c`
(∀ i : Fin n, rc i ≤ c) ∧
-- Each column count is less than or equal to `c`
(∀ i : Fin n, cc i ≤ c) ∧
-- Each downward diagonal count is less than or equal to `c`
(∀ k : ℕ, ddc k ≤ c) ∧
-- Each upward diagonal count is less than or equal to `c`
(∀ k : ℤ, udc k ≤ c) ∧
-- The board count is equal to `n * c`.
bc = n * c
:= by
sorry
end Mathoverflow513435
```
Contributor guide
Research direction
Start at the `n_c_coins_placement_conjecture` entry point in the issue's Lean code and review how this repository records formal conjectures. Verify the bounded-capacity statement and its board, row, column, diagonal, and total-count conditions; done means the conjecture is added in the repository's expected form.
Written by the indexing model from the issue text.
Assessment
- Domain
- devtools
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Quiet
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100