70

IRUS TotalDownloads

### Formalising perfectoid spaces

File | Description | Size | Format | |
---|---|---|---|---|

1910.12320v1.pdf | Working paper | 660.81 kB | Adobe PDF | View/Open |

Title: | Formalising perfectoid spaces |

Authors: | Buzzard, K Commelin, J Massot, P |

Item Type: | Conference Paper |

Abstract: | Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover. This experiment confirms that a proof assistant can handle complexity in that direction, which is rather different from formalising a long proof about simple objects. It also confirms that mathematicians with no computer science training can become proficient users of a proof assistant in a relatively short period of time. Finally, we observe that formalising a piece of mathematics that is a trending topic boosts the visibility of proof assistants amongst pure mathematicians. |

Issue Date: | 1-Jan-2020 |

Date of Acceptance: | 1-Jan-2020 |

URI: | http://hdl.handle.net/10044/1/76749 |

DOI: | 10.1145/3372885.3373830 |

ISBN: | 978-1-4503-7097-4 |

Publisher: | Association for Computing Machinery |

Start Page: | 299 |

End Page: | 312 |

Journal / Book Title: | Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs |

Copyright Statement: | © 2019 The Author(s) |

Conference Name: | POPL: Principles of Programming Languages |

Keywords: | cs.LO cs.LO math.AG math.NT cs.LO cs.LO math.AG math.NT |

Notes: | 19 pages, see also https://leanprover-community.github.io/lean-perfectoid-spaces/ |

Publication Status: | Published |

Conference Place: | New Orleans, USA |

Open Access location: | https://dl.acm.org/doi/10.1145/3372885.3373830 |

Online Publication Date: | 2020-01-01 |

Appears in Collections: | Pure Mathematics Mathematics Faculty of Natural Sciences |