alt Hacker NewsIMO mathematics benefits from being highly generic compared to normal code, so much so that the implementation itself doesn't really matter (and it's entirely normal in mathematics to skip details, unlike in software). So then to me it makes sense to have a clean separation between basically header files and implementation files like in C and C++. Then something like mathlib should be a pristine collection of what belongs in headers: data structure definitions, instances, theorem statements, macros/tactics for common techniques, etc. So basically it is a curated set of "axioms" that can be used for other math and remain understandable, indexable, etc. Maybe a companion mathlib-full that can actually compile the entire theory.
I suppose this could be done with just tooling to generate a skeleton/index of a giant repository of all mathematics if you decided that you're going to index all definitions and theorems but not lemmas or examples or something like that.
Replies
Indeed, what I'd like is formal mathematics proving language that could be viewed as an outline in that natural language math proofs are structured as outlines. The reader would be able to choose what to view - definitions, theorems, lemmas, examples, key-steps, all steps etc.
Ideally, a view would let a reader expand into not just the proof at hand but the various theories in the repository.
A reader could even tell their viewing preferences and it might strip down the UI for those purposes.
That makes me imagine a future where various languages import their core data structures and algorithms from a common, language-agnostic "standard library" of mathematically rigorous foundation.