Lara: A Machine-Checkable Claim Language for Research Agents, With a 117,000-Line Lean 4 Metatheory

arXiv·low signalXBlueskyLinkedInCopy link

He and Liu propose Lara, a language in which authors declare claims, evidence, assumptions and known objections. A deterministic checker labels each claim justified, defeated, contested or gap in milliseconds, and declared bridges link arguments across papers into an auditable network. The semantic guarantees are mechanized in about 117,000 lines of sorry-free Lean 4, with three arguments left on paper. It is an early design aimed at research agents producing more output than humans can review.