Post #2172772

2026-05-04 01:51 UTC

@egbertrijke I quite like formalizations that are made to look like encyclopedia pages. I just dislike when they are made to serve double-duty, i.e. serve a narrative purpose as well as a "source code for a library" purpose at the same time. Then you're forced into all sorts of compromises. Libraries need vastly different organization than good narrative does. I don't actually care which one ends up being the primary artifact. [But my current best guess is that it's easier to put a narrative atop a well-organized library than the other way around. I'd be happy to be shown otherwise.] @MartinEscardo @gallais

Replies (1)

@MartinEscardo@mathstodon.xyz 2026-05-04 20:48

@JacquesC2@types.pl writes "I quite like formalizations that are made to look like encyclopedia pages." I am sorry to disappoint you, but this is precisely what I don't like. What I like about mathematics is the narrative, the story that keeps us engaged, and give us intuitions of various sorts. TypeTopology chooses this view. In any case, it **couldn't** choose the encyclopedic point of view, because it is work in progress. You can only get an encyclopedia for work that has already been done. Work in the making requires a different organization, while it is done, and then after it is done and established in the mathematical literature. In TypeToopology we focus in the "while" rather than in the "after", because life is short. But of course sometimes we try to clean up and get things organized. For the purpose we use TypeTopology, namely to be a blackboard for producing ideas, including for publication, the encyclopedic point of view doesn't make any sense at all. @egbertrijke@mathstodon.xyz @gallais@mamot.fr

Open ##2636085