awakening-goedel-v2-32b-sft — дообученная модель на базе Qwen3-32B, опубликованная juihuichung как исходный чекпойнт исследования восстановления агентных возможностей. Модель обучена на примерно 860 тысячах примеров доказательств на Lean 4 и предназначена прежде всего для формального доказательства теорем и работы с математическими задачами в Lean 4.

Это плотная причинная языковая модель с 29,7 млрд параметров, использующая архитектуру Qwen3 и формат safetensors. Метаданные указывают контекст до 40 960 токенов; модель принимает и генерирует текст. Лицензия — Apache-2.0.

README сообщает о сильных способностях в доказательствах Lean 4, но также о коллапсе вызова инструментов после дообучения: в приведённой оценке BFCL Non-Live результат составил 4,6, а Multi-Turn — 0,0; модель почти всегда отклоняет вызовы функций. Поэтому её следует выбирать для формального доказательства, а не для агентных сценариев с инструментами.