Zulip Chat Archive

Stream: general

Topic: ICMS 2018: What is in mathlib?

Mario Carneiro (Jul 27 2018 at 04:59):

Hi all, you can check out yesterday's ICMS talk on YouTube: https://youtu.be/5tS4j_A1ZvU

The Lean 3 mathematical library (mathlib)

Abstract: The Lean 3 "mathlib" library has been rewritten from the ground up to take advantage of the new features and tactics framework. In this article we take stock of the meteoric growth of the library in the past several months, which covers elementary number theory, algebra, ring theory, topology and analysis, set theory, as well as support for verified pure-functional programming with lists, maps, arrays, quotient types, and coinductive types. This is supplemented with additional tactics, written in Lean on top of the Lean 3 tactic framework, for proving arithmetic equalities and inequalities, deciding the equational theory of commutative rings, as well as general automation tactics based on heuristic instantiation and resolution proving.

Patrick Massot (Jul 27 2018 at 08:08):

I got the first view on youtube!

Kevin Buzzard (Jul 27 2018 at 08:09):

I wondered who it was, as I was getting the second one ;-)

Patrick Massot (Jul 27 2018 at 09:25):

12 views and counting

Mario Carneiro (Jul 27 2018 at 11:53):

Like, comment and subscribe ;)

Mario Carneiro (Jul 27 2018 at 11:54):

(not really, I don't really care about getting a youtube audience)

Last updated: Aug 03 2023 at 10:10 UTC