Доказал на Lean 4 несколько теорем про факториал и алгоритм Евклида.

Это было довольно забавно! Правда, на индукции я немного забуксовал. Нужно разобраться с этим подробнее. Советую попробовать вам самим доказать какие-нибудь теоремы.

Для обучения Lean есть несколько игр. Там постепенно вводятся тактики, хотя мне больше пользы принесло доказательство теорем в обычном редакторе с подсказками от ИИ. Он правда иногда ошибается, но Lean подсветит ошибки.

Есть учебники по Lean, а попробовать его можно в песочнице.

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

Особенно интересно может быть написать какую-нибудь программу (это ведь язык программирования!) и доказать некоторые её свойства (это же помощник для доказательств!)

Буду рад, если кто-нибудь присоединится ко мне в изучении этого языка!

Господа, добрый день! Я собираюсь выпустить статью о языке программирования Lean.
Он сочетает в себе два назначения: это одновременно и язык программирования, и средство доказательства теорем. И они помогают друг другу. На языке программирования Lean можно писать тактики, которые помогают упростить доказательства, а при помощи средств доказательства можно гарантировать, что наша программа корректна!

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

Скажите, о чём бы вы хотели прочитать в моей будущей статье? Какие аспекты вам наиболее интересны? Решение какого-нибудь примера? Или просто обзор языка и его экосистемы? Может быть, рассказ о том, как для написания доказательств используют искусственный интеллект?

Предлагайте свои варианты и задавайте вопросы.

Приветствую!
У меня есть мечта - создать свой собственный анимационный сериал.
Но анимация - это очень дорого. От 500 000, до 1 500 000 рублей за минуту.
И вот вопрос: может быть, делу могут помочь нейронные сети?
Буду очень рад услышать о вашем опыте в комментариях!
Получалось ли у вас создать в генераторе не просто ролик, а консистентное произведение в едином стиле?
Или современные сети пока ещё не готовы для такого?