Algebraically Closed Fields in Isabelle/HOL

de Vilhena, Paulo Emílio; Paulson, Lawrence

View / Open Files

Accepted version (PDF, 332Kb)

Authors

de Vilhena, Paulo Emílio

Paulson, Lawrence

Journal Title

Automated Reasoning—10th International Joint Conference, IJCAR 2020

Conference Name

International Joint Conference on Automated Reasoning

ISSN

0302-9743

Type

Conference Object

This Version

Metadata

Show full item record

Citation

de Vilhena, P. E., & Paulson, L. (2020). Algebraically Closed Fields in Isabelle/HOL. Automated Reasoning—10th International Joint Conference, IJCAR 2020 https://doi.org/10.1007/978-3-030-51054-1_12

Abstract

A fundamental theorem states that every field admits an algebraically closed extension. Despite its central importance, this theorem has never before been formalised in a proof assistant. We fill this gap by documenting its formalisation in Isabelle/HOL, describing the difficulties that impeded this development and their solutions.

Sponsorship

ERC Advanced Grant ALEXANDRIA (Project GA 742178)

Funder references

European Commission Horizon 2020 (H2020) ERC (742178)

Identifiers

External DOI: https://doi.org/10.1007/978-3-030-51054-1_12

This record's URL: https://www.repository.cam.ac.uk/handle/1810/305801