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

...Но есть две мааалюсенькие проблемки :)

1. В создании соответствующих задачек, конкретно под темку software design, никакой AI, к сожалению не поможет. Практика показала, что он в основном больше вредит :) Проблема чисто техническая, просто потребуется вложить существенно больше времени (увы).

2. Платформа (Lean4) тоже имеет определённое значение. В частности большой вопрос, какие теории типов поддерживает прувер. Lean4 например не способен в HoTT из-за своего кривого ядра вывода. Ну и экосистема имеет значение: похоже, Лин взял всё самое худшее из экосистемы Хаскеля :) Попробуйте например собрать Mathlib в винде.

Поэтому сами задачки мне придётся сперва делать в некоторой мета-теории, без привязки к конкретным теорем-пруверам или языкам с зависимыми типами, чтобы их (как "реализацию" без изменения интерфейсов) можно было безболезненно заменять в случае чего. Можно теоркат (симплициальные ∞-категории), можно кубическую теорию типов, благо я сделал её "реализацию"...

Насколько это всё сложно в плане понимания? Ну, смотрю разные математические семинары, это например третий курс мехмата НГУ.