Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Misha Verbitsky ([info]tiphareth)
@ 2020-09-02 11:51:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение: sick
Музыка:Enjoykin - Завтрашний День (feat. Виталий Кличко)
Entry tags:covid

компиляция последних данных по смертности от ковида
Кстати,
компиляция последних американских данных по смертности от ковида
https://reason.com/2020/08/31/cdc-data-confirm-that-young-people-face-a-negligible-risk-of-dying-from-covid-19/
смертность для тех, у кого инфекцию уже обнаружили
(то есть не считая бессимптомных и тех, кто перенес
это дело на ногах) - 0.25% для тех, кто младше 50,
и 16% для тех, кто старше 64.

Если прибавить серологические исследования (которые
позволяют учитывать тех, кто переносят ковид без
симптомов или с симптоматикой обычной простуды),
цифры разнообразнее, от 0.1 процента (Юта) до 1.4
процента (Коннектикут); в среднем, около 0.26%,
в два раза опаснее обычного гриппа, и сравнимо
с эпидемией H2N2-гриппа в 1957 (около 0.2%).
При этом людей с антителами против ковида
где-то в 10 раз больше, чем тех, у кого он
диагностирован, то есть все цифры по диагностированным
пациентам, видимо, можно делить на 10; если так,
оно получается еще менее опасно.

Ну и вот это до кучи:
https://masksickness.ca/mirror/2020-08-26-CDC_IFR_Final-Joseph-Audie.pdf
Review of calculated SARS-CoV-2 infection fatality rates:
Good CDC science versus dubious CDC science, the actual
risk that does not justify the "cure", by Prof Joseph Audie.

Привет

P. S. Пресловутый Gideon Meyerowitz-Katz, ведущий ниспровергатель
Иоаннидиса, опубликовал новый обзор, цифры которого вообще
не расходятся с полученными Иоаннидисом на основе
серологических исследований
https://www.medrxiv.org/content/10.1101/2020.07.23.20160895v4

The estimated IFR is close to zero for children and

younger adults but rises exponentially with age, reaching
0.4% at age 55, 1.3% at age 65, 4.5% at age 75, and 15% at
age 85.

в тексте приводится IFR для других категорий населения,
для младше 35 это 0.01%, для 35-45 0.06%,
для 45-54 это 0.2%, 55-64 - 0.7%, 65-74 - %2.2, 75-85 - 7.3%, 85+ - 27.1%



(Читать комментарии) - (Добавить комментарий)


[info]sometimes
2020-09-02 21:02 (ссылка)
Понятно, что сейчас "дистанционное образование" примерно как Хоукингу набирать языком буквы на клавиатуре голосового синтезатора; вопрос в том, что нужно сделать программисту, чтобы этот барьер стереть. Изображение на экране монитора от изображения на сетчатке принципиально ничем не отличается.

Без упражнений, конечно, совсем бессмысленно. Сдавать задачи студенты могут (и должны как можно раньше) в TeXе, после чего оно обычно обсуждается устно, если есть недочеты; но на первых курсах это, видимо, затруднено, потому что студенты не очень хорошо отличают правильное рассуждение от неправильного.

Ещё помогает планшет для того, чтобы писать значки; особо дешевых вариантов, правда, я не видел пока, для студентов это будет трудно. Калинин пишет лекции стилом на iPad (кажется), это выглядит магнетически.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-02 21:11 (ссылка)

>вопрос в том, что нужно сделать программисту, чтобы этот
>барьер стереть

(и нужно ли вообще)

по крайней мере знакомые
математики ожидают от перехода на дистанционку
ужасов и апокалипсиса, 99% обучения, если его успешно
переведут в онлайн, можно будет вести без преподавателя
вообще, и к этому оно, конечно, в итоге и приведет,
то есть 99% коллег потеряют работу

у меня тут нет особо позиции: я калькулюс никогда
не читал и не планирую, но есть риск, что студенты
выйдут из этих онлайн-курсов окончательными дебилами
(по типу памятного "Harvard calculus project")
потому что централизованная система более
подвержена идеологическим атакам, чем
распределенная

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2020-09-02 21:37 (ссылка)
ВР-дистанционка с кошкодевочками.

(Ответить) (Уровень выше)


[info]kaledin
2020-09-02 21:58 (ссылка)
Причем не только потеряет работу, а еще и преподавание будет говно говном.

Как это относится к калкулусу, мне неведомо, но содержательные курсы онлайн читать по-видимому нет смысла. Я по крайней мере не буду.

>более подвержена идеологическим атакам

Да бог бы с ними с атаками; что хуже, она подвержена накоплению идиотизма по прицнипу positive feedback loop. Атаки отсюда же берутся естественно, но это только цветочки.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-02 22:48 (ссылка)
> по принципу positive feedback loop.

Можно пример? То есть про что это вообще.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-02 22:53 (ссылка)
Про то, что в централизованной монополистической системе глупость амплифицируется, а вверх неизбежно вылезают самые идиоты. Идиотизм которых становится каноническим, и следующие поколения идиотов пляшут уже от этой планки.

Задачу про три чашки по два рубля помнишь? -- где 2 x 3 не равно 3 x 2? Вот типичный артефакт.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-02 23:09 (ссылка)
А, вы на монополию замыкаетесь, я понял (да, про 2x3 помню). Я не думаю, что это реально issue, при удешевлении и стандартизации процесса будет куча интерактивных курсов "про одно и то же" с чуть разными фокусами; по факту это будет просто "формат новой книги". Они будут друг с другом конкурировать, как Хартсхорн с красной книгой Мамфорда и с EGA, а Вуазен с Гриффитсом-Харрисом. Уже сейчас в интернете лежит куча курсов от разных MIT и Stanford, неинтерактивных пока.

