約3週間前、プロの数学者とアマチュアの数学者、自動定理証明ツール、AIツール、証明アシスタント言語Leanの努力を組み合わせる協力プロジェクトを提案しました。このプロジェクトでは、4回までのマグマ演算の呼び出しで表現できる4694の等式法則に関する帰結グラフを記述することを目的としています。つまり、[…]