すべての数学の命題や証明は必ず形式化ができるというのは証明されているのでしょうか？
直感というものは、AIの時代にはいかに合理化あるいは否定されるべきなのか。