search

google-deepmind / alphageometry

Apache License 2.0
4.19k stars 470 forks source link

Have you ever questioned about the same definition of incenter and excenter in def.txt? #95

Open ppaaron opened 8 months ago

ppaaron commented 8 months ago

Have you ever questioned about the same definition of incenter and excenter in def.txt? Was it right or you give a wrong definition?

In line 73: incenter x a b c x : a b c a b c = ncoll a b c x : eqangle a b a x a x a c, eqangle c a c x c x c b; eqangle b c b x b x b a bisect a b c, bisect b c a

incenter2 x y z i a b c i : a b c, x : i b c, y : i c a, z : i a b a b c = ncoll a b c i : eqangle a b a i a i a c, eqangle c a c i c i c b; eqangle b c b i b i b a; x : coll x b c, perp i x b c; y : coll y c a, perp i y c a; z : coll z a b, perp i z a b; cong i x i y, cong i y i z incenter2 a b c

excenter x a b c x : a b c a b c = ncoll a b c x : eqangle a b a x a x a c, eqangle c a c x c x c b; eqangle b c b x b x b a bisect b a c, exbisect b c a

excenter2 x y z i a b c i : a b c, x : i b c, y : i c a, z : i a b a b c = ncoll a b c i : eqangle a b a i a i a c, eqangle c a c i c i c b; eqangle b c b i b i b a; x : coll x b c, perp i x b c; y : coll y c a, perp i y c a; z : coll z a b, perp i z a b; cong i x i y, cong i y i z excenter2 a b c