Mechanized reasoning in mathematics - Kuen-Bang Hou (Favonia)