Конечно, смысл обучение приобретает только во взаимодействии с преподавателем, который такие курсы будет вспомогательно использовать (то есть это та же книга). На них, наверное, будут гранты выделять, как сейчас на книжки. По крайней мере, там можно отправить решение сложной задачи в TeXе на review, и оно в автоматическом режиме будет взято одним из аспирантов-помощников преподавателей (как те же листочки в 57).

Сейчас вроде ещё есть определенный прогресс в proof assistants (так, чтобы проверяемые решения задач не надували объем, а ассистент сам заклеивал "очевидные шаги"), но не знаю, насколько это будет полезно. Вот этот товарищ большой энтузиаст:
https://www.imperial.ac.uk/people/k.buzzard
Правда, ещё энтузиаст Emily Riehl, она какая-то странная; но мало ли странных людей.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 01:16 (ссылка)
Дело не в монополии самой по себе -- дело в том, что любой курс, прочитанный для абстрактных миллионов, всегда не подходит никому конкретно, и рассчитан не на среднее даже, а на абсолютный минимум. Поэтому идиотским он не может не быть. Именно поэтому никто не учит чисто по учебнику.

>который такие курсы будет вспомогательно использовать

Предлагается, тем не менее, не это.

А это предподавателю нафиг не нужно, потому что уже есть книги; это лишнее колесо в телеге.

>Правда, ещё энтузиаст Emily Riehl, она какая-то странная

Стопроцентное жулье.

And I'm not saying it lightly; я долгое время думал вот какая замечательная, светоч, новое слово, и т.д. и т.п. Но увы. В своей области она некомпетентна, не признавать этого уже не получается. В остальных, соответственно, я уже и знать не хочу.

Ну и proof assitants туда же, естественно; пользы от них в принципе не может быть, вред может, и точно будет, как только про них прознают бюрократы. Т.е. если оно в какой-то области математики приживется, на области можно ставить крест.

>https://www.imperial.ac.uk/people/k.buzzard

Кто такой не знаю, страничка выглядит неприятно (если кто-то считает, что главное в мире это знать что такое perfectoid space... oh well).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-03 01:46 (ссылка)
Баззард точно не Риэль и не жулик, а аспирант Тейлора и крепкий профессионал с премией Уайтхеда в активе (хотя и не звезда). Естественно, ему было интересно научить LEAN определению перфектоида, он же арифметической геометрией занимался (и при чем тут "главное в мире"). Если я правильно помню, геометрии Аракелова он тоже LEAN учил.

Польза от proof assistant я уже написал, какая может быть: научить студента, чем доказательство отличается от галлюцинаций, которые он за доказательства обычно принимает на первом курсе (или на первом году обучения в матшколе). Сейчас (или даже не "сейчас", а сколько-то лет назад: посмотреть на LEAN у меня руки все не доходят) оно для таких целей неприменимо, из-за безумного количества утомительных деталей, которые нужно объяснять тупому устройству.

Если же эту боль удастся/удалось преодолеть (чтобы тупое устройство само заклеивало тупые детали), это решит часть утомительной проблемы, о которой пишет Михаил в комментарии по теории Галуа: не знаю, что там пишут ему, но по крайней мере, у них не получится никак запихнуть в assistant жульническое вычисление группы Галуа кругового поля в обход неприводимости многочлена.

Ну и для научения матлогике тоже нелишнее (наверное; я из матлогики знаю только нумерацию Г. и немножко форсинга).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 01:52 (ссылка)
>научить студента, чем доказательство отличается от галлюцинаций

Это через компьютер не делается, по-моему.

Потому что это в любом случае условность, а железки нюансов не понимают.

>крепкий профессионал

Это хорошо; но любитель buzzwords при этом. Ну и вообще, по моим наблюдениям, страсть к proof assistants обычно возникает после травматическоог опыта (грубо говоря, когда проврешься, а тебе на это укажут).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-03 02:20 (ссылка)
> это в любом случае условность, а железки нюансов не понимают.

я тоже про это подумал (действительно, откуда железке знать, что человеку очевидно, а что - стандартная или нестандартная ошибка; например, в шахматах компьютеру пятиходовая комбинация с жертвой ферзя или с обычными разменами - один хрен, а человек поставит восклицательный знак к жертве, ему ферзя жалко, если он не видит, что он окупится); но, во-первых, в рамках курса логики можно заставлять студента детализировать в случайном месте "до самого низа", а во-вторых, я не уверен, что нужно, чтобы "понимал нюасны" - главное, чтобы их воспроизводил. То есть, грубо говоря, натренировать железку на большом корпусе доказательств (хоть придуманных теми же студентами - на предмет воспроизводящейся лажи), чтобы она запомнила, что "очевидно", а что - "нет"; как в этом пресловутом GPT-3, который не только довел корчевателя до совершенства, но и делает вид, что может рассуждать систематически (например, может решить задачу про вынуть бегемота из холодильника, но на более длинных примерах запинается).

https://www.vox.com/future-perfect/21355768/gpt-3-ai-openai-turing-test-language

Я вот уже не очень понимаю, насколько сильно это за горизонтом. По крайней мере, с этим интересно было бы поиграть. Железяка ничего не умеет (пока) придумывать, только воспроизводить; но местами воспроизводит уже очень хорошо.

Типа, один из примеров
https://www.lesswrong.com/posts/L5JSMZQvkBAx9MD5A/to-what-extent-is-gpt-3-capable-of-reasoning

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 05:56 (ссылка)
>"до самого низа"

Так нет же никакого "до самого низа" на самом деле, и быть не может, теорема Геделя и пр. Это результат конвенции все равно. И оно чисто вербальными средствами передается плохо.

