Forwarded from Generative Anton (Anton Repushko)
Сегодня я обрёл тайное знание о JS (разумеется я бы предпочёл сохранить свою психику здоровой, но уже слишком поздно).
UPD: в Python тоже конечно так можно.
UPD: в Python тоже конечно так можно.
Forwarded from сладко стянул
сегодня я узнал, что в 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/
- великую теорему Ферма для регулярных простых (Куммер, 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/
Forwarded from ❆ (Artyom K)
Война с обоссаным вскодом
Пока воевал с обосанным вскодом, я выяснил, что он, так же как и емакс, вероятно, использует интерфейс mi от gdb для отладки.
Вот так выглядит отладка с этим интерфейсом в емаксе.
По сути mi это протокол, про то как гонять текст между дебаггером и редактором:
https://ftp.gnu.org/old-gnu/Manuals/gdb/html_chapter/gdb_22.html
И это снова очень напоминает language server.
Пока воевал с обосанным вскодом, я выяснил, что он, так же как и емакс, вероятно, использует интерфейс mi от gdb для отладки.
Вот так выглядит отладка с этим интерфейсом в емаксе.
По сути mi это протокол, про то как гонять текст между дебаггером и редактором:
https://ftp.gnu.org/old-gnu/Manuals/gdb/html_chapter/gdb_22.html
И это снова очень напоминает language server.