Здравствуйте, landerhigh, Вы писали:

L>Иными словами, ученые 10 лет работали, чтобы доказать, что теорема сводится к 10 тысячам частных случаев, которые можно проверить вычислительным методом?

Только не 10, а 100 лет. Теорема о 4 красках:

Теорема о четырёх красках была доказана в 1976 году Кеннетом Аппелем[en] и Вольфгангом Хакеном из Иллинойского университета. Это была первая крупная математическая теорема, доказанная с помощью компьютера. Первым шагом доказательства была демонстрация существования определённого набора из 1936 карт, ни одна из которых не может содержать карту меньшего размера, которая опровергала бы теорему. Авторы использовали специальную компьютерную программу, чтобы доказать это свойство для каждой из 1936 карт. Доказательство этого факта заняло сотни страниц. После этого Аппель и Хакен пришли к выводу, что не существует наименьшего контрпримера к теореме, потому что иначе он должен был бы содержать какую-нибудь из этих 1936 карт, чего нет. Это противоречие говорит о том, что контрпримера нет вообще.