実行を公開します。パネルがバーに到達できなかった場合も含めます。その結果は重要です。Leanカーネルが拒否する形式化は、論理が正当化されなかったステップを正確に示します。
このサイトは純粋数学と応用数学、論理学、理論計算機科学、理論物理学、経済学などの推論的な研究に作られています。実験よりも証明によって解決される主張です。経験的な質問に対しては、正直な判断が定理ではなく発見であるときは、姉妹サイトreferee.chatを使ってください。