HackerPapers

arXiv:1910.09336cs.LO

The Lean mathematical library

The mathlib Community

Abstract

This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led us here.

arXiv comments
Journal reference
DOI
doi:10.1145/3372885.3373824
Subjects
cs.LOLogic in Computer Science math.LOLogic

On Hacker News

Linked by 2 identifiable commenters in 3 comments across 2 threads, from Nov 2020 to Apr 2022. Found in 1 HN submission from Apr 2022 to Apr 2022. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments2 threads

  1. There’s more to mathematics than rigour and proofs (2007) 2 comments

    • I understood math much better after following the Software Foundations tutorials: https://softwarefoundations.cis.upenn.edu/ Another good starting point (for mathematicians) would be the Lean community group and the Math lib project: https://arxiv.org/pdf/1910.09336.pdf…

      mbrodersenView on HNParent context

    • https://arxiv.org/pdf/1910.09336.pdf

      mbrodersenView on HNParent context

  2. What Gödel Discovered 1 comment

    • > Hence why they need results reviewed and a community to agree upon what's acceptable as a proof. Otherwise reviewing a proof would be an automatic process, if everything was done in the world of syntactic symbols with clear rules that tie one statement to the next.…

      schoenView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.