✅ yandex_music_to_nuclear — python-скрипт для экспорта плейлистов Яндекс.Музыки в формат, удобный для других музыкальных плееров

📱 Python 3.x

📌 Скрипт позволяет экспортировать свои плейлисты из Яндекс.Музыки в JSON и CSV, которые затем можно импортировать в сторонние плееры (например, Nuclear Player). Работает с токеном Яндекс.Музыки, чтобы получить доступ ко всем плейлистам, включая приватные. Поддерживает работу по списку ссылок или через HTML-файлы плейлистов — удобно, если нет токена.

📌 Фичи:

🟢 Можно быстро получить плейлисты из закрытой музыкальной платформы и использовать их в другом приложении.
🟢 Можно хранить свои треки в формате CSV/JSON для анализа или бэкапа.
🟢 Отличный пример полезного сценария автоматизации, работающего с сетевыми API.

🔗 Репозиторий GitHub

#скрипты

🖥 Python_Scripts

🖥 Goedel-Prover — нейросеть, придвигающая формальные доказательства к автоматике

📌 Goedel-Prover — это открытая LLM-модель, предназначенная для автоматического вывода полных формальных доказательств в среде Lean 4. Благодаря сочетанию обучения формализации задач и итеративного режима обучения, она достигает выдающихся результатов на математических бенчмарках.

📌 Модель работает по схеме «statement formalizer + prover iterations». Сначала естественноязыковые математические задачи переводятся в формальный язык Lean 4, затем серия проверов дообучаются друг на друга — каждый следующий решает те те задачи, которые не удалось предыдущему. На benchmark miniF2F Goedel-Prover достигает 57.6% Pass@32, опережая предыдущие модели (DeepSeek-Prover-V1.5) на ~7.6%.

ℹ️ Интересный поворот — в августе 2025 вышла версия Goedel-Prover-V2, с новыми методами: scaffolded data synthesis, verifier-guided self-correction, объединение чекпоинтов (model averaging). В ней используются стратегии самокоррекции: модель сначала генерирует кандидата, затем проверяет его через компилятор Lean и вносит правки. В публичном доступе есть модель Goedel-Prover-V2-32B на Hugging Face.

🔗 Попробовать: Goedel-Prover