① AIによる証明文(自然言語使って人間に読めるような)
② その証明をAIがLEANコードに変換したもの

①を理解しようと試みる → これが数学者の仕事。テレンスタオいわく数学者が説明できないAIの論文は発表するべきではないと

②のLEANコードと証明文で齟齬がないかチェック → これは①を完全に理解してなくてもある程度機械的にやれるかな？