| Both sides previous revision Previous revision Next revision | Previous revision |
| workshops:lean_workshop1224 [2024/08/22 11:52] – First preliminary version of schedule lkastner | workshops:lean_workshop1224 [2024/12/05 17:00] (current) – Add some project proposals lkastner |
|---|
| ====== LEAN meets MaRDI 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 === | === December 05 and 06, 2024 === |
| |
| Please fill out the [[workshops:lean_workshop1224:registration|registration form]]! | 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> | <HTML><div style="width: 100%;"><div style="float: left; padding-right: 10px; width: 400px;"></HTML> |
| ^ Time ^ **Thursday** ^ **Friday** ^ | ^ Time ^ **Thursday** ^ **Friday** ^ |
| | 09:00-12:00 | | TBA || | | 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 || | | 12:00-14:00 | Lunch and arrival | Lunch and departure || |
| | 14:00-15:00 | LEAN intro | || | | 14:00-15:00 | Formalizing modern mathematics in Lean | || |
| | 15:00-18:15 | TBA | || | | | //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]]) || | | ~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 style="width: auto; overflow: hidden; padding-top: 5px; padding-right: 20px;"></HTML> |
| <HTML></div></div><div style="clear: both;"></div></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 |
| |
| |
| - [[https://www.novum-hotels.com/hotel-gates-berlin|Novum Hotel Gates]], Knesebeckstraße 8-9, Buchung über die Hamburger Reservierungszentrale nicht empfehlenswert! | - [[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.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 | - [[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 |
| |