Four Miracles In a Triangle

Oliver Knill, MathE - 320, Harvard Extension School,  2010-2017

These are all computer assisted proofs. The side bisectors intersect in the centroid, the altitudes intersect in in the orthocenter, the side bisectors intersect in the circumcenter, the angle bisectors intersect in the incenter. It is Rene Descartes point of view to translate the statements into pure algebra. The computer algebra system can then verify the statement in full generality, not only in special cases. Of course, it does not suffice that you just run the four proofs. Part of the proof verification is to read the code and understand what it does. This computer assisted proof was written in 2010. For the latest incarnation of the course MathE320, see the website http://www.math.harvard.edu/~knill/teaching/mathe320_2017

Centroid

a={aa,a2};b={b1,b2};c={c1,c2};u=(b+c)/2;v=(a+c)/2;w=(a+b)/2;
p=(a+b+c)/3;Simplify[p==a/3+2u/3==b/3+2v/3==c/3+2w/3]

Orthocenter

a={a1,a2};b={b1,b2};c={c1,c2};
f[{a_,b_,c_}]:=a+(b-a)*((c-a).(b-a))/((b-a).(b-a));
m=f[{b,c,a}];n=f[{c,a,b}];p=f[{a,b,c}];
L[x_,y_,z_,w_]:=x+(t/.Solve[x+t (y-x)==z+s (w-z),{t,s}][[1]])(y-x);
Simplify[L[a,m,b,n]==L[a,m,c,p]==L[b,n,c,p]]

Circumcenter

a={a1,a2};b={b1,b2};c={c1,c2};u1=(b+c)/2;v1=(a+c)/2;w1=(a+b)/2;
q[x_]:={-x[[2]],x[[1]]};u2=u1+q[c-b];v2=v1+q[c-a];w2=w1+q[a-b];
L[x_,y_,z_,w_]:=x+(t/.Solve[x+t (y-x)==z+s (w-z),{t,s}][[1]])(y-x);
Simplify[L[u1,u2,v1,v2]==L[u1,u2,w1,w2]==L[v1,v2,w1,w2]]

Incenter

a={a1,a2};b={b1,b2};c={c1,c2};
f[a_,b_,c_]:=a+((b-a)/Sqrt[(b-a).(b-a)]+(c-a)/Sqrt[(c-a).(c-a)])/2
u=f[a,b,c];v=f[b,c,a];w=f[c,a,b];
L[x_,y_,z_,w_]:=x+(t/.Solve[x+t (y-x)==z+s (w-z),{t,s}][[1]])(y-x);
Simplify[L[a,u,b,v]==L[a,u,c,w]==L[b,v,c,w]]