We demonstrate computer-assisted proofs of "Kariya's theorem," a theorem in elementary geometry, with computer algebra. In the proof of geometry theorem with computer algebra, vertices of geometric figures that are subjects for the proof are expressed as variables. The variables are classified into two classes: arbitrarily given points and the points defined from the former points by constraints. We show proofs of Kariya's theorem with two formulations according to two ways for giving the arbitrary points: one is called "vertex formulation," and the other is called "incenter formulation," with two methods: one is Gr\"obner basis computation, and the other is Wu's method. Furthermore, we show computer-assisted proofs of the property that the point so-called "Kariya point" is located on the hyperbola so-called "Feuerbach's hyperbola", with two formulations and two methods.

翻译：我们利用计算机代数，针对初等几何中的“Kariya定理”给出了计算机辅助证明。在几何定理的计算机代数证明中，作为证明对象的几何图形顶点被表示为变量。这些变量分为两类：任意给定的点，以及由前者通过约束条件确定的点。我们展示了Kariya定理的两种表述——一种称为“顶点表述”，另一种称为“内心表述”——分别采用Gröbner基计算和吴方法两种方法进行证明。进一步地，我们针对“Kariya点”位于所谓“Feuerbach双曲线”上的性质，同样通过两种表述和两种方法进行了计算机辅助证明。