大規模な数学モデルが機能する場合(今のところ、機能するようです)、これまで未解決の定理の束が証明される一方で、証明がどのように機能するかを実際に知るためにモデルリーンな証明を読める人間がいない可能性が非常に高いのは奇妙です

とにかくすでにこのように機能しています

@_joshdこれは、サマライザーモデルが元のモデルと型が同一のリーン証明も生成する場合に機能する可能性があります