Document Open Access Logo

A Natural Language Formalization of Perfectoid Rings in ℕaproche

Author Peter Koepke

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.6.pdf
  • Filesize: 0.7 MB
  • 15 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.6.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • formal mathematics
  • formalization
  • perfectoid rings
  • controlled natural language
  • Naproche

Metrics

Abstract

This paper describes an experiment to formalize sophisticated mathematics in the ℕaproche proof assistant which uses natural language input and a first-order internal logic. We view this as a contribution to the ongoing discussion whether formal systems for research mathematics require complex, computer-orientated type systems or whether approaches closer to traditional mathematical practices are possible. The formalization also explores the limits of the current ℕaproche system and avenues for further development.

Cite As Get BibTex

Peter Koepke. A Natural Language Formalization of Perfectoid Rings in ℕaproche. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.6

Author Details

Peter Koepke
  • University of Bonn, Germany

Funding

The formalization was completed during the Trimester Prospects of Formal Mathematics at the Hausdorff Research Institut for Mathematics, funded by the Deutsche Forschungsgemeinschaft under Germany’s Excellence Strategy – EXC-2047/1 – 390685813.

Supplementary Materials

References

  1. The Isabelle 2024 homepage. URL: https://isabelle.in.tum.de/website-Isabelle2024/.
  2. The Isabelle homepage. URL: https://isabelle.in.tum.de/.
  3. The Lean homepage. URL: https://lean-lang.org/.
  4. The ℕaproche Github repository. URL: https://github.com/naproche/naproche.
  5. The ℕaproche homepage. URL: https://naproche.github.io.
  6. The SAD homepage. URL: http://nevidal.org/sad.en.html.
  7. The Vampire homepage. URL: https://vprover.github.io/.
  8. Kevin Buzzard, Johan Commelin, and Patrick Massot. The Lean formalization of perfectoid spaces. URL: https://leanprover-community.github.io/lean-perfectoid-spaces/.
  9. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20, pages 299-312. ACM, January 2020. URL: https://doi.org/10.1145/3372885.3373830.
  10. Roland Huber. Continuous Valuations. Mathematische Zeitschrift, (212):455-477, 1993. Google Scholar
  11. Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, and Makarius Wenzel. The Isabelle/Naproche Natural Language Proof Assistant. In CADE 28, LNCS 12699, pages 614-624, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_36.
  12. Alexander Lyaletski and Konstantin Verchinine. Evidence Algorithm and System for Automated Deduction: A Retrospective View. In Intelligent Computer Mathematics, LNCS 6167, pages 411-426, 2010. URL: https://doi.org/10.1007/978-3-642-14128-7_35.
  13. Andrei Paskevich. The syntax and semantics of the ForTheL language. http://nevidal.org/download/forthel.pdf, 2007.
  14. Michael Rapoport. The work of Peter Scholze - Laudation for Scholze’s Fields medal 2018, 2022. URL: https://arxiv.org/abs/1909.07222.
  15. Peter Scholze. Perfectoid Spaces. Publications Mathématiques de l'IHÉS, (116):245-313, 2012. Google Scholar
  16. Peter Scholze. Etale cohomology of diamonds, 2022. URL: https://arxiv.org/abs/1709.07343.
  17. Stephan Schulz. The E Theorem Prover. URL: http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html.
  18. Torsten Wedhorn. Etale cohomology of diamonds, 2019. URL: https://arxiv.org/abs/1910.05934.
  19. Makarius Wenzel. Interaction with Formal Mathematical Documents in Isabelle/PIDE. In Intelligent Computer Mathematics, CICM 2019, LNCS 11617, pages 1-15, 2019. URL: https://doi.org/10.1007/978-3-030-23250-4_1.
  20. William M. Farmer. Theory Morphisms in Church’s Type Theory with Quotation and Evaluation. In H.Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, editors, Intelligent Computer Mathematics. CICM 2017, LNCS 10383, pages 147-162, 2017. URL: https://doi.org/10.1007/978-3-319-62075-6_11.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact