Post #2636089

@JacquesC2@types.pl If you are formalizing e.g. category theory, where everything is already done and organized in textbooks, then it is much easier to adopt the encyclopedic approach. If you are investigating a new subject, e.g. injective types, you don't know in advance what the better definitions are, what theorems will end up with some parts of their proofs reused somewhere else, and what you are going to discover in this journey. So there is a big difference. Doing new mathematics is trial-and-error and exploration. Formalizing mathematics that somebody else has already organized, post-fact, in textbooks is an entirely different matter, because somebody else did the organization for us. You can only organize something **after** it has been done. Things don't grow in an organized way. It is hopeless, as mathematical practice shows, to try to do this in advance. In the process of doing new mathematics, you always discover, the next day, that something you did yesterday can be generalized, simplified, and refactored. And this goes on day after day. This is what a blackboard looks like. A collection of better and better ideas. An encyclopedia, on the other hand, is the result of this journey + a big reorganization effort. @egbertrijke@mathstodon.xyz @gallais@mamot.fr