Proof graph

Every credited proof, positioned by its mathlib territory — an SVD of the typeclass machinery it touches, so distance ≈ shared territory. Colour is redundancy class, size is machinery; hover a proof to see its real dependency edges. Drag to pan, scroll to zoom.