Document Open Access Logo

Formalising the Proj Construction in Lean

Author Jujian Zhang

Thumbnail PDF


  • Filesize: 0.87 MB
  • 17 pages

Document Identifiers

Author Details

Jujian Zhang
  • Department of Mathematics, Imperial College London, UK


I want to thank Eric Wieser for his contribution and suggestion in formalising homogeneous ideals and homogeneous localisation; Andrew Yang and Junyan Xu for their review and comments on my code; Kevin Buzzard for suggesting this project and all the contributors to mathlib for otherwise this project would not have been possible.

Cite AsGet BibTex

Jujian Zhang. Formalising the Proj Construction in Lean. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 35:1-35:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Many objects of interest in mathematics can be studied both analytically and algebraically, while at the same time, it is known that analytic geometry and algebraic geometry generally do not behave the same. However, the famous GAGA theorem asserts that for projective varieties, analytic and algebraic geometries are closely related; the proof of Fermat’s last theorem, for example, uses this technique to transport between the two worlds [Serre, 1955]. A crucial step of proving GAGA is to calculate cohomology of projective space [Neeman, 2007; Godement, 1958], thus I formalise the Proj construction in the Lean theorem prover for any ℕ-graded R-algebra A and construct projective n-space as Proj A[X₀,… , X_n]. This is the first family of non-affine schemes formalised in any theorem prover.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Mathematics of computing → Topology
  • Lean
  • formalisation
  • algebraic geometry
  • scheme
  • Proj construction
  • projective geometry


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Anthony Bordg, Lawrence Paulson, and Wenda Li. Simple type theory is not too simple: Grothendieck’s schemes without dependent types. Experimental Mathematics, 31(2):364-382, 2022. URL:
  2. Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, and Scott Morrison. Schemes in Lean. Experimental Mathematics, 31(2):355-363, 2022. Google Scholar
  3. Laurent Chicli. Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq. PhD thesis, INRIA, 2001. Google Scholar
  4. Wei-Liang Chow. On compact complex analytic varieties. American Journal of Mathematics, 71(4):893-914, 1949. URL:
  5. Mathlib Contributors. Lean mathlib., 2022.
  6. Mathlib Contributors. Mathlib documentation., 2023.
  7. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction, pages 378-388. Springer, 2015. Google Scholar
  8. Roger Godement. Topologie algébrique et théorie des faisceaux. Publications de, 1, 1958. Google Scholar
  9. Robin Hartshorne. Graduate texts in mathematics. Algebraic Geometry, 52, 1977. Google Scholar
  10. Saunders MacLane and Ieke Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Springer Science & Business Media, 2012. Google Scholar
  11. Anders Mörtberg and Max Zeuner. Towards a formalization of affine schemes in cubical agda. Google Scholar
  12. Amnon Neeman. Algebraic and analytic geometry. Cambridge University Press, 2007. Google Scholar
  13. Jean-Pierre Serre. Géométrie analytique et géométrie algébrique. Ann. Inst. Fourier, VI (1955-56), pages 1-42, 1955. Google Scholar
  14. The Stacks Project Authors. Stacks Project., 2018.
  15. Ravi Vakil. The rising sea: Foundations of algebraic geometry. 2017. URL http://virtualmath1. stanford. edu/~ vakil/216blog, 24:29, 2017. Google Scholar
  16. Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. available at URL:
  17. Eric Wieser and Jujian Zhang. Graded rings in Lean’s dependent type theory. In International Conference on Intelligent Computer Mathematics, pages 122-137. Springer, 2022. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail