Post #2636088

2026-05-05 20:40 UTC

@MartinEscardo@mathstodon.xyz Hopefully we'll have occasion to meet in person in a setting where we can discuss all of this at leisure. I think the outcome of such a discussion is likely to be: 1) an "oh, I see" from you, 2) a continued "happy to disagree"! I liken it to (say) the main ocaml and haskell developers meeting to compare notes. They learn a lot from each other but still leave with some core opinions unchanged. [I have personally witnessed this.] And yet each side has truly learned something. @egbertrijke@mathstodon.xyz @gallais@mamot.fr

Replies (1)

@MartinEscardo@mathstodon.xyz 2026-05-05 21:33

@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

Open ##2636089