Formal target: Corpus.Arxiv260512342Conjecture1.conjecture_1

**Conjecture 1 (Fernandes, 2026):** Let $m \ge n \ge 2$ be integers with $(m, n) \notin \{(2,2), (3,3), (4,3), (4,4)\}$.

Exact formal statement

∀ {m n : Nat},
  LE.le.{0} 2 m →
    LE.le.{0} 2 n →
      LE.le.{0} n m →
        Not
            (Membership.mem.{0, 0}
              (Insert.insert.{0, 0} (Prod.mk.{0, 0} 2 2)
                (Insert.insert.{0, 0} (Prod.mk.{0, 0} 3 3)
                  (Insert.insert.{0, 0} (Prod.mk.{0, 0} 4 3) (Singleton.singleton.{0, 0} (Prod.mk.{0, 0} 4 4)))))
              (Prod.mk.{0, 0} m n)) →
          Exists.{1} fun g₁ =>
            Exists.{1} fun g₂ =>
              Eq.{1} (Subgroup.closure.{0} (Insert.insert.{0, 0} g₁ (Singleton.singleton.{0, 0} g₂))) Top.top.{0}

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record