惠志成 (Zhicheng Hui)

I am a PhD student at the University of Edinburgh, supervised by Prof. Wenda Li and Prof. Luo Mai. My research focuses on machine learning for theorem proving.

Previously, I was a research intern at Inria Paris, supervised by Prof. François Pottier. Before that, I received my B.Eng. in Information Engineering from Shanghai Jiao Tong University, where I worked with Prof. Qinxiang Cao on developing a natural language proof assistant.

Articles:
  Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language. arXiv preprint, 2026
  Zhicheng Hui, Lihan Xie, Xingzhi Qi, Zhehao Li, Yingjun Lan, Qinxiang Cao

  Investigating Decision Procedures for Fragments of the Iris Separation Logic Framework. Internship report, 2025
  Zhicheng Hui

  Cross-Language Symbolic Runtime Annotation Checking. JFLA 2025
  Zhicheng Hui, Léo Andrès

  A Natural Formalized Proof Language. TASE 2024
  Lihan Xie*, Zhicheng Hui*, Qinxiang Cao
  *equal contributions

  Towards Natural Formal Proof Languages. Bachelor's thesis, 2024
  Zhicheng Hui

Contact:
  Email: Z.Hui-4 [at] sms [dot] ed [dot] ac [dot] uk
  GitHub: https://github.com/ZhichengHui

Last updated: 2026-09-15