Formal Methods in Mathematics / Lean Together 2020 ran from Monday, January 6 to Friday, January 10, 2020 at Carnegie Mellon University, in Pittsburgh, Pennsylvania. The meeting was a successor to Lean Together 2019.

The first three days focused on formal methods in pure and applied mathematics, including interactive theorem proving, automated reasoning, verification of symbolic and numeric computation, and general mathematical infrastructure.

The last two days were devoted to specifically to the Lean Theorem Prover and its core library, mathlib. Users and library developers had opportunities to discuss work in progress and plans for the future. There was also a session devoted to the Formal Abstracts project.

Attendance was free and open to the public, and talks were livestreamed using Zoom.

Most talks are available on YouTube via links from the abstracts page. The recordings are not high quality, but can be watched alongslide the slides. There is a full playlist here.

The meeting was supported by grant FA9550-18-1-0325 from the Air Force Office of Scientific Research. The contents do not necessarily reflect the views of the AFOSR.