>насколько сильно это за горизонтом

Проблема в том, что они уже сейчас не понимают, как оно работает. Т.е. если научить компьютер доказывать теоремы лучше, чем человек, то науке от этого будет не польза, а феноменальный вред. "Понять значит упростить", а доказать без понимания это убить теорему. А если убийство механизовано, это только хуже.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-03 17:08 (ссылка)
> уже сейчас не понимают, как оно работает.
Не совсем: не "уже", а "ещё". Там параллельно идет деятельность по скальпированию электронных мозгов, в распознаваниях картинок с разных слоев выделяют примитивы разного порядка и т.д. Даже с GPT мы в выигрыше, по сравнению с человеком, потому что за день можно пропустить его через миллионы лет чистилища тестирования.

> Так нет же никакого "до самого низа"
Я вот о чем: допустим, простое утверждение, единичный отрезок компактен. Студент пишет (значками, но я передаю словами): сначала докажем, что можно ограничиться покрытием интервалами: любое открытое множество есть объединение интервалов; потом предположим, что конечного подпокрытия интервалами не существует. Рассмотрим все связные конечные подпокрытия, содержащие левый конец отрезка. Объединение интервалов каждого подпокрытия - интервал. У правых концов множества этих интервалов, занумерованных подпокрытиями, есть верхняя грань. Эта верхняя грань покрыта некоторым интервалом из покрытия, берем подпокрытие, которое пересекается с этим интервалом, получаем противоречие: верхняя грань сдвинулась.

Студент пишет это доказательство, как последовательность утверждений, связанных между собой стрелочками (грубо говоря, это граф с вершинами, покрашенными теоремами). AI расширяет этот граф, добавляя вершины и стрелочки внутрь стрелочек, так чтобы теперь каждая стрелочка соответствовала ровно одному правилу вывода в системе аксиом (например, из аксиоматики ZFC). Получается полностью формальное доказательство компактности отрезка в ZFC (студенту оно не показывается). После этого AI говорит студенту: вот эту свою стрелочку детализируй (выбирая самую сложную, с его точки зрения, или случайную). Он детализирует, почему любое открытое множество есть объединение интервалов (например): потому что по определению интервалы образуют базу топологии в R, а, значит, и на отрезке. Так повторяется, пока некоторую стрелку студент не додетализирует до цепочки из правил вывода в ZFC. Получается что-то вроде "доказательства с нулевым разглашением", о котором говорил Родион (хотя он там и перепутал, как я понимаю, "игры" в смысле фон Неймана-Нэша с играми Банаха-Тарского и Эренфойхта, которые совсем другое, и к "теории игр" отношения не имеют): AI нигде студенту не подсказывает, с одной стороны, студенту не приходится детализировать доказательство целиком до ZFC (это было бы слишком утомительно и объемно), при этом он показывает свое умение рассуждать строго во всех нетривиальных местах.

Возможно, все это и утопия, но вот Баззард вроде бы считает, что нет. И он гораздо менее возвышенный и более приземленный человек, чем Воеводский, так что кто знает.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-04 04:02 (ссылка)
>например, из аксиоматики ZFC

Я, например, в теорию множеств вообще не верю.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-04 15:40 (ссылка)
А зачем в нее "верить", это ж просто модель. Типа, раньше все делали из натуральных чисел, во славу Леопольда Кронекера, но некоторые вещи
делать из натуральных чисел откровенно неудобно (неабелевы группы, например, или топологические пространства). А тут подвернулся Кантор, и придумали модель на этаж более нижнего уровня, из которой можно сделать натуральные числа тоже.

Часто ли в математике за пределы континуальной мощности приходится залезать? Не когда нужно определить "все на свете", типа большой категории, а при работе с конкретными вещами?

Теория множеств, мне кажется, это просто раздел логики (ну, типа, чтобы можно было говорить не только о числах, но и о произвольных функциях N -> N).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 07:46 (ссылка)
Большую категорию надо не определять, а аксиоматизировать. Я не один так думаю, вот например Картье (к которому я вообще-то без любви, но тут он дело говорит):

Senechal: Bourbaki's last publication was in 1983. Why doesn't it publish anything now?

Cartier: There are several reasons for that. [...]

In accordance with Hubert's views, set theory was thought by Bourbaki to provide that badly needed general framework. If you need some logical foundations, categories are a more flexible tool than set theory. The point is that categories offer both a general philosophical foundation—that is the encyclopedic, or taxonomic part—and a very efficient mathematical tool, to be used in mathematical situations. That set theory and structures are, by contrast, more rigid can be seen by reading the final chapter in Bourbaki set theory, with a monstrous endeavor to formulate categories without categories.


Грубо говоря, что любой полный строгий существенно сюрьективный функтор есть эквивалентность (т.е. обратим) очевидно, а аксиома выбора для классов сомнительна. Хотя формально говоря, это строго одно и то же. Дело примерно в том, что обратный к эквивалентности единственный, с точностью до единственного изомоморфизма. Поэтому выбора не то, чтобы нет, но он уже посчитан и учтен.

Кантор не то, чтобы был такой умный придумал множества. Его главная идея была в том, что можно рассматривать множества *без какой-либо дополнительной структуры вообще* -- в то время как реально работающие математики работали с "пространствами", потому что, казалось, что рассматривать большие множества без чего-то типа топологии стремно. Ну и правильно, действительно стремно же! Конечно, все равно приходится, потому что "пространство" еще хуже, но радости в этом никакой нет. По факту же, как мы теперь знаем, "все группы" или что там еще образуют не множество, а категорию, работать с ними нужно "с точностью до изоморфизма", и основания давно пора переписать соответствующим образом.

