[cha42]

The largest fancy math object I know is probably the proof of the following theorem:

https://link.springer.com/chapter/10.1007/978-3-030-51074-9_...

The proof is 200Gb large. I am quiet sure now even larger proof exists, in particular thet exhaust some combinatorial property on graphs.