Всегда очень любил Воеводского и все эту историю о HoTT. Программу, которую он бы написал за пару лет доказывать и проверять вручную не пришлось бы - для того HoTT и задумывался - комп бы все проверил - и если она бы "скомпилировалась", то можно было бы сказать, что все ОК.
Да, скорее всего вы правы. Я немного не в теме по данному вопросу. Надо будет выпустить отдельный цикл по подходам к компьютерному доказательству теорем, и разобраться))
Я вот недавно подумал вот о чём (некое беспокойство): квантуя макрообъект (R^4, локаное квантование), например, электромеханическую тележку с близкими к человеку параметрами не погнёт ли стойку (всмысле не останутся ли остаточные деформации после того как процесс завершится, т.е. вернёт ли телега свой рабочий/механический вид)??? Я уже знаю как дифференциальной форме записать это квантование. Интегрирование на мой взгляд в некоторых моментах принциально сложнее (требуется огромный опыт/навык), но ключевые вещи можно поставить в уже известные формулы - будет известна "сила" с которой "конечности" будут выворачиваться. Немного поразмыслив я понял, что большого смысла в этом нет (для маленьких и средних машин), но для больших и огромных (длиномеры, "козловые краны" и прочее, разумеется, с адаптацией под квантование) - это вопрос ни на один миллион рублей, например, и дураку ясно, что огромный "башенный кран" сложится как оригами; этот вопрос будет интересен конструкторам по большой технике с уклоном квантования, т.к. сопромат, там, конечно, нужен, но плодов этом деле он явно не даст. Это пока последняя прикладная мысль по поводу квантования
5:36 но мне кажется это и весь смысл, ты создаёшь тип теоремы которой ты хочешь доказать, и конструируешь терм этого типа и если компилируется, то значит теорема доказана, в отдельной проверке нуждается только формулировка теоремы на этом языке
5:21 можно было бы попробовать зафайнтюнить LLM уровня GPT-4o для генерации подобного кода LLMки хорошо справляются с задачей генерировать типовой код, и хотя в данном случае, подозреваю, это не сработало бы "из коробки" (предметная область кардинально отлична от того что LLM могла видеть на github/stackoverflow в процессе обучения), но прогресс в данном направлении движется быстрее чем успевают выходить новые ролики на RUclips (не говоря уже о многолетнем написании программы вручную)
Это смешно, мне о1 врала о том как запихнуть проект с зависимостями в один jar'ник в определенной версии градла, хотя это не сакральные знания и ответ просто есть в доках.
на Хабре есть тесты нейронок по решению детских задач типа "есть 16 конфеток, как разделить чтобы у Васи было на 2 конфетки больше чем у пети» только gpt4 справляется с 70% таких задач... Не путайте имитацию интеллекта за счёт бигдата с интеллектом... там до доказательства теорем как до луны...
то есть сами математики не понимают, что наворотили. какие-то абстрактные теоремы без цифр, какие-то афторитеты от математики, которых никто не проверяет /рукалицо
Во многих отраслях науки этот кризис есть и там-то как раз намного хуже, и невозможно проверить и никто и никогда системно их не проверяет. Математика счастлива тем, что в ней можно проверять доказательства. Впереди всех конечно находится Computer Science / Informatique, созданные алгоритмы можно запрограммировать и проверить тестами (разные тесты есть не только unit-tests), а также важно, что часто возможна формальная верификация.
@Alpasonic 0 seconds ago Замечательный ролик. Спасибо. (Только всё же не "Гортензик", а Гротендик (Alehander Grothendieck) И ударение на последнем слоге.
Всех с наступившим!!!
Не мог на ютубе поздравить ранее из-за проблем с доступом.
Перемещайтесь все в телеграм или вк
Спасибо, что выложили данное видео в открытый доступ!
Георгий Шабат? У меня его родственница матан преподавала в универе) Наталья Алексеевна Шабат. Жеееесть.
Всегда очень любил Воеводского и все эту историю о HoTT.
Программу, которую он бы написал за пару лет доказывать и проверять вручную не пришлось бы - для того HoTT и задумывался - комп бы все проверил - и если она бы "скомпилировалась", то можно было бы сказать, что все ОК.
Да, скорее всего вы правы. Я немного не в теме по данному вопросу. Надо будет выпустить отдельный цикл по подходам к компьютерному доказательству теорем, и разобраться))
Встретиться в будущем и проверить верность предсказаний каждый может, а ты математически докажи…
"Каких же умопомрачительных высот может достичь мышление, если с самого начала пойти в неправильном направлении."
"О наступающей сингулярности в развитии языка описания."
Я вот недавно подумал вот о чём (некое беспокойство): квантуя макрообъект (R^4, локаное квантование), например, электромеханическую тележку с близкими к человеку параметрами не погнёт ли стойку (всмысле не останутся ли остаточные деформации после того как процесс завершится, т.е. вернёт ли телега свой рабочий/механический вид)???
Я уже знаю как дифференциальной форме записать это квантование. Интегрирование на мой взгляд в некоторых моментах принциально сложнее (требуется огромный опыт/навык), но ключевые вещи можно поставить в уже известные формулы - будет известна "сила" с которой "конечности" будут выворачиваться. Немного поразмыслив я понял, что большого смысла в этом нет (для маленьких и средних машин), но для больших и огромных (длиномеры, "козловые краны" и прочее, разумеется, с адаптацией под квантование) - это вопрос ни на один миллион рублей, например, и дураку ясно, что огромный "башенный кран" сложится как оригами; этот вопрос будет интересен конструкторам по большой технике с уклоном квантования, т.к. сопромат, там, конечно, нужен, но плодов этом деле он явно не даст. Это пока последняя прикладная мысль по поводу квантования
5:36 но мне кажется это и весь смысл, ты создаёшь тип теоремы которой ты хочешь доказать, и конструируешь терм этого типа и если компилируется, то значит теорема доказана, в отдельной проверке нуждается только формулировка теоремы на этом языке
5:21 можно было бы попробовать зафайнтюнить LLM уровня GPT-4o для генерации подобного кода
LLMки хорошо справляются с задачей генерировать типовой код, и хотя в данном случае, подозреваю, это не сработало бы "из коробки" (предметная область кардинально отлична от того что LLM могла видеть на github/stackoverflow в процессе обучения), но прогресс в данном направлении движется быстрее чем успевают выходить новые ролики на RUclips (не говоря уже о многолетнем написании программы вручную)
LLM вроде как только и годится для того, чтобы "генерировать типовой код".
@@alexandertrofimov561 "кожаные мешки", по сути, хорошо годятся для ровно того же
весь трюк в том для кого какой код "типовой"
Это смешно, мне о1 врала о том как запихнуть проект с зависимостями в один jar'ник в определенной версии градла, хотя это не сакральные знания и ответ просто есть в доках.
на Хабре есть тесты нейронок по решению детских задач типа "есть 16 конфеток, как разделить чтобы у Васи было на 2 конфетки больше чем у пети» только gpt4 справляется с 70% таких задач... Не путайте имитацию интеллекта за счёт бигдата с интеллектом... там до доказательства теорем как до луны...
@@Lapyrik Вот именно. Хорошо сформулировано.
то есть сами математики не понимают, что наворотили. какие-то абстрактные теоремы без цифр, какие-то афторитеты от математики, которых никто не проверяет /рукалицо
Со временем все приходит на свои места
Во многих отраслях науки этот кризис есть и там-то как раз намного хуже, и невозможно проверить и никто и никогда системно их не проверяет. Математика счастлива тем, что в ней можно проверять доказательства. Впереди всех конечно находится Computer Science / Informatique, созданные алгоритмы можно запрограммировать и проверить тестами (разные тесты есть не только unit-tests), а также важно, что часто возможна формальная верификация.
@Alpasonic
0 seconds ago
Замечательный ролик. Спасибо. (Только всё же не "Гортензик", а Гротендик (Alehander Grothendieck) И ударение на последнем слоге.
А, ну да
ruclips.net/video/bjlVW1IcLYU/видео.htmlsi=5YjhNNuOrbn8Fw6U
"Каких же умопомрачительных высот может достичь мышление, если с самого начала пойти в неправильном направлении."