张毅，博士，副教授，硕士生导师，美国数学评论评论员，德国数学文摘评论员。主要从事代数表示论，Rota-Baxter代数与Hopf代数的研究，在Adv. Theor. Math. Phys.，Science China Math.，J. Algebra，JPAA，Pacific J. Math., J. Algebraic Combin.等国内外三高期刊发表SCI论文20余篇。现主持完成国家自然基金青年基金、科技部“一带一路”创新人才交流外国专家项目各1项。研究成果被美国数学物理学家，加州理工学院Marcolli教授，以及语言学家，美国国家科学院Chomsky院士应用到生成语言学中的Minimalist纲领。

Lean是由微软研究院开发的现代化形式化证明系统，结合依类型理论与高效函数式编程，广泛应用于数学定理验证与可验证软件开发。它正受到国际顶尖学者关注，包括陶哲轩，他在多次公开发言中倡导数学的“形式化未来”。Kevin Buzzard则致力于推动Lean在纯数学中的应用，并提出在Lean中重构费马大定理的设想。随着 mathlib 等大型数学库的快速发展，Lean正成为连接人工智能、形式验证与前沿数学研究的重要平台，代表着未来数学的新范式。目前本课题组与帝国理工学院研究生合作，正在推进代数结构的形式化工作。

欢迎对代数，组合，Lean领域感兴趣的同学报考我的研究生。

联系方式：zhangy2016@nuist.edu.cn

ResearchGate:

https://www.researchgate.net/profile/Yi-Zhang-6

Google Scholar

https://scholar.google.com/citations?user=9QRBIUIAAAAJ&hl=zh-CN&oi=sra