LEAN meets MaRDI and OSCAR

This is a workshop to structure the work on interactions of LEAN and the MaRDI portal, and LEAN and OSCAR.

Participants are encouraged to bring a laptop with an installed version of LEAN and OSCAR.

The workshop will take place in the E-N building of TU Berlin in the rooms 058 and 057. See here for a pin.

Please fill out the registration form!

Lean's mathematical library is a rapidly growing unified library of formalized mathematics. It contains a good foundation to verify current research problems in various areas of mathematics. In this talk I will give an overview of Mathlib, and describe some of the exciting ongoing projects. In particular, I will describe an ongoing project that I'm leading to formalize a generalization of Carleson's 1966 theorem in harmonic analysis, which shows that the Fourier series converges pointwise to the original function under weak conditions. This is a major result in harmonic analysis, with a difficult proof.

As LEAN is growing, such is the amount of data it contains in the form of proofs. The MaRDI portal can provide a frontend for this library. At the same time, LEAN can provide a mathematically rigorous foundation for the mathematics behind the portal.

OSCAR can be used to provide ingredients for proofs in LEAN, a simple example would be the inverse of a matrix. There is already some existing code that can be found at GitHub. We want to survey the directions we can take and sketch potential projects.

Formation of other working groups is encouraged. Some topics have been suggested:

1. Polyhedral geometry in LEAN
2. Game theory in LEAN
3. https://www.wikidata.org/wiki/Wikidata:WikiProject_Mathematics/1000%2BTheorems 1000 theorems in LEAN and portal
4. Polynomials in LEAN

1. B&B Hotel Berlin-Tiergarten, Englische Str. 1-4, Tel: +49 (0)30 33 00 66-0, Mail: berlin-tiergarten@hotelbb.com
2. Novum Hotel Gates, Knesebeckstraße 8-9, Buchung über die Hamburger Reservierungszentrale nicht empfehlenswert!
3. Hotel Indigo Berlin - Ku’damm, Hardenbergstrasse 15, Tel: +49 (0)30 860 90 90, Mail: info.indigoberlin@ihg.com
4. Hotel Motel One Berlin-Ku’Damm, Kantstraße 10, Tel: +49 (0)30 315 17 36-0, Mail: berlin-kudamm@motel-one.com
5. Novotel Berlin am Tiergarten, Strasse des 17 Juni 106-108, Tel: +49 (0)30 60 03 50, Mail: h3649@accor.com

1. Lars Kastner

Please contact us with any questions about the workshop. To email us, please use LASTNAME@math.tu-berlin.de.