====== 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 [[https://maps.app.goo.gl/t7fztRZ5JW22CF8WA|here]] for a pin. ===Registration=== Please fill out the [[workshops:lean_workshop1224:registration|registration form]]! ===Schedule===
^ Time ^ **Thursday** ^ **Friday** ^ | 09:00-12:00 | | Discussion and group work on interactions of LEAN and [[https://www.oscar-system.org/|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 [[https://portal.mardi4nfdi.de/wiki/Portal|MaRDI portal]] (and other groups) | || | ~18:45 | **Dinner** (self paid, at [[http://cafe-hardenberg.com/|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 [[https://github.com/todbeibrot/Lean-Oscar|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: - Polyhedral geometry in LEAN - Game theory in LEAN - [[https://www.wikidata.org/wiki/Wikidata:WikiProject_Mathematics/1000%2BTheorems]] 1000 theorems in LEAN and portal - Polynomials in LEAN =====Hotel recommendations in proximity of the Institute of Mathematics:===== - [[https://www.hotel-bb.com/de/hotel/berlin-tiergarten|B&B Hotel Berlin-Tiergarten]], Englische Str. 1-4, Tel: +49 (0)30 33 00 66-0, Mail: berlin-tiergarten@hotelbb.com - [[https://www.novum-hotels.com/hotel-gates-berlin|Novum Hotel Gates]], Knesebeckstraße 8-9, Buchung über die Hamburger Reservierungszentrale nicht empfehlenswert! - [[https://www.ihg.com/hotelindigo/hotels/de/de/berlin/beriw/hoteldetail|Hotel Indigo Berlin - Ku’damm]], Hardenbergstrasse 15, Tel: +49 (0)30 860 90 90, Mail: info.indigoberlin@ihg.com - [[https://www.motel-one.com/de/hotels/berlin/hotel-berlin-kudamm/|Hotel Motel One Berlin-Ku’Damm]], Kantstraße 10, Tel: +49 (0)30 315 17 36-0, Mail: berlin-kudamm@motel-one.com - [[https://all.accor.com/hotel/3649/index.de.shtml|Novotel Berlin am Tiergarten]], Strasse des 17 Juni 106-108, Tel: +49 (0)30 60 03 50, Mail: h3649@accor.com ===== Local organizers ===== - [[https://page.math.tu-berlin.de/~kastner/|Lars Kastner]] Please contact us with any questions about the workshop. To email us, please use ''LASTNAME@math.tu-berlin.de''.