[B! math] 宇宙際タイヒミュラー空間についての雑感｜下部　博一
https://b.hatena.ne.jp/entry/s/note.com/complex_manifold/n/ne2d5e726beda

オレンジ的には、『『本人が』』Leanで書き下せないのであれば誤っていると捉えていいと考えるようになった＞＜
膨大になるというのは言い訳にならない＞＜（詰まってる部分だけ本人が書けばいいわけだから＞＜）