Post #2636090

@MartinEscardo@mathstodon.xyz Your main point remains: doing new mathematics with a theorem prover as blackboard is different. I've done that too, I love it, and fully agree that it is both pleasurable and very different than writing either a library or an encyclopedic reconstruction. However, allow me to be pedantic for a moment: pretty much everyone who has formalized category theory, in particular, comes to hate how it is organized in textbooks. I know agda-categories is seriously sub-optimal because it follows the classical organization way too much. Other formalizations are better for having thrown off those shackles! There are similarly lots of papers, indeed from the mathlib people, who report the same: the classical textbooks were not the best source. And, of course, same is true for MathComp in Rocq. @egbertrijke@mathstodon.xyz @gallais@mamot.fr