Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
То есть хотелось бы не на бумаге написанное — а на исполняемом ЯП. Чтобы запустил и сразу понимаешь фигня или нет, а не искать загогулины — вдруг что-то упустил и фигню спорол.
Здравствуйте, Shmj, Вы писали:
S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
S>То есть хотелось бы не на бумаге написанное — а на исполняемом ЯП. Чтобы запустил и сразу понимаешь фигня или нет, а не искать загогулины — вдруг что-то упустил и фигню спорол.
Имхо, им не хватает ресурса вроде википедии. Чтобы миллионы студентов подключить к этому делу. Нормальная же курсовая. И главное — чтобы всё было закешировано и не повторялось.
Здравствуйте, Shmj, Вы писали:
S>То есть хотелось бы не на бумаге написанное — а на исполняемом ЯП. Чтобы запустил и сразу понимаешь фигня или нет, а не искать загогулины — вдруг что-то упустил и фигню спорол.
Я думаю, это доказуемо невозможно. Как невозможно алгоритмически решить проблему остановки.
Здравствуйте, Shmj, Вы писали:
S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
Нет, не хотелось бы. Это ложный путь.
S>То есть хотелось бы не на бумаге написанное — а на исполняемом ЯП. Чтобы запустил и сразу понимаешь фигня или нет, а не искать загогулины — вдруг что-то упустил и фигню спорол.
Человек не машина и мыслит принципиально неформально.
Переложить внутреннее видение математика в компьютер -- непосильная задача.
Здравствуйте, Шахтер, Вы писали:
Ш>Человек не машина и мыслит принципиально неформально. Ш>Переложить внутреннее видение математика в компьютер -- непосильная задача.
Ну и пусть себе мыслит. А уже потом как намыслил — то в чем проблема написать в формальном виде? Если будет не хватать фишек языка Coq — можно будет их добавлять.
Здравствуйте, Shmj, Вы писали:
Pzz>>Я думаю, это доказуемо невозможно. Как невозможно алгоритмически решить проблему остановки.
S>Сейчас то нет проблем формализовать ВТФ на Coq? Когда будет не хватать фишек языка — можно будет их добавлять.
Блин, еще раз. Я думаю, эта задача — алгоритмически неразрешима. На каком языке не пиши, суть не изменится.
Здравствуйте, Shmj, Вы писали:
S>Здравствуйте, Pzz, Вы писали:
Pzz>>Блин, еще раз. Я думаю, эта задача — алгоритмически неразрешима. На каком языке не пиши, суть не изменится.
S>Какая именно задача? Если конкретная — ВТФ — то чувак брался это сделать, технических проблем нет, просто много работы.
Ты чего хочешь? Описать доказательство на формальном языке? Да, наверное можно. Чтобы компьютер сам доказывал? Нет, в общем случае нельзя. В ряде полезных частных случаев можно.
Здравствуйте, Shmj, Вы писали:
S>Ну и пусть себе мыслит. А уже потом как намыслил — то в чем проблема написать в формальном виде? Если будет не хватать фишек языка Coq — можно будет их добавлять.
Мда. Попробуйте написать даже не самый сложный нетривиальный математический текст.
Заведите Tex -- и вперёд.
А если текст по современной геометрии или теории чисел?
Проблема -- в коммуникации. Математики используют много изощрённых техник, для того чтобы зафиксировать на бумаге математическую мысль в
компактном виде.
Просто добавить в Coq несколько фишек -- не получится.
Здравствуйте, Shmj, Вы писали:
S>Хотелось бы 100% формализации мат. теорем. Есть Coq, вроде даже чувак с интернета хотел формализовать на нем доказательство Великой Теоремы, но это был труд на годы, не знаю закончил или нет.
Может пока не очень активно.
По-моему, главная проблема в неудобстве существующих языков/средств.
Попробовал проследить доказательство первой теоремы из списка (иррациональность sqrt(2)), черт ногу сломит.
Кто активно занимаются, пишут в 4 раза больше времени уходит на формализацию, чем на доказательство.
Неудивительно, что это пока удел энтузиастов.
Вот когда наоборот среда формализации будет помогать поиску доказательств, тогда станет гораздо популярнее.
Здравствуйте, Pzz, Вы писали:
Pzz>Ты чего хочешь? Описать доказательство на формальном языке? Да, наверное можно. Чтобы компьютер сам доказывал? Нет, в общем случае нельзя. В ряде полезных частных случаев можно.
Речь о том, чтобы компьютер сам проверял доказательство. Эта задача решена, нужно только перенести в пригодный для проверки вид все теоремы.
Здравствуйте, graniar, Вы писали:
G>Кто активно занимаются, пишут в 4 раза больше времени уходит на формализацию, чем на доказательство.
Да, это весомый аргумент. Начать с удобного представления формализации, чтобы это имело смысл. Потом прогнать всю мат. базу в формальный язык. А то вроде бы математика наука и точная, но не каждый может в этом убедиться — только у кого хватает мозгов, а мозги не купишь.
Вот когда доказать можно будет не на биологических мозгах а на покупных — на недорогом процессоре — тогда и поверю что математика точная — а так не верю, возможно даже доказательство ВТФ и Пуанкаре содержат ошибку, которую пока не заметили.
И уже после этого, новым шагом, будет поиск решений для нерешенных задач методом случайного умного подбора. Есть версия что и человек так же находит решения.
Здравствуйте, vsb, Вы писали:
vsb>Речь о том, чтобы компьютер сам проверял доказательство. Эта задача решена, нужно только перенести в пригодный для проверки вид все теоремы.
Просто математикам лень этим заниматься. Вот если бы за это давали плюшки — тогда да, переводили бы.
Здравствуйте, graniar, Вы писали:
G>Кто активно занимаются, пишут в 4 раза больше времени уходит на формализацию, чем на доказательство.
Так в этом вся суть. Если для элементарных задач такое соотношение, то шансов перевести в формальный вид
что-то из современной математики, ту же теорему Ферма, 0 -- потому что будет не в 4 раза больше а в 4000.
Технология антиэргономична.
Здравствуйте, Шахтер, Вы писали:
Ш>Технология антиэргономична.
Вот и я считаю, что надо работать над технологией, а не страдать рутинной формализацией, того, что устареет.
Чем я собсно и занимаюсь, на общественных началах и с неясными перспективами.
Не успеваю написать компилятор, вылезают косяки бай дизайн, приходят новые идеи... Вобщем все как обычно.
И думаю таких много. Так что, рано или поздно, что-то должно появиться.
