11 ноября 2025 г. в 08:47

В хакатоне участвовало 900 команд из 30+ стран. В
финальном туре команды встретились в Абу-Даби чтобы создать проект на базе открытой 32B языковой модели K2 Think за 48 часов. Среди финалистов были команды из Google Deepmind, Cornell University, Harvard Medical School, Hong Kong University of Science and Technology, MBZUAI и др.
Победителями стала казахстанская команда Axiom: Бахыт Момунов, Нурмухамед Зибаткалиев и Александр Шакиев
Используя свой опыт в математических олимпиадах, ребята представили Math Research and Proof ассистента, настроив модель K2 Think для автоматического ИИ-перевода математических доказательств с естественного человеческого языка в формальный вид на машиночитаемом языке Lean. Формализованное доказательство вне зависимости от длины и сложности в результате можно точно проверить на логическую обоснованность и истинность