[TYPES] A geometry problem for proof systems

Peter Freyd pjf at saul.cis.upenn.edu
Thu Sep 22 06:53:26 EDT 2005

Yong Lua asks if the following is a theorem:

  A triangle with two internal angle bisectors of equal length is
  an isosceles triangle.

When I was asked this by a fellow high school student (thousands of
years ago) I gave him a long, quite ugly, computational proof (which
did not, alas, satisfy her notion of proof).

I've never seen a proof other than the ugly one.

These days, of course, one just asks Google. The query:

   angle bisector isosceles

leads one to 


It has the ugly proof.


More information about the Types-list mailing list