A natural language formalization of perfectoid rings in Naproche

DOI10.4230/LIPICS.ITP.2025.6MaRDI QIDQ7323649zbMATH OpenFDO

Authors Peter Koepke

Publication date 1 September 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2025.6

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Continuous valuations
• Evidence algorithm and system for automated deduction: a retrospective view. (In honor of 40 years of the EA announcement)
• Interaction with formal mathematical documents in Isabelle/PIDE
• Perfectoid spaces
• The Isabelle/Naproche natural language proof assistant
• Theory morphisms in Church's type theory with quotation and evaluation

This page was built for publication: A natural language formalization of perfectoid rings in \(\mathbb{N}\)aproche

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7323649)