Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
2026-06-16Code Available0· sign in to hype
Xiyu Zhai, Xinyi Chen, Yiping Wang, Runlong Zhou, Liao Zhang, Simon S. Du
Code Available — Be the first to reproduce this paper.
ReproduceCode
- github.com/xiyuzhai-husky-lang/visoredOfficialIn paper★ 0
Abstract
We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design choices are a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file. Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark. Lean output excerpts: https://github.com/xiyuzhai-husky-lang/visored/