> Hmmh, I don't really think it is against the spirit of the language. After all, I think you cannot just annotate arbitrary things to be of type integer (or can you?).
Yes, you can: (annotate 'int #\newline). It won't be useful, but yes, you can.
> The above solution would surely work in principle, but in practice I create millions of intermediate theorems, I do not want to store all of them!
Standard answer: Garbage collection
In any case: you can always destructure the annotation wrapper and work with the raw data (probably by using some sort of higher-order function, like combinators), only wrapping it in the annotation type. Sort of like explicit monads.
Garbage collection does not work here if you keep a track of all the defined theorems in a list as 'known*. We would need weak references to achieve this.
