3 papers
cs.LO2026
Construction-Verification: A Benchmark for Applied Mathematics in Lean 4
Bowen Yang, Yi Yuan, Chenyi Li +5
Recent advances in large language models have demonstrated impressive capabilities in mathematical formalization. However, existing benchmarks focus on logical verification of decl…
cs.LO2025
Translating Informal Proofs into Formal Proofs Using a Chain of States
Ziyu Wang, Bowen Yang, Chenyi Li +4
We address the problem of translating informal mathematical proofs expressed in natural language into formal proofs in Lean4 under a constrained computational budget. Our approach…
cs.SD2025
Automatic Melody Reduction via Shortest Path Finding
Ziyu Wang, Yuxuan Wu, Roger B. Dannenberg +1
Melody reduction, as an abstract representation of musical compositions, serves not only as a tool for music analysis but also as an intermediate representation for structured musi…