Kazakhstan's Axiom team wins the K2 Think Hackathon

The hackathon attracted 900 teams from more than 30 countries. Finalists met in Abu Dhabi to build a project with the open 32B K2 Think language model in 48 hours. Teams included participants from Google DeepMind, Cornell University, Harvard Medical School, Hong Kong University of Science and Technology, MBZUAI, and others.

Kazakhstan's Axiom team won: Bakhyt Momunov, Nurmukhamed Zibatkaliyev, and Alexander Shakiyev.

Drawing on their mathematical-olympiad experience, the team built a Math Research and Proof assistant. They adapted K2 Think to automatically translate mathematical proofs from natural human language into formal, machine-readable Lean. Regardless of length or complexity, the formalized proof can then be checked precisely for logical validity and correctness.