Lean 4 — это интерактивный помощник по доказательствам, где математика пишется как код, а машина проверяет каждое определение и шаг рассуждения
Учебник Mathematics in Lean учит формализовывать задачи на понятном «языке доказательств»: от элементарной теории чисел до анализа и меры
За спиной — большая библиотека Mathlib и активное сообщество в чате Lean Zulip, так что вы не останетесь одни
Книга задумана как «живой» учебник внутри VS Code
Открываете Lean, печатаете определения и леммы, а в правой панели сразу видите цели и подсказки от системы
Практика — в центре: каждый раздел сопровождается файлом с примерами и упражнениями, их удобно править прямо в редакторе и тут же смотреть реакцию Lean (вплоть до простых экспериментов вроде #eval "Привет, мир!")
Старт простой: ставите Lean 4 и VS Code, клонируете репозиторий mathematics_in_lean, открываете папку MIL и работаете в своей копии, чтобы безболезненно подтягивать обновления
Внутри — аккуратная структура по главам, текстовые подсказки и готовые решения в отдельной папке для самопроверки
Документацию удобно вызывать прямо из редактора через команду «Lean 4: Docs»
Если не хочется настраивать среду локально, всё запускается в облаке через Gitpod: открыли проект — и можно учиться с телефона или любого ноутбука
Учебник ещё развивается, поэтому время от времени стоит обновлять репозиторий — материалы пополняются
https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html
Учебник Mathematics in Lean учит формализовывать задачи на понятном «языке доказательств»: от элементарной теории чисел до анализа и меры
За спиной — большая библиотека Mathlib и активное сообщество в чате Lean Zulip, так что вы не останетесь одни
Книга задумана как «живой» учебник внутри VS Code
Открываете Lean, печатаете определения и леммы, а в правой панели сразу видите цели и подсказки от системы
Практика — в центре: каждый раздел сопровождается файлом с примерами и упражнениями, их удобно править прямо в редакторе и тут же смотреть реакцию Lean (вплоть до простых экспериментов вроде #eval "Привет, мир!")
Старт простой: ставите Lean 4 и VS Code, клонируете репозиторий mathematics_in_lean, открываете папку MIL и работаете в своей копии, чтобы безболезненно подтягивать обновления
Внутри — аккуратная структура по главам, текстовые подсказки и готовые решения в отдельной папке для самопроверки
Документацию удобно вызывать прямо из редактора через команду «Lean 4: Docs»
Если не хочется настраивать среду локально, всё запускается в облаке через Gitpod: открыли проект — и можно учиться с телефона или любого ноутбука
Учебник ещё развивается, поэтому время от времени стоит обновлять репозиторий — материалы пополняются
https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html
Anthropic и OpenAI дают доступ к своим самым последним Ml
Это сильно повлияет на институт государства
Это большой культурный шифт
Государство становится программным обеспечением, которое может работать без людей, которые сегодня находятся внутри и уже не имеют ценности
Это сильно повлияет на институт государства
Это большой культурный шифт
Государство становится программным обеспечением, которое может работать без людей, которые сегодня находятся внутри и уже не имеют ценности
Anthropic
Offering expanded Claude access across all three branches of government
We are removing barriers to government AI adoption by offering Claude for Enterprise and Claude for Government to all three branches of government, including federal civilian executive branch agencies, as well as legislative and judiciary branches of government…
SuperNeuro_A_Fast_and_Scalable_Simulator_for_Neuromorphic_Computing.pdf
448.4 KB
SuperNeuro для больших сетей точечных спайковых нейронов
Сотрудники Ок-Риджской национальной лаборатории (англ. Oak Ridge National Laboratory) [1] Министерства энергетики США разрабатывают собственный композитный симулятор спайковых нейронных сетей SuperNeuro [2] (реально состоящий из двух концептуально различных симуляторов - MAT и ABM), способный быстро работать на нейроморфном "железе" (в частности, на условном FPGA-нейропроцессоре NeuroCoreX [3] их собственной разработки)
Основными конкурентами SuperNeuro, который, по заявлению разработчиков (см. прилагаемую статью), в разы превосходит их по скорости, выступают "европейские" нейросимуляторы NEST and Brian2
[1]: https://www.ornl.gov/
[2]: https://github.com/ORNL/superneuro
[3]: https://github.com/ORNL/NeuroCoreX
Сотрудники Ок-Риджской национальной лаборатории (англ. Oak Ridge National Laboratory) [1] Министерства энергетики США разрабатывают собственный композитный симулятор спайковых нейронных сетей SuperNeuro [2] (реально состоящий из двух концептуально различных симуляторов - MAT и ABM), способный быстро работать на нейроморфном "железе" (в частности, на условном FPGA-нейропроцессоре NeuroCoreX [3] их собственной разработки)
Основными конкурентами SuperNeuro, который, по заявлению разработчиков (см. прилагаемую статью), в разы превосходит их по скорости, выступают "европейские" нейросимуляторы NEST and Brian2
[1]: https://www.ornl.gov/
[2]: https://github.com/ORNL/superneuro
[3]: https://github.com/ORNL/NeuroCoreX
DL-модель TRIBE (Trimodal Brain Encoder) для предсказания fMRI-реакций человеческого мозга на предъявляемые стимулы, причем стимулы могут быть в трёх разных форматах - как текст, аудио или видео
PS: Своеобразная симуляция 3D клеточного (точнее, воксельного) автомата?
Сразу вспомнилась книга "A New Kind of Science" (2002) Стивена Вольфрама
PS: Своеобразная симуляция 3D клеточного (точнее, воксельного) автомата?
Сразу вспомнилась книга "A New Kind of Science" (2002) Стивена Вольфрама
Доклад на AGI-25
В контексте свежих речей Самы про то, что AGI уже плохой концепт
Some people who have been promising the Moon are now saying that the Moon is maybe not the best concept ever
https://www.youtube.com/live/eCUtGU4qKVY?si=rI1Pi51riiuLAP7v&t=25917
(начало тут)
В контексте свежих речей Самы про то, что AGI уже плохой концепт
Some people who have been promising the Moon are now saying that the Moon is maybe not the best concept ever
https://www.youtube.com/live/eCUtGU4qKVY?si=rI1Pi51riiuLAP7v&t=25917
(начало тут)
YouTube
AGI-25 Conference | Day 2 | Keynotes and Paper Presentations
Welcome to Day 2 of the 18th Annual AGI Conference taking place at Reykjavík University, Iceland.
Experience keynotes from leading academics, researchers, and practitioners, and explore pioneering research on the path to AGI, covering AGI frameworks, design…
Experience keynotes from leading academics, researchers, and practitioners, and explore pioneering research on the path to AGI, covering AGI frameworks, design…
Формула Лейбница — взятие производной по параметру определенного интеграла
Очень полезная практически (например, если надо продифференцировать автокорреляционную функцию, заданную на конечном интервале)
К сожалению, далеко не все профильные студенты знают/помнят эту формулу, поэтому рекомендую разобраться с её выводом и выучить наизусть, как правила дифференцирования
Очень полезная практически (например, если надо продифференцировать автокорреляционную функцию, заданную на конечном интервале)
К сожалению, далеко не все профильные студенты знают/помнят эту формулу, поэтому рекомендую разобраться с её выводом и выучить наизусть, как правила дифференцирования
Wikipedia
Формула Лейбница (производной интеграла с параметром)
правило дифференцирования под знаком интеграла