leandojov2 хочет всегда от пользователя гитхаб аксес токен) так что нам не…

leandojo выкинул. он не работает с новыми версиями lean4 и https://github.com/leanprover-community/mathlib4 тут теоремы и тактики для доказательств пайплайн из…

берта потюнили он используется в процессе доказательств помогает искать более релевантные стратегии

Learning to Repair Lean Proofs from Compiler Feedback https://arxiv.org/abs/2602.02990

для воспроизведения работы пока использую leandojo первый когда по этой работе смогу генерить доказательства то потом leandojov2 буду прикручивать

начало положено