1) Плотность задачи.
Давайте разберемся с такой штукой, как доказательство теорем. Очень мало кто пробовал доказывать что-то в своей жизни и потому люди обычно не понимают, в чём там сложность. Наверное, обыватель представляет себе доказательство очередной теоремы как невероятное кипение изощренного ума, аналитически пробивающегося через сложные умопостроения, заходящего то с одной стороны, то с другой, и вот, наконец находящего лазейку к цели. Обладатель ума при этом мечется от компьютера к доске, исступлённо исписывая всё, что можно, рядами страшных формул. Так? Конечно, без нетривиальных аналитических способностей едва ли можно обойтись, но основная закавыка в другом. Эта же заковыка во многом ответственна за замедление прогресса на ряде фундаментальных научных фронтиров.
Закавыка в огромном объёме контекста, учёт которого необходим, чтобы эту самую фундаментальную теорию хоть немного сдвинуть. Помните Перельмана, доказавшего теорию Пуанкаре? Его достижение некоторые серьёзные математики комментировали в том ключе, что «и мы бы смогли, если бы знали все те же самые леммы и теоремы, что и он». Можно задаться вопросом – что за бред, кто же им мешал знать теоремы, разве это не их работа? Да, конечно, но любая теорема – это, фактически, утверждение, являющееся более или менее сложной рекомбинацией других утверждений, которые, в свою очередь, сами являются рекомбинацией третьих утверждений и так до формализованного эмпирического опыта. Какова глубина такой инкрементной рекомбинации? Даже если говорить о математике, то её исток тоже лежит в том самом формализованном эмпирическом опыте, подвергшемся декомпозиции на отдельные факторы влияния, абстрагированию этих факторов и какой-то рекомбинации. Можете почитать труды пифагорейцев, например, Филолая – то, что он пишет, это, фактически, попытка выстроить некую примитивную, ещё очень плохо формализованную, теорию множеств на основе своего опыта восприятия окружающего мира и таких же корявых «теорем» предшественников.
Да, маленькая ремарка – почему некоторые обыватели склонны считать, что древние философы (те же пифагорейцы) являются носителями некоей высшей мудрости, недоступной современникам? Дело именно в том, что их умопостроения банально ближе к чувственному опыту, доступному обывателю, чем более поздние наработки, представляющие собой уже многослойные узконаправленные абстракции. На деле, конечно, современные утверждения (теоремы) куда глубже.
Возвращаясь к вопросу об объеме утверждений, который надо знать и понимать, чтобы в современных реалиях доказать какое-то новое утверждение (например, решить одну из открытых проблем математики), можно с уверенностью сказать, что это минимум сотни тысяч строк – что является вполне верифицируемой оценкой, о чём чуть ниже. Что ещё важно, если говорить об относительно новых теоремах (на которые не слишком часто ссылались), так это то, что они могут быть попросту некорректными, содержать ошибки. Такое часто встречается просто потому, что мало составить новое утверждение, надо же ещё всё проверить, а когда для этого требуется потратить годы на выверку сотен и тысяч рекомбинаций, ошибиться очень просто.