Problem NT-004 — the Collatz conjecture

Conjectura.Problems.NT004.Statement

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Conjectura.Statements.Mathematics.NumberTheory.CollatzConjecture

/-! # Problem NT-004 — the Collatz conjecture

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.NT004

/-- Does the Collatz iteration reach one from every positive start? -/
def goal : Prop := Conjectura.NumberTheory.CollatzConjectureProp

end Conjectura.NT004