2 papers
cs.CL2026
DeepSeek-V4.1-Flash: Pushing the Limits of KV Cache Compression
DeepSeek-AI, :, Anyi Xu +585
The widespread adoption of long-horizon agents has made model workloads increasingly input-heavy. Although prior work has substantially reduced the cost of long-context computation…
cs.AI2026
MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
Hao Shen, Junyu Guo, Tian Cui +2
We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework,…