49

Гипотеза Тебо — это весьма занимательная (и даже не слишком сложная) теорема из плоской евклидовой геометрии, которую, тем не менее, не так-то просто доказать непосредственно. Как выяснилось, единственный способ ее доказательства заключается в том, чтобы отыскать подходящее обобщение (что сделать не в пример легче), а уже затем выводить требуемый результат в виде особого случая. Такая процедура довольно широко распространена в математике, однако для компьютеров она, как правило, совершенно не годится, поскольку отыскание необходимого обобщения требует немалой изобретательности и способности разбираться в сути проблемы. Компьютерное же доказательство подразумевает наличие некоей четкой системы нисходящих правил, которым машина в дальнейшем и следует неуклонно с поражающей воображение скоростью. В данном случае львиная доля человеческой изобретательности как раз и пошла в первую очередь на разработку эффективной системы таких нисходящих правил.