Lean 中的概形
代数几何
2022-03-21 v2
摘要
我们讲述了概形在 Lean 定理证明器中以三种不同方式被形式化的历程。
关键词
引用
@article{arxiv.2101.02602,
title = {Schemes in Lean},
author = {Kevin Buzzard and Chris Hughes and Kenny Lau and Amelia Livingston and Ramon Fernández Mir and Scott Morrison},
journal= {arXiv preprint arXiv:2101.02602},
year = {2022}
}
备注
10 pages. To appear in Experimental Mathematics