Hausdorff formalization brief

This is the current v2.5 example PDF. It uses native minted Lean blocks and separate LeanTeX output blocks.

More examples forthcoming

Older example PDFs are still in the repository history, but the public examples page now points to the v2.5 native minted style.