← All papers
First page of Beyond Natural Language: An Agent-Native Language for Autonomous Science

Beyond Natural Language: An Agent-Native Language for Autonomous Science

Yifeng He, Jiachen Liu

cs.PL Sep 21, 2026 · v1 cs.AI
Semantic guarantees of the Lara claim-support language and metatheory are mechanized in Lean 4 ( 117,000 lines, sorry-free using standard axioms).
As autonomous AI agents take on every stage of scientific inquiry, research output is expanding far beyond human review capacity. Yet scientific communication still relies on natural-language prose: an informal medium prone to ambiguity, hidden assumptions, and untracked limitations that machines cannot reliably audit. We introduce Lara, a machine-checkable language and protocol for checking and revising support for research claims. By turning research arguments into executable artifacts, Lara provides an epistemic kernel for autonomous science: it enables automated validation pipelines for research agents, lets declared bridges connect arguments across papers into an auditable network, and allows both humans and machines to recheck the standing of an encoded claim in milliseconds. In a Lara program, authors explicitly declare their claims, supporting evidence and assumptions, and known objections or limitations. A lightweight, deterministic checker adjudicates these interactions, assigning each claim a reproducible status: "justified", "defeated", "contested", or "gap", which marks a claim whose support is incomplete and locates the unanswered question. Case studies cover empirical review, a philosophical debate without measurements, and the loss of support when an assumed axiom is withdrawn. We establish the metatheory of claim checking and cross-context argument transport, and mechanize the semantic guarantees in Lean 4 (roughly 117,000 lines), leaving three arguments on paper. The audited public metatheory is "sorry"-free and uses only Lean's three standard axioms; some executable examples additionally trust native evaluation.

Scientific communication relies on natural-language prose, an informal medium prone to ambiguity and unstated assumptions that machines cannot reliably audit. As autonomous AI agents generate research at scale, there is no machine-checkable way to validate and track support for research claims.

The authors introduce Lara, a machine-checkable language and protocol that turns research arguments into executable artifacts with declared claims, evidence, assumptions, and objections. A well-formed Lara program compiles to a Dung argumentation framework whose grounded labelling assigns each claim a status: justified, defeated, contested, or gap. Cross-context bridges allow arguments to transport across papers. The semantic guarantees (decidability, compilation soundness, status preservation, certificate soundness, transport) are mechanized in Lean 4, and a Haskell implementation is validated against the executable Lean semantics.

Thirty-four of thirty-five specification results are mechanized in full across roughly 117,000 lines and 144 Lean files; the audited public metatheory is sorry-free and uses only Lean's three standard axioms (propext, Classical.choice, Quot.sound). Three arguments remain on paper (cost bound, NP-completeness bookkeeping, and closure/indirect-consistency clauses).