google-deepmind / google-deepmind/formal-conjectures

A Bounded Capacity Generalization of the Classic n-Queens Problem

Open
#4,177 3 comments 1 reaction 0 assignees View on GitHub
new conjecture
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

Open the contributing 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.