Dear Russell:
1) The UD proof of the object "all theorems" is complex because each step
is a unique slice of progress towards some sub component of the target
object thus all steps are different and there are a great many of them.

##
Advertising

2) The UD knows its proof is complex and since it is the only way it has to
the target object it knows it is elegant.
3) The following are some combinations of a low complexity FAS, different
proof types, and different object types: ["ok" means the combination is
possible, "simple" means low complexity]
a) simple FAS - simple proof, non elegant - simple object -> ok
b) simple FAS - simple proof the FAS can not prove is elegant - simple
object -> ok
c) simple FAS - simple proof the FAS can prove [knows] is elegant - simple
object -> ok
d) simple FAS - complex proof, non elegant - simple object -> ok
e) simple FAS - complex proof - complex object -> ok
The UD follows:
f) simple FAS - complex proof the FAS can prove [knows] is elegant - simple
object -> no good
Hal