на прошлой неделе прикручивал lean в re-rl https://github.com/researchim-ai/re-rl для генережки данных, чтобы можно было генерить пары (состояние, тактика) для каких-нибудь своих обученческих целей (есть начальное состояние и применяя тактики надо дойти до состояния финального что теорема доказана) ну и в целом чтобы можно было работать в теме доказательств теорем и формальной математики если кто не помнит то lean это верификатор доказательств https://github.com/leanprover/lean4 надо выкачать mathlib4 (v4.26.0), извлечь все шаблоны тактик. потюнить берт чтобы по состоянию пытаться подбирать более лучшую тактику которую можно применить (кстати правда помогает), применяем тактики получаем новые состояния и тд чтобы попытаться дойти до финального весь процесс установки с 0 где-то час-полтора займет все нужное есть внутри. В конечном итоге все это собирается чтобы потом подключить в модельки дома https://github.com/researchim-ai/models-at-home и это будет один из envoв для работы с теорем-пруверами. ray тоже добавлен чтобы можно было распараллелить генерацию. Ну и в целом регулируется и количество состояний на теорему и выделяемое время. подход из работы Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs https://arxiv.org/abs/2503.04772 https://www.alphaxiv.org/ru/overview/2503.04772 Авторы кстати работают с LeanDojo, но с более современными версиями mathlib оно не поехало, поэтому без него обошелся и функционал отдельно сделан все проекты делаются в https://t.me/researchim