LEGO is a powerful tool for interactive proof development in the natural deduction style. It supports refinement proof as a basic operation. The system design emphasizes removing the more tedious aspects of interactive proofs. For example, features of the system like argument synthesis and universe polymorphism make proof checking more practical by bringing the level of formalization closer to that of informal mathematics. The higher-order power of its underlying type theories, and the support of specifying new inductive types, provide an expressive language for formalization of mathematical problems and program specification and development.

Particularly, Zhaohui Luo's type theory UTT includes:

- type universes, which make it possible to formalize abstract mathematics;
- strong sum types, which can be used to naturally express abstract structures, mathematical theories and program specifications, and
- a schema for inductive data types, which captures the common inductive structures in programming languages and mathematics.

For further information, go to the Contents page.