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: |

A Russian Telegram channel with over 700,000 followers is spreading disinformation about Russia's invasion of Ukraine under the guise of providing "objective information" and fact-checking fake news. Its influence extends beyond the platform, with major Russian publications, government officials, and journalists citing the page's posts. But Telegram says people want to keep their chat history when they get a new phone, and they like having a data backup that will sync their chats across multiple devices. And that is why they let people choose whether they want their messages to be encrypted or not. When not turned on, though, chats are stored on Telegram's services, which are scattered throughout the world. But it has "disclosed 0 bytes of user data to third parties, including governments," Telegram states on its website. It is unclear who runs the account, although Russia's official Ministry of Foreign Affairs Twitter account promoted the Telegram channel on Saturday and claimed it was operated by "a group of experts & journalists." Lastly, the web previews of t.me links have been given a new look, adding chat backgrounds and design elements from the fully-features Telegram Web client. And while money initially moved into stocks in the morning, capital moved out of safe-haven assets. The price of the 10-year Treasury note fell Friday, sending its yield up to 2% from a March closing low of 1.73%.
from us


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