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.
December 05 and 06, 2024
Participants are encouraged to bring a laptop with an installed version of LEAN and OSCAR.
Location
The workshop will take place in the E-N building of TU Berlin in the rooms 058 and 057. See here for a pin.
Registration
Please fill out the registration form!
Schedule
| Time | Thursday | Friday | |
|---|---|---|---|
| 09:00-12:00 | Discussion and group work on interactions of LEAN and OSCAR | ||
| 12:00-14:00 | Lunch and arrival | Lunch and departure | |
| 14:00-15:00 | Formalizing modern mathematics in Lean | ||
| Floris van Doorn | |||
| 15:00-18:15 | Discussion and group work on interactions of LEAN and the MaRDI portal | ||
| ~18:45 | Dinner (self paid, at Café Hardenberg) | ||
Abstracts
Formalizing modern mathematics in Lean
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.
LEAN and the MaRDI portal
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.
LEAN and OSCAR
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.
Hotel recommendations in proximity of the Institute of Mathematics:
- B&B Hotel Berlin-Tiergarten, Englische Str. 1-4, Tel: +49 (0)30 33 00 66-0, Mail: berlin-tiergarten@hotelbb.com
- Novum Hotel Gates, Knesebeckstraße 8-9, Buchung über die Hamburger Reservierungszentrale nicht empfehlenswert!
- Hotel Indigo Berlin - Ku’damm, Hardenbergstrasse 15, Tel: +49 (0)30 860 90 90, Mail: info.indigoberlin@ihg.com
- Hotel Motel One Berlin-Ku’Damm, Kantstraße 10, Tel: +49 (0)30 315 17 36-0, Mail: berlin-kudamm@motel-one.com
- Novotel Berlin am Tiergarten, Strasse des 17 Juni 106-108, Tel: +49 (0)30 60 03 50, Mail: h3649@accor.com
Local organizers
Please contact us with any questions about the workshop. To email us, please use LASTNAME@math.tu-berlin.de.