目前，随着计算机技术的发展，机器证明已经成为一个非常活跃的研究领域。人们根据机械化方法成功创建了各种机器语言来编写程序，并在计算机上实现了数学问题的机器证明。欧洲最常用的机器证明系统是Mizar语言系统，该系统参与研究者之多，使用者在世界上区域分布之广，数据库之大是其它语言系统不能比拟的。　　 本文介绍了机器证明及Mizar系统的历史和研究现状，对利用Mizar语言完成数学论文和进行自动推理检验做了简要说明。作者给出了线性空间中泛函在Mizar系统下的若干定义及性质；实现了线性空间中对偶空间的定义及性质。主要工作如下：　　 1.实现了线性空间中泛函在Mizar系统下的加法、减法、数乘等定义，证明了泛函运算的基本性质定理；　　 2.定义了线性空间和向量空间之间的模式转换，利用模式转换和向量空间对偶空间的定义实现了线性空间对偶空间的定义，并以定理的形式证明了对偶空间中元素满足的条件，讨论了对偶空间的若干性质。　　 以上结果均通过了Mizar系统的验证，并在系统中给出了相应的算法和严格的证明。