当研究室では数学をコンピュータを使って形式化（コンピュータ言語化） するプロジェクトを行っています。
具体的には、『Mizar（ミザール）』というコンピュータ言語を用いて、 一般には難しい数学の論文の証明をチェックするシステムを作ったり、 既存の数学の証明を形式化（コンピュータ言語化）したりといったことを 行います。
Mizarはプルーフチェッカーのひとつで歴史的にかなり古いものですが 本格的な数学記述用言語としては一番完成度が高いものといえるでしょう。
Mizarでは数学の証明を記述したテキストのことをarticleといいます。 新たにarticleを書くときには、すでにチェックされていてMizarのライブラリ に登録されている多くのarticleを参照することができます。
そして、そのarticleがいずれMizarライブラリに登録されたときには、 それを他のarticleが参照することができます。
以下はMizarの全体構成を大まかに表したものです。
Mizarの研究成果としては、JORDAN曲線定理の完全証明が挙げられます。
JORDAN曲線定理とは左図のように「閉じた曲線が平面を、内と外に分ける」 という直感的には明らかな定理です。
Oswald Veblenが1905年に一応の証明をしたと言われていますが、前提となる 知識の至るところに直感が使われ、完全証明とは言いがたいものでした。
Mizarによるコンピュータを使った証明は、このような人間の直感を排除し、 正確な証明を導き出すことができるのです。
当研究室に来る人はどちらかと言えばソフトウェアが得意（好き）な人、 数学が得意な人の少なくともいずれか一方の人を望みます。
また、数学的なパズルを解くことが好きな人も歓迎します。