Anatoly Vorobey (avva) wrote,
Anatoly Vorobey
avva

Category:

теорема фейта-томпсона (математическое)

Доказательство теоремы Фейта-Томпсона в теории групп полностью формализовано и проверено в проверщике Coq.

(теорема Фейта-Томпсона гласит, что любая конечная группа нечетного порядка разрешима. Она была доказана в 60-х и легла в основу программы классификации простых конечных групп)

Это, несомненно, самое значительное достижение в области автоматических проверок математических доказательств до сих пор. Группа исследователей работала над этим результатом в течение 6 лет. Математическая польза от этого конкретного результата, полагаю, близка к нулю. Будущее покажет, какую пользу принесет вся эта область в целом.
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 25 comments