Забавно, что сейчас временный перевес в борьбе за основания опять за дебилами-американцами, конкретно за "американскими топологами", а они так ничего не забыли и ничему не научились, возвращаются на ту же блевотину, и снова верят в "пространства" (всерьез пеняя Гротендику, например, что тот так и "не осознал", что надо работать "с точностью до гомотопии"). Если бы Бурбаки в 60-е набрались сил, выкинули теорию множеств на помойку, и переписали все с нуля на нормальных категорных основаниях, этой проблемы не было бы. Ну да что уж теперь.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-06 10:00 (ссылка)
У choice же есть вполне себе "малые" "применения", не только про выбор изоморфизма: что спектр кольца не пуст, что отрезок не является объединением счетного семейства нигде неплотных, что произведение семейства компактов компакт, что существуют неглавные ультрафильтры и асимптотические конусы на группах (а не только бессмысленные "несуществующие на самом деле" образования вроде разрезания сферы на две таких же, множества Витали или базиса Гамеля).

Как это объехать без choice (и, соответственно, без голых точек, на которые надевается структура - что в контексте более существенно)?

На комментарий про функан, чтобы два раза не вставать: не знаю про банаховы, но есть Фреше, они вполне осмысленные, типа, все функциональные пространства такие; или там распределения, которые ещё более nuclear.
А, ещё, вспомнил, теорема Гельфанда-Торнхейма про то, что не бывает нормированных полей над C, через теорему Хана-Банаха доказывается, кажется (правда, там не надо полноты, достаточно наличия нормы).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 18:16 (ссылка)
Это не то. Ты мне говоришь, что разумные пространства Фреше в природе бывают. Кто бы сомневался. Банаховы тоже бывают. Но это не значит, что само понятие разумно. Определение разумно, если про определяемый обьект потом можно построить теорию (т.е. доказать сколько-то взаимосвязанных теорем, причем именно в той общности, в которой определение). А здесь не так: теория есть, но весьма куцая, куда более куцая, чем заявленные понты. И когда люди этого не понимают, и начинают изборетать "банаховы многообразия" и прочую подобную лабуду, получается черт-те что.

С аксиомой выбора для множеств я не вижу никаких проблем. Все множества проективны, ну и ок. Хотя рассматривать несчетные множества без топологии все-таки глупо, если можно не, лучше не.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-06 18:41 (ссылка)
> Определение разумно, если про определяемый обьект потом
> можно построить теорию

глупая точка зрения. Про группы (цитирую Громова)
известно, что любое общее утверждение либо тривиально,
либо имеет очень сложный и неинтересный контрпример.
Из этого никак не следует, что само понятие группы
дурацкое. Eсли наложить осмысленные ограничения
(группа Ли, групповая схема, whatever), получаются
очень красивые теории.

То же и с банаховыми пространствами, сами они,
как и абстрактные группы, неинтересные, но есть
масса интересных теорий, которые получаются,
если наложить еще условия, типа C^*-алгебр,

Например, коммутативная банахова C^*-алгебра
это алгебра непрерывных функций на компакте, и
соответствующие категории эквививалентны.
Это утверждение ("теорема Гельфанда-Наймарка")
донельзя содержательное.

Такие дела
Миша

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 18:48 (ссылка)
>Это утверждение

единственное во всей теории, и ему 80 лет.

Причем все его реальное содержание чисто алгебраическое, и этому наблюдению 70 лет.

Какое старье тухлое, право слово.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-06 19:12 (ссылка)

не единственное, есть его аналог, который
позволяет интерпретировать пространства Штейна
как алгебры Фреше с дополнительными структурами
(алгебры Аренса-Майкла), там очень интересная наука с массой применений
https://www.math.uwaterloo.ca/~banalg20/Talks/pirkovskii.pdf
(ну и дофига еще есть, конечно)

все это связано с тем, что алгебра голоморфных
функций, ограниченных на компакте - банахова, и
есть масса применений общей науки про банаховы
пространства (базисы Шаудера, вот это все) к
комплексному анализу

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 20:09 (ссылка)
>очень интересная наука с массой применений

Ни одного применения в докладе я не нашел. Да и теоремы все какие-то на уровне sanity check.

В целом, кто-то наверно должен этим заниматься, ну просто чтоб было, но одного человека вполне хватит (например того, которого ты цитируешь).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-06 20:40 (ссылка)

вот у меня применения
Embedding of LCK manifolds with potential into Hopf
manifolds using Riesz-Schauder theorem
https://arxiv.org/abs/1702.00985

An locally conformally Kahler (LCK) manifold with
potential is a complex manifold with a cover which
admits an automorphic Kahler potential. An LCK
manifold with potential can be embedded to a Hopf
manifold, if its dimension is at least 3. We give a
functional-analytic proof of this result based on
Riesz-Schauder theorem and Montel theorem. We give an
alternative argument for complex surfaces, deducing
embedding theorem from the Spherical Shell
Conjecture.

у Пирковского, естественно, применений нет, он не геометр
но в комплексном анализе оно используется постоянно,
потому что теорема Монтеля это теорема о банаховых
пространствах на самом деле.

Nаиболее внятная
ее формулировка такая: пусть A\subset B
два компакта в комплексном многообразии,
причем A лежит во внутренности B,
C_A, C_B алгебры голоморфных
функций, ограниченных на A, B,
с нормой максимума на A, B.
Тогда отображение ограничения
из C_B в C_A - компактный оператор.

именно эту версию использовал Гротендик,
когда доказывал, что когомологии когерентных
пучков конечномерные (он там походу "монтелевские
пучки" изобрел, весь аргумент - чисто банахова
алгебра).

