Добрый день!

Я готовлюсь написать свою первую статью на Хабре про Lean 4.
Мне хочется, чтобы она рассказывала интересные темы просто. Lean - довольно сложный язык, и это может легко отпугнуть. А я хочу поднять его популярность как можно сильнее.

Скажите пожалуйста, а как писать просто о сложном?
Я читал книгу "Начала программирования", от Александра Степанова - создателя C++ STL. В первой же главе было выдано множество определений, так что я забывал их через страницу, хотя они сами по себе были не сложные.
Почему так? Обычный такой человеческий человечек удерживает в голове около семи объектов. Плюс минус два. Но если плюс два, то этот человечек уже не очень обычный (хотя всё ещё человеческий). Чтобы он мог жонглировать определениями, их должно быть либо не очень много, либо они должны уже отложиться в буйной головушке.

Я читал книгу достаточно быстро, не пробегал её глазами заранее, не выписывал тезисы. А зря. Это могло бы очень помочь.

Но вот беда... Это всё должен делать чукча читатель! А я то чукча писатель! Как мне решить проблему? Книжка Степанова не плохая!. Насколько я понимаю, ему пришлось пожертвовать лёгкостью чтения для краткости. Такое моё предположение.

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

Ещё очень важное место в этом деле играет язык. Он должен легко ложиться на перегруженный мозг современного читателя. В книге Джесси Шелла "Геймдизайн" язык льётся, и практически не требует расшифровки. Я очень надеюсь, что мне удастся писать так же. Хотя я не расшифровал секрет такого льющегося языка. Хотя некоторые мысли есть.

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

Ещё язык может страдать от плохого перевода с английского. В английском языке предложения строятся по другому. Если переносить структуру предложения абы как, будет некрасиво. Этим часто грешат фанатские переводы сетевой литературы.

Вот такие мои сумбурные мысли. А написал я это для того, чтобы вы мне помогли найти ответ на поставленный вопрос: как писать просто о сложном? Может быть, у вас есть какие-то статьи в припасе?

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

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

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

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

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

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

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

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

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

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

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

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