[
    {
        "id": "osp-20195",
        "type": "article-journal",
        "title": "Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization",
        "author": [
            {
                "family": "Zhao",
                "given": "Wei"
            },
            {
                "family": "Zou",
                "given": "Yangshuo"
            },
            {
                "family": "Ding",
                "given": "Chengxiang"
            },
            {
                "family": "Wu",
                "given": "Yifan"
            },
            {
                "family": "Wang",
                "given": "Xuchuan"
            },
            {
                "family": "Mao",
                "given": "Zimu"
            },
            {
                "family": "Zhang",
                "given": "Lei"
            },
            {
                "family": "Luo",
                "given": "Tao"
            }
        ],
        "URL": "https://omanscience.com/ar/articles/fyan-a-human-ai-harness-with-semantic-auditing-for-document-level-formalization",
        "language": "en",
        "issued": {
            "date-parts": [
                [
                    2026
                ]
            ]
        },
        "abstract": "We present FYAN, a human--AI harness for document-level mathematical formalization. Rather than treating theorems in isolation, FYAN coordinates an end-to-end workflow spanning specification, proof planning, logical review, Lean proof construction, knowledge curation, and validation, with support for independent supervision and human guidance. A central component is evidence-grounded semantic auditing, which assesses whether formal statements faithfully preserve their informal specifications. A language model constructs structured evidence over local correspondences, omissions, scope, and logical relations, while a deterministic validator checks this evidence and produces reproducible judgments. When a substantive but admissible deviation is accepted, FYAN requires an explicit proof-transfer obligation connecting the formal statement back to a source-facing interpretation. With the same model (DeepSeek-V4.1-Flash) in every stage, FYAN proves 86 of 143 FormalTCS theorems under a strict Lean check, against 69 for a general agent harness, and raises the natural-language proof score from 0.501 to 0.851. On ConsistencyCheck, its semantic audit catches more inconsistent statements than a direct LLM judge, both on labels verified against the source (recall 0.777 vs. 0.636) and on the original labels (0.873 vs. 0.820), and localizes each mismatch it reports to a specific hypothesis, conclusion, or scope. FYAN also built ODENumLib, a 9,355-line Lean library for the numerical analysis of ordinary differential equation."
    }
]