A sheaf of Abelian groups F over a locally compact topological space X is called
a Fre'chet-Montel sheaf (cf. [4]) if the following conditions are satisfied:

(a) for every open set U c X the group of sections F(U; F) is a Frechet topo-
logical vector space;

(b) for any two open sets V c U in X the restriction map F(U; F) -* F(V; F)
is linear and continuous, and completely continuous when V is relatively compact

in U.


(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 21:10 (ссылка)
>именно эту версию использовал Гротендик, когда доказывал, что когомологии когерентных пучков конечномерные

Ну все-таки это тоже было очень давно.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-06 21:47 (ссылка)
а комплексный анализ как самостоятельная наука помер
примерно тогда же

сейчас это просто набор методов, применяемых в геометрии

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-07 00:26 (ссылка)
Что не особо хорошо, вообще-то. Лучше бы таки понять, почему Калаби-Яу. Но что делать.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-07 00:57 (ссылка)
к этому идет
но там комплексного анализа не то чтобы сильно много

(Ответить) (Уровень выше)


[info]sometimes
2020-09-06 19:49 (ссылка)
> Все множества проективны, ну и ок.
Я не совсем это говорю, нет проблемы со свойствами морфизмов в категории Set (наличие сечения), есть проблема в том, что кольца приходится делать из множеств (то есть уже теория колец и проч. вкладывается в теорию множеств, и вуаля). Я видел на mathoverflow такого рода, например, ответ: а нефиг рассматривать кольца, в которых нельзя построить все идеалы руками. По-моему это чрезмерный максимализм, например, нужно отказаться от рассмотрения кольца гладких функций на некомпактном многообразии (ну и вообще не уверен, что в таких узких рамках будет удобно).

Про "банаховы многообразия" я совсем не знаю; знаю, что когда-то давно хотели "группы и алгебры токов" запихнуть в некий генеральный сеттинг аналогов бесконечномерных гладких многообразий (в связи с физикой), но не знаю, насколько преуспели.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 20:18 (ссылка)
>нужно отказаться от рассмотрения кольца гладких функций на некомпактном многообразии

Это сколько угодно, хоть бы даже и на компактном (рассматривать его как просто кольцо все равно чрезвычайно глупо). Проблема в том, что тогда нужно отказаться и от нетеровых колец, а это уже не годится, конечно.

При этом коммутативная алгебра это наука не замкнутая, и по-человечески она не строится. Факт в принципе хорошо известный и задокументированный. Но здесь уж делать нечего, пишем на том, что есть.

А так-то, ну, ничего плохого в том, чтобы что-то строить из множеств, я не вижу, бывает даже очень изящно. Знаешь же современное определение компактного хаусдорфова топ. пространства, через codensity comonad? Берешь вложение конечных множеств во все, берешь его правое расширение Кана, получаешь эндофунктор всех множеств, который еще и комонада (в явном виде, множество переходит в множество ультрафильтров на нем). Коалгебры это компактные хаусдорфовы пространства и есть.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 21:12 (ссылка)
Только вру -- не комонада, а монада (и соотв. алгебра, а не коалгебра).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-06 21:41 (ссылка)
Вроде да, отображение множества в ультрафильтры это монада.

(Ответить) (Уровень выше)


[info]sometimes
2020-09-06 21:40 (ссылка)
> Знаешь же
Не знал, сейчас разбираюсь (только вроде монада, если рассматривать не Set^{op}, а не комонада, и алгебра над ней).

Кстати, мне всегда определение топ. пространства казалось загадочным - собственно, исток этой загадочности в определении непрерывности на R (откуда и происходит, видимо, "категория открытых множеств"). То есть не то чтобы даже загадочным, определение непрерывности через пределы было "технический трюк, чтобы построить осмысленные морфизмы на кусках R^n", а то, что оно эквивалентно определению через открытые множества - некоторое волшебство.

Возвращаясь к proof verification, тогда я не понимаю, если мы строим из множеств, в чем проблема формальной проверки на корректность через ZF (а C никаких новых противоречий не добавит, как как раз Гедель нам и объяснил; кстати, если все ультрафильтры главные, в отсутствие C, конструкция ломается). Выбираем одно из стандартных вложений изучаемой теории в теорию множеств, и дальше эта штука по факту spellchecker.

(Ответить) (Уровень выше)


[info]sometimes
2020-09-04 15:42 (ссылка)
Ну то есть, в смысле, вкладывание математики в теорию множеств - это типа как реализация машины Тьюринга на Conway's game of life. А нужно, чтобы можно было убедиться, что доказательство без дырок.

(Ответить) (Уровень выше)


[info]sometimes
2020-09-03 17:46 (ссылка)
> доказать без понимания это убить теорему.

Разумеется; но это просто выставляет другой статус "машинному доказательству", что-то вроде численных экспериментов Берча и Суиннертон-Дайера. Сейчас уже довольно приличный массив таких "доказательств" размером в десять терабайт, в которых обходится огромный граф, на манер доказательства Four Colors Theorem.

Вот показательный пример, что "материя не пропадает":

Акт первый:

In February 2014, Alexei Lisitsa and Boris Konev of the University of Liverpool showed that every sequence of 1161 or more elements satisfies the conjecture in the special case C = 2, which proves the conjecture for C ≤ 2. This was the best such bound available at the time. Their proof relied on a SAT-solver computer algorithm whose output takes up 13 gigabytes of data, more than the entire text of Wikipedia at that time, so it cannot be independently verified by human mathematicians without further use of a computer.

Ни один здоровый человек не сочел бы это доказательством, конечно - это просто подтверждение. Поэтому

Акт второй:

In September 2015, Terence Tao announced a proof of the conjecture, building on work done in 2010 during Polymath5 (a form of crowdsourcing applied to mathematics) and a suggestion made by German mathematician Uwe Stroinski on Tao's blog.

Это было нормальное совершенно обычное доказательство на несколько страничек, и оно небось даже что-то объясняет (к сожалению,
это комбинаторика и функан, не знаю их).

https://en.wikipedia.org/wiki/Sign_sequence

Не вижу, кстати, в этом для математики ничего особо нового: давно существуют огромные невнятные манускрипты, вроде доказательства Новикова-Адяна, или даже с неисцелимыми ошибками, как мемуар Дюлака. Потом люди лучше разбираются в происходящем, и пишут внятные и глубокие вещи. Computer proof - это just another step to the Hell. Трудно себе представить, что вся математика (или какая-то вообще невспомогательная часть) будет состоять из них, в этом нет смысла.

Компьютерные шахматы, например, не убили человеческие (в эпоху переборных движков шахматы у компьютеров были причем дико скучные, а сейчас в нейросетях они повеселели и какие-то позиционные идеи в человеческие вбросили, там есть очень красивые партии теперь, в духе классиков начала 20 века), и автомобили не уничтожили бег. При правильной постановке дел, мне кажется, это добавит некоторое измерение и возможность (вроде проверки верности гипотезы в каких-то случаях, и нахождения контрпримеров).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-04 04:01 (ссылка)
>к сожалению, это комбинаторика и функан, не знаю их

И неудивительно: их нет.

Я в детстве очень хотел выучить все теории, которые бывают, но у меня проблема с теорией графов -- по ней была в природе книга, какого-то там Харари, но она была библиографческая редкость. И я очень страдал.

А потом вырос, и узнал, что теории графов не бывает. Есть некоторый не вполне связный набор трюков, а теории никакой нет.

Если у какой-то реально важной гипотезы вдруг найдется машинное доказательство, это будет дико вредно, потому что убьет предмет на корню. Ну там, Берча-Свиннертон-Дайера хотя бы можно применять как черный ящик, хотя радости тоже мало (никого не ебут эллиптические кривые, ебут общие алгебраические многообразия, а это просто конкретный тестовый случай). Но скажем гипотеза Римана сама по себе нафиг никому нормальному не нужна, вообще. И жутко важна только потому, что всем интересно, как именно ее докажут. А передоказывать за машиной дураков нет.

>https://en.wikipedia.org/wiki/Sign_sequence

Ненавижу такое. Эрдеш это 100% зашквар.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-04 15:30 (ссылка)
> передоказывать за машиной дураков нет.
А Фюрстенберг не передоказывал за Семереди? (как будто есть какая-то разница между ним и Deep Blue).

Что касается "графов" - ну клеточные пространства размерности 1 они. Собственно, Эйлер же их и придумал, как 1-остов сферы; и посчитал у нее группу гомологий, б.м. Какая может быть "теория" у 1-остовов?

Ещё их можно линеаризовать, классика же:
http://www.cs.yale.edu/homes/spielman/PAPERS/SGTChapter.pdf
Практически ряд Гильберта.
Но это вряд ли было у "Харари".

Вообще понятно, что слова нет, но жопа-то же есть. Например, меня в детстве очень раздражала "лемма Шпернера" из (не очень, увы, хорошей) книжки про теорему Брауэра о неподвижной точке (там про пересечение графика с диагональю вообще ни слова, при том, что у того же автора в той же серии, кажется, есть книжка про эйлерову характеристику), но потом я примерно понял, что это в каком-то смысле естественный перевод на дискретный язык, типа как в табличке:
https://en.wikipedia.org/wiki/Borsuk%E2%80%93Ulam_theorem#Equivalent_results
А когда проводятся параллели, это всегда интересно.

Или там с функаном - теории, может, и нет, но векторам состояний и гладким функциям и распределениям на многообразии и гладким сечениям расслоения и гармоническим формам надо же где-то жить.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-06 07:50 (ссылка)
С гильбертовыми пространствами нет проблем. Банаховы уже, по-видимому, бессмысленны -- определение не описывает точно ничего реального (что убедительно доказал Говерс, придумав патологические контрпримеры более-менее ко всему). А такие определения не особо полезны. Ну и получается набор фактов, а по сути набор трюков.

(Ответить) (Уровень выше)


(Анонимно)
2020-09-03 02:24 (ссылка)
>страсть к proof assistants обычно возникает после травматическоог опыта

Я смотрел его лекцию (кажется эту https://www.youtube.com/watch?v=Dp-mQ3HxgDE) и он говорил, что у него действительно был травматический опыт -- ему дали статью на peer review, в которой он нашел ошибку, но сабмитер годами продолжал нагло утверждать что никакой ошибки там нет, и это был для него очень неприятный, нервирующий, затяжной конфликт, где он в результате победил.

Не думаю, что что-то есть плохое в том, что математика будет параллельно заформализована на компе, особенно если будет прорыв, и это дело сделают significantly less time consuming. В плане trustworthiness теорем, и удобства для программистов одни сплошные бенефиты. Могут конечно начать требовать формализации, но это не в этом, и не в следующем десятилетии. Вам к тому времени уже будет похуй.

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2020-09-03 03:14 (ссылка)
>и он говорил, что у него действительно был травматический опыт

Нашел https://youtu.be/Dp-mQ3HxgDE?t=3149

(Ответить) (Уровень выше)


[info]kaledin
2020-09-03 06:02 (ссылка)
>нервирующий, затяжной конфликт, где он в результате победил

Это еще хороший вариант. Плохой это когда сам проврался. С Воеводским было именно так, например.

>удобства для программистов

А математика здесь причем? Математике программисты в лучшем случае бесполезны, хорошо если не вредны.

Математика и программирование устроены принципиально по-разному. Компьютер он железный, а теоремы доказываются для людей. Доказательство, которое ссылается на непонятный черный ящик, пусть даже проверенный компьютером, это дело весьма вредоносное. Не надо нагромождать одно на другое, оно неизбежно ебнется. Реальное развитие математики происходит методом упрощения, высота башни в любом момемнт времени ограничена (и невелика). Развитие идет не вверх, а куда-то вбок, непредсказуемым образом. Ризома типа. Все по Делезу. А башни пусть строят всякие древние тоталитарные вавилоняне.

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2020-09-03 07:14 (ссылка)
>А математика здесь причем?

Для прикладных целей же. Криптография например. Удобно иметь библиотеку теорем для верификации кода.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 07:29 (ссылка)
Все теоремы, которые нужны в криптографии, вполне тривиальны.

Ну, в очень продвинутых версиях полезна оценка на число точек эллиптических кривых, кажется, т.е. гипотезы Вейля, но даже с ним все понятно безо всяких компьютеров.

(Ответить) (Уровень выше)


(Анонимно)
2020-09-03 20:03 (ссылка)
код тоже пишется для людей, положим доказательства будут писаться в виде кода

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-04 04:08 (ссылка)
Нет. Люди там вторичное; до людей есть компьютер, который или работает, или нет. А в математике никакого компьютера не предусмотрено, и это фича, а не баг.

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2020-09-08 18:50 (ссылка)
понял, действительно
во всяких coq приходится учитывать всякую техническую хуйню
очевидные вещи объяснять.
как и в программировании, от идеи до решения недели-месяцы

люди - не вторичное конечно, важно нахуярить побыстрее и чтобы поддерживать можно было. но компьютер тоже приходится учитывать

(Ответить) (Уровень выше)


(Анонимно)
2020-09-03 02:30 (ссылка)
>proof assistants

Да, и лет через 30 может вообще математики будут не нужны, с proof assistants или нет. Запустят какой-нибудь "math discovery AI" и он наоткрывает всю математику с нуля, причем с возможностью сконвертировать в читаемую человеками форму. Сингулярность типа. Приятно конечно думать про "квантовые мозги" и всё такое, но сейчас уже очевидно что хуита.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 06:03 (ссылка)
Дураку многое очевидно. Мне скорее очевидно, что "AI" как был хайп тупой, так и остался, с "илоном маском" во главе.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-03 06:06 (ссылка)
не вполне
гуглопереводчик работает очень хорошо,
то есть с испанского на английский, например,
даже грамматически правильный текст выдает
а он на нейросетях плюс CFG

(собственно, весь современный осмысленный AI это
нейросети плюс CFG, [info]sometimes уже упоминал сие)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 06:13 (ссылка)
Переводчик и Го. Но что-то мне кажется, что дальше все. Перевод это все-таки сильно формализованная вещь, и к нему есть куча трейнинг-материала.

В смысле, ну машину оно водить научится, тут нет вопросов. М.б. ставить рутинные диагнозы, или даже не рутинные. Но науки вряд ли (в ближайшие лет 50, дальше не знаю).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]lolepezy
2020-09-03 16:13 (ссылка)
AI нынче сложно назвать фуфлом.
Там много фуфла, потому что денег много и много желающих примазаться,
но с этого года начиная, скажем, GPT-3 -- вполне себе нормальное такое
движение в сторону вот прямо серьезного ИИ. Ну типа если научить машинку
на терабайтах текста, то она начинает решать арифметические примеры при
том, что арифметики ее никто не учил. И там еще огромное пространство для
роста, как говорят.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-03 16:39 (ссылка)
А черт его знает, что там внутри происходит (все-таки через нее весь интернет пропустили,
там наверняка были какие-то примеры арифметики для детей; хотя понятно, что оно немножко
выходит за). Впрочем, в отличие от человеческого мозга, насчет изучения этих моделей
простор для оптимизма - можно за день его нагрузочно натестировать миллионами лет
субъективного времени. И в любой узел весов засунуть электрод.

Плохо, что веса не находятся в публичном доступе пока. Но это дело нескольких лет, полагаю
(конкуренты скоро накинутся, их много).

(Ответить) (Уровень выше)


(Анонимно)
2020-09-03 20:06 (ссылка)
в 1960 была пара игрушечных примеров и море обещаний
в 1980 была пара игрушечных примеров и море обещаний
сейчас ровно такая же хуйня, скоро будет опять ремиссия, ai winter
я даже видел каких усилий стоит сделать эту пару иргушечных примеров
хуй они это обобщат

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]panduro
2020-09-04 12:28 (ссылка)
проснись, мойшин лёрнингом уже кучу сфер, где белые воротнички работали, автоматизировали, и многие в процессе

