- Почему не доверить машине самой вести доказательство?
- При переборе всех возможностей, при выводе всех резольвент дерево опровержений становится великаном. Время решения задачи машиной достигает времени жизни нескольких поколений людей.
- Значит, я попрошу ЭВМ доказать теорему, а мой внук заберет готовое доказательство?
- На блюдечке с голубой каемочкой. Если, конечно, машина, ведущая перебор, не окажется в металлоломе, а само доказательство будет хоть кому-нибудь нужно.
- Все-таки память о дедушке... Как же хотите вы ускорить работу машины?
- Научив ее математике. Для этого и нужен особый язык, язык практической математики.
- Язык практической математики - зачем его придумывать вновь? Разве математика издавна не обладает своим строгим, точным и однозначным языком?
- Это распространенное заблуждение, что язык математики строг и однозначен. Точнее сказать, часть его именно такова - формулы. Но все остальное... Мы проанализировали десятки книг по современной математике и увидели, что словесная ткань, связки между формулами, - все эти "легко увидеть", "подобным же образом", "после некоторых преобразований", "из чего следует", - скорее намеки, чем объяснения. Они требуют от читателя додумывания, иногда несложной, а иногда большой мыслительной работы. В общении с машиной неопределенностям не место.
- Итак, язык практической математики делает аксиомы, теоремы, следствия - весь арсенал математики доступным машине. Но кто беседует с ЭВМ на этом языке, кто учит ее математике?
- Каждый, кому не лень. Я говорю серьезно: передача машине математических знаний - дело коллективное. Все математики должны хотеть, чтобы ЭВМ знала и фундаментальные вещи, и новейшие, только что опубликованные факты. Все математики будут стремиться к полноте и детальности машинных знаний.
- Отчего же такая забота о компьютере?
- Не о компьютере забота, а о себе. Знающая машина спасает математика от неловкости. Вообразите, вы прибегаете утром на работу и оповещаете своих коллег: "Сегодня ночью я решил десятую проблему Гильберта! Получился простенький алгоритм..." Вы ожидаете взрыва восторга, а в ответ несутся сдавленные смешки...
- Коллеги смеются, потому что десятую проблему решили раньше?
- Конечно! Но не только потому. Еще и потому, что запоздалое решение ошибочно - там нет никакого алгоритма, ни простого, ни сложного, там алгоритмическая неразрешимость... Вот если б незадачливый математик, прежде чем оповещать мир об открытии, сел бы за пульт ЭВМ и сообщил бы ей...
