Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization

DOI10.48550/ARXIV.2609.39228MaRDI QIDQ7367935arXivFDO

Authors Chengxiang Ding, Yifan Wu, Wei Zhao, Yangshuo Zou, Xuchuan Wang, Zimu Mao, Lei Zhang, Tao Luo

Publication date 30 September 2026

Published in arXiv

Tldr We present FYAN, an end-to-end human--AI harness for document-level formalization with evidence-grounded semantic auditing; it proves more theorems (86/143) and outperforms a direct LLM judge on consistency checks (recall 0.777 vs. 0.636).

Full work available at URL https://doi.org/10.48550/ARXIV.2609.39228

arXiv classification

cs.AI

Cites work

• Liquid tensor experiment
• QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems
• The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

This page was built for publication: Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7367935)