(Ответить) (Уровень выше) (Ветвь дискуссии)


(Анонимно)
2020-09-04 19:38 (ссылка)
Лол, это потому что в этих сферах вообще никакой интеллект не нужен.

(Ответить) (Уровень выше)


(Анонимно)
2020-09-03 02:59 (ссылка)
Coqовец про lean:

https://github.com/coq/coq/issues/10871

"TL;DR: Lean support for quotients is FUD. They break an essential metatheoretical property of CIC. Coq people care for this kind of properties, and prefer extending the theory much more slowly at a cost of reduced expressivity"

(Ответить) (Уровень выше)


[info]p_k
2020-09-03 11:35 (ссылка)
> Стопроцентное жулье.

Что, правда? Я наткнулся как-то на ее текст "Category theory in context", вроде был ничего (но мне много не надо, нужен был справочник для прикладных целей).

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 15:34 (ссылка)
Ну... ну да, по-моему. Увы.

Т.е. она типа как бы хорошая, пишет бойко, но например, не отлавливает простые ошибки в вещах, по которым писала диссертацию. Ну и теорем соответственно не имеет. Будущий Майк Хопкинс в юбке (или что они там теперь носят).

(Ответить) (Уровень выше)


[info]tiphareth
2020-09-03 01:24 (ссылка)
>оно в автоматическом режиме будет взято одним из
>аспирантов-помощников преподавателей (как те же листочки в 57).

