なにかのAIに、これとこれのIUT文献見込んで
lean 解析やってくれと やればいいんでないの
あるいは、leanにAIが導入されれば 同じことができる