  In 1933, Borsuk proposed the following problem: Can every bounded set in
$\mathbb{E}^n$ be divided into $n+1$ subsets of smaller diameters? This problem
has been studied by many authors, and a lot of partial results have been
discovered. In particular, Kahn and Kalai's counterexamples surprised the
mathematical community in 1993. Nevertheless, the problem is still far away
from being completely resolved. This paper presents a broad review on related
subjects and, based on a novel reformulation, introduces a computer proof
program to deal with this well-known problem.
