Насколько близко компьютеры подошли к автоматическому построению математических рассуждений?

Инструментарий искусственного интеллекта определяет форму автоматических доказывателей теорем нового поколения, а вместе с этим – и взаимоотношения математики и машин