Сообщение Re[2]: Великая теорема Ферма от 17.10.2022 13:33
Изменено 17.10.2022 13:46 graniar
Re[2]: Великая теорема Ферма
Здравствуйте, Shmj, Вы писали:
S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
Работа в этом направлении ведется. QED Manifesto
S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
Работа в этом направлении ведется. QED Manifesto
Re[2]: Великая теорема Ферма
Здравствуйте, Shmj, Вы писали:
S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
Работа в этом направлении ведется. QED Manifesto
Может пока не очень активно.
По-моему, главная проблема в неудобстве существующих языков/средств.
Попробовал проследить доказательство первой теоремы из списка (иррациональность sqrt(2)), черт ногу сломит.
Кто активно занимаются, пишут в 4 раза больше времени уходит на формализацию, чем на доказательство.
Неудивительно, что это пока удел энтузиастов.
Вот когда наоборот среда формализации будет помогать поиску доказательств, тогда станет гораздо популярнее.
S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
Работа в этом направлении ведется. QED Manifesto
Может пока не очень активно.
По-моему, главная проблема в неудобстве существующих языков/средств.
Попробовал проследить доказательство первой теоремы из списка (иррациональность sqrt(2)), черт ногу сломит.
Кто активно занимаются, пишут в 4 раза больше времени уходит на формализацию, чем на доказательство.
Неудивительно, что это пока удел энтузиастов.
Вот когда наоборот среда формализации будет помогать поиску доказательств, тогда станет гораздо популярнее.