[七重天]

你指的是吴文俊院士，他研究的是几何的计算机自动化证明问题，而符号计算涉及解决代数问题，譬如：前面有图片，介绍的就是三角函数的化简、分解因式，以及微分和不定积分解原函数等。