My main research interests are Compiler Optimization, Document Language, Computer Algebra System, and Machine-Asisted Theorem Proving. I once worked as a visiting scholar at the Beijing International Center for Mathematical Research at Peking University for one year, during which I researched how to adjust the Lean 4 compiler to facilitate better generation of mathematical proofs by Large Language Models.
I am also deeply interested in literary and artistic works with a strong personal style, such as the films of 周星驰, the music composed by 菅野よう子, 梶浦由記, et 神前暁, und the novels of 鲁迅, 芥川龍之介, and 虚渊玄. Because the number one spot always remains an unknown, my second favorite anime of all time is KILL la KILL, and my second favorite instrumental piece is the Kyogen track 狂言「九十九星降」. I also do graphic design from time to time, creating logos for my own projects as well as those of my friends.
LLMs cannot fundamentally evolve into AGI, even if LLMs currently represent the closest approach humanity has achieved. Therefore, MATP does not inherently imply using LLMs as the machine learning method for interactive theorem proving. Concurrently, the existence of Proof Assistants makes verifying the actual reliability of a proof highly feasible. For this reason, I also believe that MATP will serve as a crucial testing ground on the path toward AGI.
I have been a GitHub user for over 10 years. However, given GitHub's shameless introduction and promotion of LLM services for code review and PR, combined with major incidents affecting its core Git hosting functionality (such as lost commits), I will be moving all of my projects to Codeberg and Tangled in the future.