mathlib

swMATH36839MaRDI QIDQ52541FDOQ52541

Jump to:navigation, searchThe Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant.

Author name not available (Why is that?)

Source code repository: https://github.com/leanprover-community/mathlib

Described by source

• Maintaining a library of formal mathematics

Cited In (9)

• Leveraging the information contained in theory presentations
• Schemes in Lean
• A Coq formalization of Lebesgue integration of nonnegative functions
• Metric spaces are paracompact
• Formalizing geometric algebra in Lean
• Formalizing Galois Theory
• Program logic for higher-order probabilistic programs in Isabelle/HOL
• A bi-directional extensible interface between Lean and Mathematica
• Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem

This page was built for software: mathlib