Paper Title
On The Proving Theorems of Euclidean Geometry by Using Isabelle/HOL

Abstract
Isabelle/HOL is a generic proof assistant (software). We try to prove theorems mathematically by using Isabelle/HOL. An effective activity that utilizes programming skill has not succeeded until now in Japan. Isabelle/HOL allows mathematical formulas to be expressed in a formal language and is a software tool for proving those formulas in a logical calculus. We perform a case study/trial of proving theorems of Euclidean geometry by using Isabelle/HOL. We apply the latest tool to an old theme in this trial. The use of the Isabelle/HOL techniques is different from that of paper-and-pencil techniques. The learning of mathematics is often presented as a primarily mental activity that involves the construction of mathematical objects and relations. Using Isabelle/HOL requires insight into the procedures, as well as into the concepts involved. This trial of proving theorems of Euclidean geometry by using Isabelle/HOL can consider mathematical concepts more deeply than before. We explain the process which solves concrete theorems of Euclidean geometry by using Isabelle/HOL in this paper. Keywords - Isabelle/HOL, Theorem Proving, Euclidean Geometry.