Да это норм, покойный Воеводский, математик с филдсовской медалью программу автоматических доказательств пытался поднимать, наработки были, но не вывез
Воеводский крутой был, это да. Чокнутый на всю голову (в хорошем смысле). Однако мне кажется что задача автоматизации доказательств сильно сложнее, чем проверка на ошибку. Нет?
Скилы мои в этом всем невелики есть, ощущения, в основном. Задача сложнее, но мода на "обьяснение каждого шага" ( o1 и другие) может приведет к схеме, когда новые основные свойства и мат обьекты люди математики придумают, а ии полностью достроит все доказательства рядом, может контримеры найдут ;)
Comments 9
Reply
Reply
Reply
Reply
Reply
Reply
Reply
Reply
Leave a comment