Fernandes' conjecture on the 2-generation of even direct product permutation groups

formal-conjectures · arxiv · ams-20

**Conjecture 1 (Fernandes, 2026):**
Let $m \ge n \ge 2$ be integers with $(m, n) \notin \{(2,2), (3,3), (4,3), (4,4)\}$.
Then the group
$$
\Gamma_{m \oplus n} = \{(\sigma_1, \sigma_2) \in \mathrm{S}_m \times \mathrm{S}_n :
\mathrm{sgn}(\sigma_1) = \mathrm{sgn}(\sigma_2)\}
$$
has rank $2$, i.e., minimal generating set of size $2$.

Note: Fernandes states the conjecture for groups of exact rank $2$, which is why $(2,2)$
is in the exception list: $\Gamma_{2 \oplus 2} \cong C_2$ has rank $1$. The formalised
conclusion ∃ g₁ g₂, closure {g₁, g₂} = ⊤ encodes 2-generation (at most $2$ generators),
which $\Gamma_{2 \oplus 2}$ also satisfies. The other three exceptions $(3,3), (4,3), (4,4)$
have rank $3$ and are genuinely not 2-generated.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://arxiv.org/abs/2605.12342
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Arxiv/2605.12342/Conjecture1.lean
Local target: Corpus.Arxiv260512342Conjecture1.conjecture_1
Source SHA-256: 2233dbfbafbad1db0612b05e1c7622883b024d12c1981d8f69bbd43c73e49f75
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record