activity
20242026
most citedKimi K2: Open Agentic Intelligence

14 citations · 17 across the 9 of their papers we have counts for

collaborators
Showing cs.AIShow all

5 papers · 1 filter

cs.AI2025

LeanGeo: Formalizing Competitional Geometry problems in Lean

Chendong Song, Zihan Wang, Frederick Pu +5

Geometry problems are a crucial testbed for AI reasoning capabilities. Most existing geometry solving systems cannot express problems within a unified framework, thus are difficult…

cs.AI2025

CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

Junqi Liu, Xiaohan Lin, Jonas Bayer +12

Neurosymbolic approaches integrating large language models with formal reasoning have recently achieved human-level performance on mathematics competition problems in algebra, geom…

cs.AI2025★ 1 cited

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning

Haiming Wang, Mert Unsal, Xiaohan Lin +37

We introduce Kimina-Prover Preview, a large language model that pioneers a novel reasoning-driven exploration paradigm for formal theorem proving, as showcased in this preview rele…

cs.AI2024

FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving

Xiaohan Lin, Qingxing Cao, Yinya Huang +5

Formal verification (FV) has witnessed growing significance with current emerging program synthesis by the evolving large language models (LLMs). However, current formal verificati…

cs.AI2024

MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data

Yinya Huang, Xiaohan Lin, Zhengying Liu +6

Recent large language models (LLMs) have witnessed significant advancement in various tasks, including mathematical reasoning and theorem proving. As these two tasks require strict…