Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics

LLM

Xiyu Zhai, Xinyi Chen, Yiping Wang, Runlong Zhou, Liao Zhang, Simon S. Du

Visored is a dependent-type-based prover that transforms math natural language to formal proofs.