Post #2599026

@MartinEscardo@mathstodon.xyz Welcome to the joys of a particular flavour of meta-mathematics. From every system (Mizar, Rocq, mathlib, Agda, Isabelle/HOL for sure), I've heard people who have dug into the de facto dependency graph marvel at how unexpected it is. These modern tools ought to be used to teach us how mathematics is actually organized.