本論文では、Isabelle/HOLを用いて、ディオファントス方程式の複雑性境界に関する形式的な構成と証明を提示しています。ヒルベルトの第十問題に関連し、変数数と次数に制限を加えた方程式クラスの非可決性について、形式検証を通じて実証。多変数多項式の扱いや数論の定理を形式化することで、数学研究と定理証明支援ツールの協調が実現可能であることを示しました。