Today's research into the historical and contemporary use of [proof assistants] and [automated theorem provers] is a sobering reminder of certain idiocies which annoyed me as an undergraduate :
- 1. many professional mathematicians are not practitioners of formal mathematics - this may not be news for many, but it was certainly an irritating discovery for me back in the day ( and it remains irritating to be reminded of this today )
- 2. the entire concept of relying on intuition and a closed community-of-the-intuitively-attuned to uphold norms of any sort, let alone scientific norms, is just ass-backwards and needs to die; or you know, it should be made explicit who is a low-context/explicit mathematician, and who is a high-context/intuitive mathematician, so that others can pick their associations, pedagogical paths, and strategise about any other work appropriately
I am happy with my decision at the time to set all of this aside, and to focus the first part of my career on accumulating other knowledge. Now the time has come for me to do the harder work. Hopefully something will come of it, which I will be happier with, than I am with the state of the world as it is.
No comments :
Post a Comment