Verification on Tarski's High School Algebra Problem with Lean4

Tarski の高校代数問題の反例である Wilkie の等式と，Burris-Yean の構成した 12 要素の有限モデルについて，Lean4 を用いて形式検証しました．

参考文献

• Joseph Tassarotti. Tarski's High School Algebra Problem. http://www.cs.bc.edu/~tassarot/2011/12/30/Tarski.html
• Stanley Burris, Karen Yeats. The Saga of the High School Identities.