Maintaining a Library of Formal Mathematics

被引：11

作者：

van Doorn, Floris ^{[1
]}

Ebner, Gabriel ^{[2
]}

Lewis, Robert Y. ^{[2
]}

机构：

[1] Univ Pittsburgh, Pittsburgh, PA 15260 USA

[2] Vrije Univ Amsterdam, NL-1081 HV Amsterdam, Netherlands

来源：

INTELLIGENT COMPUTER MATHEMATICS, CICM 2020 | 2020年 / 12236卷

基金：

荷兰研究理事会; 欧洲研究理事会;

关键词：

Formal mathematics; Library development; Linting; PROOF;

D O I：

10.1007/978-3-030-53518-6_16

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.

引用

页码：251 / 267

页数：17

共 22 条

[1]

Andronick June, 2019, Formal Methods - The Next 30 Years. Third World Congress, FM 2019. Proceedings. Lecture Notes in Computer Science (LNCS 11800), P11, DOI 10.1007/978-3-030-30942-8_2

[2]

Avigad J., 2014, Theorem Proving in Lean

[3] The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar [J].

Bancerek, Grzegorz ;

Bylinski, Czeslaw ;

Grabowski, Adam ;

Kornilowicz, Artur ;

Matuszewski, Roman ;

Naumowicz, Adam ;

Pak, Karol .

JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) :9-32

[4] The Lean Mathematical Library [J].

CPP '20: PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2020, :367-381

[5]

Bourke Timothy, 2012, 11th International Conference, AISC 2012 19th Symposium, Calculemus 2012. Proceedings 5th International Workshop, DML 2012. 11th International Conference, MKM 2012. Systems and Projects, Held as Part of CICM 2012, P32, DOI 10.1007/978-3-642-31374-5_3

[6] Formalising Perfectoid Spaces [J].

Buzzard, Kevin ;

Commelin, Johan ;

Massot, Patrick .

CPP '20: PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2020, :299-312

[7]

Cohen C., 2020, Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi

[8]

Dahmen S.R., 2019, Leibniz International Proceedings in Informatics (LIPIcs), V4, DOI [10.4230/LIPIcs.ITP. 2019.15, DOI 10.4230/LIPICS.ITP.2019.15]

[9] The Lean Theorem Prover (System Description) [J].

de Moura, Leonardo ;

Kong, Soonho ;

Avigad, Jeremy ;

van Doorn, Floris ;

von Raumer, Jakob .

AUTOMATED DEDUCTION - CADE-25, 2015, 9195 :378-388

[10] A metaprogramming framework for formal verification [J].

Ebner G. ;

Ullrich S. ;

Roesch J. ;

Avigad J. ;

De Moura L. .

1600, Association for Computing Machinery (01)

← 1 2 3 →