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_4 https://link

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_4 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.