We don't think that people using math libraries should all have to accept a
common logic, or even choose between a few.
We don't think they should have to depend on a monolithic software system.
We think that Knowledge Management is a fundamental service that a
math library should provide, specifically,
A Math Library should help each User determine which things in the library
represent Knowledge as opposed to mere Information.
(elaboration)
We think math libraries should be Theoretically Neutral.
Designers should refrain from imposing an orthodoxy on all as to
what constitutes knowledge, even accepting purported proofs whose
correctness may be disputable by different parties (due, for example,
to doubts about logic designs or system implementations).
Elaboration:
Providing Knowledge Management in a Theoretically Neutral repository
requires careful accounting for various, possibly contradictory,
criteria for what counts as knowledge represented in the repository.