Верификация док-ва Великой теоремы Ферма системой Coq

[docent71]

Добрый вечер, уважаемые коллеги! Ведущая международная мировая система верификации математических доказательств Coq сказала, что данное доказательство Великой теоремы Ферма верно. Проверьте пожалуйста это утверждение.

https://github.com/Gendalf71/FLT-Coq

[mihaild]

Гипотезу на 162 строчке нужно доказать.

[tolstopuz]

А если серьезно, то вот здесь идет длительный процесс формализации в Lean.
https://github.com/ImperialCollegeLondon/FLT
https://xenaproject.wordpress.com/2024/ ... its-going/

А здесь закончена формализация доказательства для регулярных простых.
https://github.com/leanprover-community/flt-regular

[Shadow]

Бредогенератор в работе писал(а):

$z^n-x^n=y^n \quad (2.2)$

$(m^n+p^n)^n-(m^n-p^n)^n=y^n \quad (2.3)$

Переход от 2.2 к 2.3 можно считать эквивалентными. Докажем это строго математически:
...

$m=\sqrt[n] {\dfrac{z+x}{2}}$

$p=\sqrt[n] {\dfrac{z-x}{2}}$

Мы получили строгие математические выражения для $m$ и $p$.

Уравнения

$z^3-x^3=26y^2$ и

$(m^3+p^3)^3-(m^3-p^3)^3=26y^3$

можно считать эквивалентными (доказательство выше).

$z=3,x=1$,y=1. Конечно, есть строгие математические выражения для $m,p$

$m=\sqrt[3] 2, n=1$

А вот почему дальше автор работает с $m,p$ как с целыми непонятно. Бред короче.

[Shadow]

Shadow в сообщении #1702734 писал(а):

А вот почему дальше автор работает с $m,p$ как с целыми непонятно.

Извиняюсь, не работает как с целыми, но все равно бред.