workshops:lean_workshop1224

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 (and other groups)
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 (and other groups)
~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.

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

  1. Polyhedral geometry in LEAN
  2. Game theory in LEAN
  3. 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

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

  • workshops/lean_workshop1224.txt
  • Last modified: 2024/12/05 17:00
  • by lkastner