それぐらい出来てもらえないと困る、とは思うがLean4でおれが院試で要求されている線形代数、複素解析、微分方程式周辺ってMathlib無しで自力で形式化出来るのだろうか