arakur/ProofHSI
https://github.com/arakur/ProofHSI
Tarski の高校代数問題の反例である Wilkie の等式と,Burris-Yean の構成した 12 要素の有限モデルについて,Lean4 を用いて形式検証しました.
Tarskiの高校代数問題
に関する
Lean 4
での形式化