Reproduce “KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Zihua She, Xiao Wang
KAPPA checks statistical papers by translating each result and its proof into Lean, then reviewing the formal statement and checking the proof step by step along the paper’s route. In a comparison on the longest of three selected papers, it classified all 12 results correctly, versus 9 for a direct agent and 10 for a chat. The selected cases do not establish general error rates.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.