а что толку?
результатом будет один бит информации,
"правильно/неправильно"

научиться этак ничему невозможно

(Ответить) (Уровень выше)


[info]maxmornev
2020-09-03 13:54 (ссылка)
> Вот этот товарищ большой энтузиаст:

У Баззарда кризис среднего возраста (сам говорит), он забросил науку к херам.
Кевин хороший, и по жизни адский панк, но такое с каждым может случиться.

Знаменит вот этим достижением в программе Ленглендса:
http://wwwf.imperial.ac.uk/~buzzard/maths/research/papers/eigenvarieties.pdf

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-03 14:10 (ссылка)
> забросил науку к херам
я заметил (поэтому и написал "занимался арифметической геометрией", а не "занимается"). Тем не менее, как я понимаю, он адски преподает;
список достаточно впечатляющий (размером)
https://genealogy.math.ndsu.nodak.edu/id.php?id=49405
не знаю, конечно, как много людей в результате остаются; как раз у вас хотел про Баззарда спросить.

То есть понятно, что эта его нынешняя деятельность отнимает у него массу времени, и, видимо, он ей доволен; но по крайней мере он вполне компетентный чел, а не выдающийся представитель ЛГБТ-сообщества.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]maxmornev
2020-09-03 15:01 (ссылка)
> список достаточно впечатляющий (размером)

