JC
А какой самый адекватный язык для доказательств?
Coq, Idris
Size: a a a
2020 May 02
SS
Coq, Idris
Кок
SS
Ирис
JC
Ну на Coq доказали какую-то задачу раскраски карты
JC
Типо, что любую карту можно раскрасить четырьмя цветами, или что-то такое
SS
Тупые человеки
SS
Они даже для создания алгоритмов скоро будут не нужны
JC
Не совсем
SS
Языки сами будут их генерировать, да ещё и валидировать
JC
Есть теорема Геделя, которая говорит, шо все очень хуево и ты ничего не можешь доказать
JC
Ну, что-то можешь, но в общем, в достаточно сильных теориях (которые могут выразить арифметические операции) найдется бесконечное количество теорем, которые нельзя опровергнуть или доказать
SS
Бляьь, хотел бы я матаном таким заниматься
I
Тупые человеки
Тупые славы
SS
От него реально голова кипит
r
у меня башка кипит от матана 6 класса
JC
Ну, что-то можешь, но в общем, в достаточно сильных теориях (которые могут выразить арифметические операции) найдется бесконечное количество теорем, которые нельзя опровергнуть или доказать
Так что пока ИИ не дойдет до уровня человека, то компьютеры в науке не очень продвинутся
r
SS
у меня башка кипит от матана 6 класса
Он не такой
JC
Пока что это просто помощники для людей
SS
Он не абстрактныы