ICMS 2018: What is in mathlib?

Stream: general

[Mario Carneiro]

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]

I got the first view on youtube!

[Kevin Buzzard]

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

[Patrick Massot]

12 views and counting

[Mario Carneiro]

Like, comment and subscribe ;)

[Mario Carneiro]

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