Martin Escardo on Nostr: However, it seems to me that, at present, proof assistants don't provide a built-in ...

However, it seems to me that, at present, proof assistants don't provide a built-in way to reconcile the opposing ends (1) and (4) in a useful, practical and theoretical way.

Or maybe they do, but people are not imaginative enough to exploit the already-existing features in proof assistants for that purpose. I don't know.

In any case, at present, in TypeTopology, we adopt the "genetic approach" induced by (4), rather the "historical" approach induced by (1).

This is both good and bad, in my view. It is good because we can concentrate on the level of generality needed at any particular moment of the development. It is bad because we can't benefit from the level of generality of "all currently existing mathematics".

But the suppose we do embrace "all currently existing mathematics" and implement it. Then next there will be something new, perhaps radically new, and our "all currently existing mathematics" will be obsolete.

How can proof assistants and proof-assistant mathematical developments cope with the fact that mathematics is never finished, and yet try maximum generality at each stage?