теорема фейта-томпсона (математическое)
Oct. 3rd, 2012 12:16 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
avvaДоказательство теоремы Фейта-Томпсона в теории групп полностью формализовано и проверено в проверщике Coq.
(теорема Фейта-Томпсона гласит, что любая конечная группа нечетного порядка разрешима. Она была доказана в 60-х и легла в основу программы классификации простых конечных групп)
Это, несомненно, самое значительное достижение в области автоматических проверок математических доказательств до сих пор. Группа исследователей работала над этим результатом в течение 6 лет. Математическая польза от этого конкретного результата, полагаю, близка к нулю. Будущее покажет, какую пользу принесет вся эта область в целом.
(теорема Фейта-Томпсона гласит, что любая конечная группа нечетного порядка разрешима. Она была доказана в 60-х и легла в основу программы классификации простых конечных групп)
Это, несомненно, самое значительное достижение в области автоматических проверок математических доказательств до сих пор. Группа исследователей работала над этим результатом в течение 6 лет. Математическая польза от этого конкретного результата, полагаю, близка к нулю. Будущее покажет, какую пользу принесет вся эта область в целом.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-10-02 10:43 pm (UTC)http://www.ams.org/notices/200811/tx081101382p.pdf
no subject
Date: 2012-10-02 11:54 pm (UTC)Во всяком случае, в эту "теорему" (о классификации простых конечных групп) нет никаких оснований верить без формального доказательства в компьютерной системе с сильными гарантиями. При таком размере общего текста, и при том, что он намного больше, чем может понять один человек, интуитивно кажется, что вероятность отсутствия серьёзных ошибок, не поддающихся быстрому исправлению, невелика.
Так что, они молодцы, что работают в этом направлении.
no subject
Date: 2012-10-03 12:21 pm (UTC)Ну почему, Lyons и Solomon, а равно и Aschbacher и Smith понимают и пишут новое доказательство в виде серии книг.
Больше половины работы уже сделано.
Заявления про “нет никаких оснований верить без формального доказательства” совершенно безосновательны.
no subject
Date: 2012-10-03 04:40 pm (UTC)(Я, всё же, опираюсь на историю с Дюлаком и Ильяшенко, как достаточно на достаточно разумный индикатор того, начиная с какой сложности уже не стоит особо доверять.
И когда сложность на два порядка велины больше, чем у Дюлака, как было, когда я последний раз на смотрел на эту классификацию, то...)
no subject
Date: 2012-10-03 05:33 pm (UTC)Доказательство Дюлака никто особо
до Ильяшенко не читал и передоказывать
не пытался, в противоположность
классификации конечных групп,
которую передоказывают другими методами
(отсюда и second generation proof).
no subject
Date: 2012-10-03 06:07 pm (UTC)На мой вкус, многовато, чтобы поверить без компьютерной поддержки...
Но это зависит от того, как тот или иной человек оценивает вероятность серьёзных ошибок и то, как она растёт с размером математического текста. Я, всё же, склонен считать, что вероятность того, что всё правильно, падает экспоненциально с размером текста, P в степени N, где P в хороших случаях не очень сильно меньше единицы, но, всё же, всегда меньше, чем 1, а N порядка нескольких единиц на страницу. У других людей могут быть более оптимистические представления на эту тему...
no subject
Date: 2012-10-03 06:58 pm (UTC)нам придётся по крайней мере в обозримом будущем,
ибо требуется радикальный прогресс
в области формальной проверки доказательств,
прежде чем длина формальных доказательств
сократится до приемлемой (то есть
хотя бы в десять раз меньше по сравнению с нынешней).
Нам, однако, доступны косвенные методы проверки:
доказательство другим способом (как
это происходит с second generation proof),
применение теоремы в других областях
(что тоже имеет место).
Чем лучше теорема встроена в другие
контексты, тем лучше она проверена.
no subject
Date: 2012-10-03 07:59 pm (UTC)сократится до приемлемой (то есть
хотя бы в десять раз меньше по сравнению с нынешней)
реалистично, видимо, добится ситуации, когда всё, что требуется, это формально записать все нетривиальные леммы (далее от системы требуется только убедится, что они действительно доказаываются, но эта часъ доказательства уже не несёт математического содержания, которое надо знать людям; математическое содержание всё оказывается в формулировках лемм, которых, таким образом, становится больше, чем в неформальном тексте).
no subject
Date: 2016-09-01 04:55 pm (UTC)Вот если бы теорема звучала как "существует ровно 193242123 неразрешимых групп нечтного порядка", то тогда да, вероятность ошибки там была бы значительная.
no subject
Date: 2016-09-01 07:22 pm (UTC)https://ru.wikipedia.org/wiki/%D0%9A%D0%BB%D0%B0%D1%81%D1%81%D0%B8%D1%84%D0%B8%D0%BA%D0%B0%D1%86%D0%B8%D1%8F_%D0%BF%D1%80%D0%BE%D1%81%D1%82%D1%8B%D1%85_%D0%BA%D0%BE%D0%BD%D0%B5%D1%87%D0%BD%D1%8B%D1%85_%D0%B3%D1%80%D1%83%D0%BF%D0%BF
С какой стати мы должны верить, что они не пропустили ещё какую-нибудь 27-ю группу, тоже жуткую, непонятно...
(Это всё в предположении, что это вообще важно; я понятия не имею, важно знать правильное решение этой задачи, или нет...)
no subject
Date: 2016-09-01 09:04 pm (UTC)Ну я встречал, где эту теорему используют, и сам ею пользуюсь. Так что пожалуй факт важный (смотря для кого, конечно).
В самом док-ве конечно могут быть несущественые ошибки, что вообще-то нормально в науке, но они вряд ли влияют на конечный результат, т.к. он проверен на множестве примеров.
no subject
Date: 2016-09-01 09:51 pm (UTC)На мой взгляд, наша степень доверия к правильности всех этих результатов слишком велика, но это обычное явление, в то время как классификация - это какой-то выдающийся монстр...
В любом случае, мой комментарий относился к классификации, а не к теореме Фейта-Томпсона, как относительно того, насколько надо считать результат установленным, так и относительно того, важно ли, чтобы в нём не было ошибок......
no subject
Date: 2012-10-03 12:48 am (UTC)no subject
Date: 2012-10-03 03:52 am (UTC)no subject
Date: 2012-10-03 04:44 am (UTC)no subject
Date: 2012-10-03 07:15 am (UTC)Понятно, что мощность такого инструмента невелика.
Или Вы о чём?
no subject
Date: 2012-10-03 04:42 pm (UTC)(Но, как и в теме поста, это не автоматическое доказательство, оно полностью автоматически проверено, и есть помошь со стороны компьютерное системы в его генерации, но оно не "автоматическое без подсказок".)
no subject
Date: 2012-10-03 05:02 am (UTC)no subject
Date: 2012-10-03 05:56 am (UTC)no subject
Date: 2012-10-03 08:00 am (UTC)no subject
Date: 2012-10-05 06:40 pm (UTC)no subject
Date: 2012-10-03 06:16 am (UTC)Все больше и больше умных в у нас.
Date: 2012-10-04 08:05 pm (UTC)The Train Shop offers fans of the popular
Date: 2012-10-05 05:09 am (UTC)[url=http://www.coachbagshopjapan.com/]コーチ バッグ[/url] [url=http://www.coachbagshopjapan.com/]コーチ 財布[/url] [url=http://www.coachbagshopjapan.com/]コーチ アウトレット[/url] コーチ バッグ : http://www.coachbagshopjapan.com/ コーチ バッグ (http://www.coachbagshopjapan.com/)
[url=http://www.coachbagshopjapan.com/]` [/url] [url=http://www.coachbagshopjapan.com/]` [/url] [url=http://www.coachbagshopjapan.com/]` [/url] ` : http://www.coachbagshopjapan.com/ ` (http://www.coachbagshopjapan.com/)
Ааааа.................
Date: 2012-10-07 12:25 am (UTC)http://tractor32.livejournal.com/20081.html