arXiv:2101.02602math.AG
HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.
We tell the story of how schemes were formalised in three different ways in the Lean theorem prover.
No comments linking this paper were found in the collected sources. Found in 1 HN submission from Jan 2021 to Jan 2021. Open submission discussions.
No comments linking this paper were found in the collected sources. Open submission discussions.
Connected through shared HN threads, not inferred similarity or a recommendation.