摘要：在Mizar语言下实现了多元函数的微分。借助其微分建立起欧氏空间中二元函数偏微分定义的新形式，讨论了二元函数偏微分的运算性质及可微。在Mizar系统下，首次实现了二阶偏微分的Mizar表述，定义的形式简洁明了，并完成了相应的运算公式和定理。

关键词：数学机械化 mizar语言系统 形式化数学 

单位：福建船政交通职业学院基础教研室 福建福州350007