From Narrative to Formalism: A Case Study in the Origin of Molecular Translation System

We extend autoformalization into domain of natural sciences by exposing the logical structure of scientific narratives. We outline the Expert-in-the-Loop workflow that extracts axiom-like statements from the prose, uses LLM to generate Lean code enumerating propositions consistent with these axioms, and then identifies and interprets the most promising hypotheses. We demonstrate this approach in the investigation of the origin of translation as the key phase in the origin of life: we formalize an earlier proposed exaptation hypothesis, factorize an implicit signaling hypothesis, and derive a novel "signaling-first" hypothesis of the origin of translation.