| |||
|
|
Да, чтобы компьютер мог проверить доказательство, нужно сначала его записать на каком-то формальном языке. Дальше уже дело нехитрое автоматически проверить, что текст на формальном языке корректно использует правила/аксиомы. Пока что подобное невозможно, и в ближайшем будущем не предвидится. Имеющиеся наработки позволяют за месяцы (и больше) кропотливой работы закодить то, что можно за полчаса объяснить первокурснику. То же самое и с рассказом про то, что компьютер может сам доказывать теоремы. Конечно, если у есть какие-то исходные данные и правила вывода, то можно написать программу, которая будет применять всевозможные правила в поисках желаемого результата. Но на деле ничего нетривиального таким образом получить нельзя за разумное время и с разумной памятью. Так что это всё безумно интересно само по себе, и много умных людей над этим работает, но это скорее принесет плоды в информатике и логике и ничего не изменит в математике. Добавить комментарий: |
|||