この証明を理解できるか？形式化された数学の一端

スティーブン・ウルフラムは、長年の数学上の謎、驚くほど単純なブール代数の公理の証明に取り組みます。自動定理証明を用いて生成されたこの証明は、非常に複雑で、人間には理解不能なままです。「機械語」レベルでの操作を解剖し、この証明を人間にも理解できる形にするという課題を提示します。大規模言語モデル（LLM）による証明の理解と簡素化の可能性、そして数学の未来への影響について議論します。結論として、数学の証明の中には本質的に解釈不可能なものがあり、数学はますます実験科学に近づくことを示唆しています。