Это английский подход к жизни.
У Кевина репутация лучшего теоретика чисел в Лондоне.
Все студенты, интересующиеся чем-нибудь таким,
идут к нему, чтобы иметь шанс на трудоустройство.
"Если вы не учились у лучшего из лучших, то зачем вы
нам нужны."

(Ответить) (Уровень выше)


[info]kaledin
2020-09-03 15:39 (ссылка)
А, ну ок. А перфектоиды прямо на страничке потому что студенты все время спрашивают. Бывает.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]maxmornev
2020-09-03 16:04 (ссылка)
Он забросил дело, но панковать не перестал.

(Ответить) (Уровень выше)


[info]tiphareth
2020-09-03 01:15 (ссылка)

>Я по крайней мере не буду.

я пару раз подкатывал к Вышке, чтобы меня поставили читать
теорию Галуа на Курсере, для эксперимента, говорят, оба
раза мою кандидатуру заблокировал лично ректор, во
избежание репутационного ущерба для конторы (в результате
ее прочла Катя, очень хорошо)

но делать это в Импе абсолютно бестолку, для
онлайн-курса нужно сильно больше ассистентов,
там тупо нет (ну и неинтересно это, если честно,
я более-менее все, что мне могут студенты
написать в качестве решения упражнений,
уже читал, и перечитывать не хочу;
оно почти все уныло и неправильно, но, чтобы
рассказать им, где именно уныло и где неправильно,
надо лично общаться, и с доской; без этого никто
ничему, думаю, не обучится)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 01:18 (ссылка)
Меня просто Вадик Вологодский с Гориновым развели в феврале-марте читать стабильную теорию гомотопий. Но если ковид не кончится, я не буду.

(Ответить) (Уровень выше)


(Анонимно)
2020-09-03 07:09 (ссылка)
>теорию Галуа на Курсере, для эксперимента
>прочла Катя, очень хорошо

зарегался, смотрю

может Open edX поднять или Moodle? тоже для эксперимента

(Ответить) (Уровень выше)


[info]sometimes
2020-09-02 22:46 (ссылка)
А чего за Harvard calculus project?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-02 22:54 (ссылка)
Попытка создать новый, модный, молодежный и современный курс калкулуса (и впарить его всей стране). В начале 90-х. Получилось еще хуже, чем среднее по больнице.

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-02 23:14 (ссылка)
https://math.stackexchange.com/questions/3481/what-is-reform-calculus
это про него?

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]tiphareth
2020-09-03 00:46 (ссылка)
ugu
http://people.math.harvard.edu/~knill///pedagogy/harvardcalculus/index.html

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]sometimes
2020-09-03 01:15 (ссылка)
Ага, спасибо. Да, это ужасно выглядит, примерно понятно, что у людей потом в голове.

(Ответить) (Уровень выше)


[info]tiphareth
2020-09-03 01:00 (ссылка)
http://www.actuarialoutpost.com/actuarial_discussion_forum/attachment.php?s=40cdd48763521c8a7e0ad544d603def1&attachmentid=3436&d=1143499732
весьма аккуратное изображение этого самого проекта
(автор хотел пародию, но получилось неотличимо от оригинала)

(Ответить) (Уровень выше) (Ветвь дискуссии)


[info]kaledin
2020-09-03 01:20 (ссылка)
Гениально вообще!

Every concept in Calculus has THREE interpretations: Geometrical, Numerical, Physical, and Financial.

(Ответить) (Уровень выше)


[info]tiphareth
2020-09-03 01:16 (ссылка)
получилось феерически плохо
(я там был и даже немного бабла на этом говне наварил,
тому що деньги не пахнут)

вот оно в очищенном состоянии
http://www.actuarialoutpost.com/actuarial_discussion_forum/attachment.php?s=40cdd48763521c8a7e0ad544d603def1&attachmentid=3436&d=1143499732

(Ответить) (Уровень выше)


(Читать комментарии) -