In reply to the question 'What does mathematics study?', it is hardly acceptable to answer 'structures' or 'sets with specified relations'; for among the myriad conceivable structures or sets with specified relations, only a very small discrete subset is of real interest to mathematicians, and the whole point of the question is to understand the special value of this infinitesimal fraction dotted among the amorphous masses. In the same way, the meaning of a mathematical notion is by no means confined to its formal definition; in fact, it may be rather better expressed by a (generally fairly small) sample of the basic examples, which serve
the mathematician as the motivation and the substantive definition, and at the same time as the real meaning of the notion.
- I. R. Shafarevich
We must never forget the call for a radical critique and reform of mathematics in the spirit of Hilbert, Brouwer and the constructivist and finistic schools and most of all Voevodsky's wake-up call to the potential errors of published papers and the necessity of a formal mathematics project based on dependent type theory.
Both the formal rigor and certainty of proof assistants and the clarity of pure computational and combinatorial intuition are called for.
What role does category play here? How can we define and clarify the opposition between good and bad abstraction and construction?
And the philosophically deep question: what part of mathematics is strictly necessary - including for efficiency and reliability - for the most important accomplishments in modern technology, medicine and engineering? What tangible beneficial progress in these domains is the direct result of mathematics?
We need a radical (philosophically, logically and humanistically enlightened) reform of our valuation of mathematical productivity, mathematical theories, mathematical methodologies and practice, mathematical certainty claims and mathematical foundational frameworks.
No comments:
Post a Comment