Mizar系统是一种计算机语言系统,是集逻辑证明、推理演绎、复杂计算、校验排版、科研教学于一体的处理数学信息的形式化系统,并拥有自己的数学知识数据库Mizar Mathematical Library。本文首先介绍数学机械化及Mizar系统的发展历史,其次对如何利用Mizar语言完成数学论文的撰写和进行自动推理校验给出了简要的说明。本文在Mizar系统下讨论了函数偏微分、高阶偏微分理论及相关性质,实现了矢量场、梯度、散度、旋度的Mizar形式,针对不同的数学问题给出了相应的算法和严格的证明,且通过了系统验证。所获结果被收录在Mizar数据库中,并以论文的形式发表在波兰《Formalized Mathematics》杂志上。主要工作如下:1.在Mizar语言下实现了多元函数的微分,借助其微分建立起欧氏空间中二元函数偏微分定义的新形式,讨论了二元函数偏微分的运算性质及可微与连续的关系。2.在Mizar系统下,首次实现了二阶偏微分的Mizar表述,定义的形式简洁明了,并完成了相应的运算公式和定理的Mizar证明与验证。3.将二元函数偏微分的理论推广到三维欧氏空间中,定义了矢量场,由此在Mizar系统下第一次实现了梯度、散度、旋度的定义并将其相关的定理与运算实现了机械化。