Deep0Thinking
Academic

Yiyang Liu

Mathematics and logic at Carnegie Mellon University.

I go by Louis and publish as Yiyang Liu.

Research interests

Proof theory, formalized mathematics, and automated theorem proving.

I study mathematics, with a focus on discrete mathematics and logic, at Carnegie Mellon University. I am interested in the structure of proofs and in using proof assistants to make mathematical arguments precise. I write proofs in Lean.

Publications & preprints

PreprintarXiv:2610.27046

ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems

Zeyu Zheng, Yiyang Liu, Yuyang Zhao, et al.

All 23 authors

Zeyu Zheng, Yiyang Liu, Yuyang Zhao, Congmin Zheng, Jiachen Zhu, Jianian Chen, Kangning Zhang, Kayue Daniel Wong, Lingyu Yang, Rong Shan, Shihao Chen, Thomas Zhu, Wentao Zhang, Xiaopeng Li, Yan Hu, Yongxi Lin, Yuxiang Chen, Zhuoying Ou, Jianghao Lin, Jeremy Avigad, Prasad Tetali, Jingbang Chen, Sean Welleck.

A benchmark of 244 open problems from undergraduate research, formalized in Lean 4, for evaluating coding agents on proving statements or their negations.

Current work

Axiomatization of Classical Mechanics

I am working on an axiomatization of classical mechanics.

I also write about mathematics and logic in my notes and longer series.