Не думаю, что их результат признает сообщество математиков, но зато это супер-реклама. Правда если найдут явную лажу то будет не очень, но в таком длинном тексте быстро не найдут. А когда найдут через год, хайп пройдет и всем будет пофиг.
Проблема любых неконструктивных доказательств - верификация. Если легко проверить то ОК, но тогда и доказательство должно быть простым и коротким - помещаться в памяти или проверяться простой, проверенной тестами программой. Но разве можно легко проверить что-то на 100 страницах и быть уверенным, что там нет ошибки?
Означает, что модель не годится в некоторых условиях. Что впрочем итак очевидно, поскольку эта модель не учитывает величину давления жидкости, а только его градиент. Там может быть отрицательное давление в этой модели, и теоретически ничего - нормально. А на практике при пониженном давлении в жидкости будут пузыри и модель сплошной среды уже неприменима.
Формула: ускорение капли в потоке равно градиенту давления + сила вязкого трения + внешняя сила дальнодействия (тяжести или эктромагнитная, если заряжена жидкость). Доказали, что при какой то особой силе, которой наверно не бывает в природе, не бывает решения уравнений, но это тоже очень важно для математики.
Насколько я понял доказано, что есть условия, когда нет гладкого решения уравнений НС - типа доказали, это круто. Есть кстати доказательство существования обобщенного решения уравнения НС - модная тема математики 20 века, но не доказана единственность обобщенного решения. Были лекции профессора Вишика на мехмате МГУ в 1990-х. Проблема гладкого решения интересна, но отрицательный результат (нет гладкого решения) скорее разочаровывает. Это как-бы дискредитирует модель. Но в плане математики это круто.
Не понятно что доказали: существование гладкого решения уравнений Навье-Стокса, или вывели контрпример, когда не существует гладкого решения при гладких начальных условиях - сразу разрыв? Я что-то не верю в доказательство от ИИ, там какая-то ахинея наверное. И сейчас, к сожалению, даже большинство работ нормальных математиков плохо проверяемо, слишком сложно всё. Тем более вряд ли возможно проверить творчество ИИ. А во всех сложных логических построениях зачастую бывают неочевидные ошибки. Что до результата, то он скорее интересен только специалистам-математикам. Модель уравнений Навье-Стокса несжимаемой вязкой жидкости не предполагает роль давления как физической величины, что для реальной гидродинамики не всегда годится. Кто запускал насосы знают про кавитацию и что надо давление, чтобы насосы работали. А модель учитывает только градиент давления.
Самостоятельная установка корневых и любых сертификатов - это дырка в безопасности. Я установил и надеюсь, что они те, что надо. Корневые - потому, что корпоративный мессенджер требовал. Отдельные - чтобы не устанавливать корневой в браузере.
Эти сертификаты только для браузеров разве нужны? Разве не все безопасные подключения используют и проверяют TLS/SSL сертификаты. Корневые сертификаты прописаны во всех системах, которые подключаются к другим серверам, или нет так? Надо по идее во всех таких системах добавлять корневой сертификат Минцифры, чтобы они не отвергали подключение. Или путаю что-то?
Тогда, в 90-е, у IT были маленькие зарплаты. Никто наверно не поверит сейчас, что такие были зарплаты. IT было очень непривлекательно в смысле денег. В 2010-ые годы у IT-шников стали расти оклады сильнее, а сейчас наверно будет наоборот - выравнивание.
Интересно, есть ли клавиатуры с двумя рядами букв: кириллица и латиница. У меня очень много времени уходит на alt shift - переключение. Купил бы такую. Для русских большой минус в конкуренции - использовать два алфавита.
Наверное проблема таких кодеков в том, что точно выделить спектр не получается. Звук ведь не периодическая функция по времени, а преобразование Фурье применимо для периодических функций. Кроме ряд Фурье хорошо приближает гладкие функции (гласные звуки, скрипка, флейта), а для разрывных функций (согласные звуки, барабаны) приближение будет плохое и не поможет при сжатии. Я сам занимался сжатием звука и у меня получился хороший кодек, который сжимает в 4 раза и звучит как исходник (хотя, может быть, это только кажется - нет ведь способов объективно сравнивать звучание, но если сжимать в 8 раз, то уже слышно снижение качества музыки). Сжатие не использует БПФ и основано на относительной амплитуде звука, тогда как PCM кодирует абсолютную амплитуду. Наверное есть ещё такие кодеки, вряд ли до этого никто раньше не додумался.
А как проверить, что в Lean перенесено корректно? Никак.
Не думаю, что их результат признает сообщество математиков, но зато это супер-реклама. Правда если найдут явную лажу то будет не очень, но в таком длинном тексте быстро не найдут. А когда найдут через год, хайп пройдет и всем будет пофиг.
Проблема любых неконструктивных доказательств - верификация. Если легко проверить то ОК, но тогда и доказательство должно быть простым и коротким - помещаться в памяти или проверяться простой, проверенной тестами программой. Но разве можно легко проверить что-то на 100 страницах и быть уверенным, что там нет ошибки?
Плюс ещё - несжимаемость - дивергенция поля скоростей равна нулю.
Означает, что модель не годится в некоторых условиях. Что впрочем итак очевидно, поскольку эта модель не учитывает величину давления жидкости, а только его градиент. Там может быть отрицательное давление в этой модели, и теоретически ничего - нормально. А на практике при пониженном давлении в жидкости будут пузыри и модель сплошной среды уже неприменима.
Это основные уравнения гидродинамики вязкой несжимаемой жидкости. В Википедии есть нормальная статья Уравнения Навье — Стокса — Википедия .
Формула: ускорение капли в потоке равно градиенту давления + сила вязкого трения + внешняя сила дальнодействия (тяжести или эктромагнитная, если заряжена жидкость). Доказали, что при какой то особой силе, которой наверно не бывает в природе, не бывает решения уравнений, но это тоже очень важно для математики.
Насколько я понял доказано, что есть условия, когда нет гладкого решения уравнений НС - типа доказали, это круто. Есть кстати доказательство существования обобщенного решения уравнения НС - модная тема математики 20 века, но не доказана единственность обобщенного решения. Были лекции профессора Вишика на мехмате МГУ в 1990-х. Проблема гладкого решения интересна, но отрицательный результат (нет гладкого решения) скорее разочаровывает. Это как-бы дискредитирует модель. Но в плане математики это круто.
Не понятно что доказали: существование гладкого решения уравнений Навье-Стокса, или вывели контрпример, когда не существует гладкого решения при гладких начальных условиях - сразу разрыв? Я что-то не верю в доказательство от ИИ, там какая-то ахинея наверное. И сейчас, к сожалению, даже большинство работ нормальных математиков плохо проверяемо, слишком сложно всё. Тем более вряд ли возможно проверить творчество ИИ. А во всех сложных логических построениях зачастую бывают неочевидные ошибки. Что до результата, то он скорее интересен только специалистам-математикам. Модель уравнений Навье-Стокса несжимаемой вязкой жидкости не предполагает роль давления как физической величины, что для реальной гидродинамики не всегда годится. Кто запускал насосы знают про кавитацию и что надо давление, чтобы насосы работали. А модель учитывает только градиент давления.
Нелинейные уравнения в частных производных.
Самостоятельная установка корневых и любых сертификатов - это дырка в безопасности. Я установил и надеюсь, что они те, что надо. Корневые - потому, что корпоративный мессенджер требовал. Отдельные - чтобы не устанавливать корневой в браузере.
Эти сертификаты только для браузеров разве нужны? Разве не все безопасные подключения используют и проверяют TLS/SSL сертификаты. Корневые сертификаты прописаны во всех системах, которые подключаются к другим серверам, или нет так? Надо по идее во всех таких системах добавлять корневой сертификат Минцифры, чтобы они не отвергали подключение. Или путаю что-то?
Госуслуги тоже используют сертификат от GlobalSign. Не будут работать теперь?
Тогда, в 90-е, у IT были маленькие зарплаты. Никто наверно не поверит сейчас, что такие были зарплаты. IT было очень непривлекательно в смысле денег. В 2010-ые годы у IT-шников стали расти оклады сильнее, а сейчас наверно будет наоборот - выравнивание.
никто не скажет: "мы вас ничему не учим, сами ничего не знаем"
Интересно, есть ли клавиатуры с двумя рядами букв: кириллица и латиница. У меня очень много времени уходит на alt shift - переключение. Купил бы такую. Для русских большой минус в конкуренции - использовать два алфавита.
Наверное проблема таких кодеков в том, что точно выделить спектр не получается. Звук ведь не периодическая функция по времени, а преобразование Фурье применимо для периодических функций. Кроме ряд Фурье хорошо приближает гладкие функции (гласные звуки, скрипка, флейта), а для разрывных функций (согласные звуки, барабаны) приближение будет плохое и не поможет при сжатии. Я сам занимался сжатием звука и у меня получился хороший кодек, который сжимает в 4 раза и звучит как исходник (хотя, может быть, это только кажется - нет ведь способов объективно сравнивать звучание, но если сжимать в 8 раз, то уже слышно снижение качества музыки). Сжатие не использует БПФ и основано на относительной амплитуде звука, тогда как PCM кодирует абсолютную амплитуду. Наверное есть ещё такие кодеки, вряд ли до этого никто раньше не додумался.
Интересно, как устроено сжатие звука PAC? В MP3 используется преобразование Фурье и сжатие преобразованного массива. В PAC другой принцип сжатия?