Никак. Рекламы не надо. Забыли уже, что счётноё мн-во счётных мн-в тоже счётно?
Бери хоть 1:10000000, всё равно обе части биективны. Сокращение на 0,000000001% (по сравнению с чем? с компьютерным док-вом?) - никак не достижение.
И в общем-то, ещё в начале 80-х годов было доказано отсутствие бесконечного кол-ва исключений из теоремы.

авторматиндукция Тоже никак. МИ доказывает нечто регулярное. А здесь (1:1 1:999 1:7779994993 ...) только ":" регулярно.

tchingiz,
элементарно, Уотсон! Вы доказываете, что имеет место в пределе 1:1.
Я доказывыаю, что в пределе 1:100500.
Пронин доказывает, что 1:3.
Очевидно, что дроби не равны. Значит где-то что-то пошлО не так.

Как минимум надо представить методологию, с к-рой сравниваешь. Всё остальное потом.

Не-не. После окончательного док-ва в 90-х,по-прежнему многим не нравится привлечение компа к док-ву. Ну не красиво это. Это как играть в шахматы грубым перебором вариантов вместо комбинаций и оценок. Искусство хде? Так что поддерживаю ТС.

Gennadiy Usov, только в том случае наоборот, из-за необозримости возможных исключений, все (или несколько, не ведаю) виды этих исключений обсчитаны на компе. А где ещё раньше калькулятор использовался в качестве последнего арбитра в доказательстве при переборе?

mayton, и тогда бы нет. Мне - по одной всегда причине: компы потенциально могут ошибиться (вкупе с прогером). Поэтому комп "не спортивно" в кавычках, а в просторечии: не изящно. К слову, много есть не изящных док-в теорем.
Ш - спорт. Тож самое имел ввиду: не потому, чтоб пользовать карманный усилитель моска, а просто не по-человечески, не изящно.

А формула - не формула - мне всё равно. Вот же есть полином (забыл уже про что он). Сам громоздкий такой, что описывается его построение длиннющим текстом. Матевосян/Мтиясевич ??, 70-ые, теорчисел. Зато он первый. Потом уже нашли варианты попроще.

mayton, не спорю. Уж не знаю как моделировать математическую реальность, чтобы выбирать тему по вкусу. Наверное надо заносить в БД аксиомы и правила формирования утверждений, и правила проверки исинности (вроде как "Бурбаки" этим занимаются). Но я имею ввиду, что это была отправная точка исследования или промежуточная вспомогательная точка.

В случае же ВТФ комп оказался ключевым участком доказательства. Он сказал: "Нет исключений из теоремы." Док-во непогрешимости комповых сессий отсутствует. Есть всего лишь убеждающая правдоподобность, но достоверности меньше, нежели бы это было без компа. Правда я не в курсе, мож сегодня для ВТФ уже есть и другие док-ва. И ИМХО неэстетично именно это: "ключевой участок доказательства". Какая-то болванка мне что-то пытается доказать)) На самом деле мне всё равно, признали, значит признали. Но запашок сохранился.

Меня не надо убеждать, я понимаю ситуацию. Просто раньше к дедукции добавлялось мнение эксперта, говорившего, что так правильно. Он мог обозреть мысленно проблему в случае чего. В этом же случае эксперт не шмог оборзеть и попросил комп. А может поленился? или спешил, что его опердят? ТС вот всегда же спешит.

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

Gennadiy Usov, мож так?
pow(x, y[, z])
Return x to the power y; if z is present, return x to the power y, modulo z (computed more efficiently than pow(x, y) % z). The two-argument form pow(x, y) is equivalent to using the power operator: x**y.

The arguments must have numeric types. With mixed operand types, the coercion rules for binary arithmetic operators apply. For int operands, the result has the same type as the operands (after coercion) unless the second argument is negative; in that case, all arguments are converted to float and a float result is delivered. For example, 10**2 returns 100, but 10**-2 returns 0.01. If the second argument is negative, the third argument must be omitted. If z is present, x and y must be of integer types, and y must be non-negative.

Gennadiy Usov, да уже всё сказано выше: наука, заточенная на результат. На таком пути хорошо бы не уйти в "странную" реальность. Не пытаться движением пальцев увеличить муху, сидящую на оконном стекле. Не отменять отправленную в милицию с обратным адресом анонимку по Ctrl-Z или Shift+Del. Тем более не прыгать с колокольни в костюме спайдера))

Забудем для начала о Гёделе либо о саморекурсивных утверждениях.
Предположу, что всё упрётся в неадекватность такой формальной реальности окружающему миру. Тогда придётся связывать всю базу с сенсорным восприятием. Потому что куда деться от индуктивных методов порождения. И некуда деться от экспертных заключений в доказательствах.
В принципе есть неплохой ДСМ-метод. В нём уже учтено индуктивное порождение утверждений (там это гипотезы). И как часто бывает, разговор непринуждённо переходит в плоскость концепций ИИ, у к-рого д.б. руки-ноги-голова и инстинкт сохранения.
Я не потяну эту тему.