じゃあそのaiで作ったLeanの定式化コード公開したらいい