cat ~/about/README.md
Research Intern @ Microsoft Research Asia
I study AI for Mathematics — exploring how large language models can assist and automate formal mathematical reasoning and theorem proving.
Czech Technical University in Prague · 2023 — 2025
University of Science and Technology Beijing (USTB) · 2018 — 2022
Sep 2025 — Present · AI for Formal Mathematics, Theorem Proving
2021 — 2022
Swarma Club · October 2023 · Link →
Swarma Club · March 2025 · Link →
ls ~/research/
Leveraging large language models to assist mathematicians in formalizing and verifying proofs in systems like Lean 4. Bridging the gap between informal mathematical reasoning and machine-verifiable proofs.
Developing neural approaches to automate the search for mathematical proofs. Combining deep learning with symbolic reasoning to tackle open problems in automated deduction.
Translating informal mathematical text (papers, textbooks) into formal specifications automatically. A key step toward machine-readable mathematics at scale.
Applying neural networks to Boolean satisfiability problems, exploring architecture choices, training paradigms, and interpretability of learned solving strategies.
cat ~/publications/list.bib
April 2025
A comprehensive study examining how neural network architectures can be applied to Boolean satisfiability (SAT) problems. We analyze key design decisions — including graph representations, message-passing mechanisms, and training strategies — and provide interpretability insights into what these networks learn about SAT structure.
2025 · AITP 2025
We leverage large language models to summarize theorem library files into auxiliary prompts for the autoformalization task. Under a pass@5 budget, our approach achieves 100% syntactic accuracy on the MiniF2F-test. The main advantage is enabling low-cost and timely adaptation to the latest theorem libraries, a capability difficult to achieve with traditional fine-tuning-based methods.
More publications coming soon...
// TODO: keep publishing
ls ~/projects/
Major contributor to Chinese translations of core Lean 4 community tutorials: Theorem Proving in Lean 4, Mathematics in Lean 4, and Metaprogramming in Lean 4. Making formal mathematics accessible to Chinese-speaking developers and mathematicians.
1700+ followers on Zhihu. Authored the earliest Chinese-language introduction to AI for Formal Theorem Proving (2023). Writing monthly research paper roundups and technical deep-dives on AI for mathematics.
Contributor to FormalBook — a community project formalizing proofs from Aigner & Ziegler's "Proofs from THE BOOK" in Lean 4. Turning elegant mathematical proofs into machine-verified formal statements.
ls ~/blog/ -lt
📝 New posts coming soon...
Stay tuned for research notes and technical deep-dives on AI for Mathematics.