Notice: file_put_contents(): Write of 763 bytes failed with errno=28 No space left on device in /var/www/group-telegram/post.php on line 50

Warning: file_put_contents(): Only 8192 of 8955 bytes written, possibly out of free disk space in /var/www/group-telegram/post.php on line 50
сладко стянул | Telegram Webview: sweet_homotopy/1957 -
Telegram Group & Telegram Channel
сегодня я узнал, что в Lean'е уже формализовали (то есть записали математическое доказательство, строгость которого проверена на компьютере):

- великую теорему Ферма для регулярных простых (Куммер, 1847)
- основную теорему арифметики, основную теорему алгебры, основную теорему анализа
- выворачивание сферы наизнанку (Смейл, 1957)
- независимость континуум-гипотезы от ZFC (Гёдель, 1940 + Коэн, 1963)
- всякие абстрактные понятия, введенные Шольце (перфектоиды, жидкие векторные пространства...)
- некоторые свежие результаты аддитивной комбинаторики
- довольно много фундаментальной математики https://leanprover-community.github.io/undergrad.html

#картинка:
https://leanprover-community.github.io/lean-perfectoid-spaces/

А из "ста великих теорем" на данный момент формализованы (хотя бы в одном из proof assistant'ов) все, кроме великой теоремы Ферма:
https://www.cs.ru.nl/~freek/100/



group-telegram.com/sweet_homotopy/1957
Create:
Last Update:

сегодня я узнал, что в Lean'е уже формализовали (то есть записали математическое доказательство, строгость которого проверена на компьютере):

- великую теорему Ферма для регулярных простых (Куммер, 1847)
- основную теорему арифметики, основную теорему алгебры, основную теорему анализа
- выворачивание сферы наизнанку (Смейл, 1957)
- независимость континуум-гипотезы от ZFC (Гёдель, 1940 + Коэн, 1963)
- всякие абстрактные понятия, введенные Шольце (перфектоиды, жидкие векторные пространства...)
- некоторые свежие результаты аддитивной комбинаторики
- довольно много фундаментальной математики https://leanprover-community.github.io/undergrad.html

#картинка:
https://leanprover-community.github.io/lean-perfectoid-spaces/

А из "ста великих теорем" на данный момент формализованы (хотя бы в одном из proof assistant'ов) все, кроме великой теоремы Ферма:
https://www.cs.ru.nl/~freek/100/

BY сладко стянул




Share with your friend now:
group-telegram.com/sweet_homotopy/1957

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

Telegram has gained a reputation as the “secure” communications app in the post-Soviet states, but whenever you make choices about your digital security, it’s important to start by asking yourself, “What exactly am I securing? And who am I securing it from?” These questions should inform your decisions about whether you are using the right tool or platform for your digital security needs. Telegram is certainly not the most secure messaging app on the market right now. Its security model requires users to place a great deal of trust in Telegram’s ability to protect user data. For some users, this may be good enough for now. For others, it may be wiser to move to a different platform for certain kinds of high-risk communications. As a result, the pandemic saw many newcomers to Telegram, including prominent anti-vaccine activists who used the app's hands-off approach to share false information on shots, a study from the Institute for Strategic Dialogue shows. The regulator took order for the search and seizure operation from Judge Purushottam B Jadhav, Sebi Special Judge / Additional Sessions Judge. Telegram Messenger Blocks Navalny Bot During Russian Election To that end, when files are actively downloading, a new icon now appears in the Search bar that users can tap to view and manage downloads, pause and resume all downloads or just individual items, and select one to increase its priority or view it in a chat.
from es


Telegram сладко стянул
FROM American