Differences

This shows you the differences between two versions of the page.

--- workshops:lean_workshop1224 [2024/08/21 19:40] – LEAN workshop page lkastner
+++ workshops:lean_workshop1224 [2024/12/05 17:00] (current) – Add some project proposals lkastner
@@ Line 1: / Line 1: @@
-====== LEAN meets polymake and OSCAR  ======
+====== 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, polymake and OSCAR.
+Participants are encouraged to bring a laptop with an installed version of LEAN and OSCAR.
 ===Location===
@@ Line 13: / Line 16: @@
 Please fill out the [[workshops:lean_workshop1224:registration|registration form]]!
-===Preliminary Schedule===
+===Schedule===
 <HTML><div style="width: 100%;"><div style="float: left; padding-right: 10px; width: 400px;"></HTML>
-|  |**Thursday**   |      **Friday**                                                                                                             ||
+^ Time  ^ **Thursday**  ^ **Friday** ^
-| 09:00-09:30  |                                            |                                      ||
+| 09:00-12:00  |                                            | Discussion and group work on interactions of LEAN and [[https://www.oscar-system.org/|OSCAR]] (and other groups)                                    ||
-| 09:30-10:30  |   |                                                         ||
+| 12:00-14:00  | Lunch and arrival | Lunch and departure                                 ||
-| 10:30-11:00  |                                                                          ||
+| 14:00-15:00  | Formalizing modern mathematics in Lean                          |    ||
-| 11:00-12:00  |                       |   ||
+| | //Floris van Doorn// | ||
-| 12:00-14:00  |                                 ||
+| 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)                                     |                                             ||
-| 14:00-15:00  |                           |    |
-| 15:00-15:30  |                                                                                   ||
-| 15:30-16:30  | ||
-| 16:30-18:15  |                                                                                             ||
 | ~18:45       | **Dinner** (self paid, at [[http://cafe-hardenberg.com/|Café Hardenberg]])                                        ||
 <HTML></div><div style="width: auto; overflow: hidden; padding-top: 5px; padding-right: 20px;"></HTML>
 <HTML></div></div><div style="clear: both;"></div></HTML>
+=== 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
@@ Line 36: / Line 62: @@
   - [[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]], Kannstraße 10, Tel: +49 (0)30 315 17 36-0, Mail: berlin-kudamm@motel-one.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