Differences

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

--- workshops:lean_workshop1224 [2024/10/23 14:07] – Add some text blocks describing workshop. lkastner
+++ workshops:lean_workshop1224 [2024/12/05 17:00] (current) – Add some project proposals lkastner
@@ Line 19: / Line 19: @@
 <HTML><div style="width: 100%;"><div style="float: left; padding-right: 10px; width: 400px;"></HTML>
 ^ Time  ^ **Thursday**  ^ **Friday** ^
-| 09:00-12:00  |                                            | Discussion and group work on interactions of LEAN and [[https://www.oscar-system.org/|OSCAR]]                                     ||
+| 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  | LEAN intro                          |    ||
+| 14:00-15:00  | Formalizing modern mathematics in Lean                          |    ||
-| 15:00-18:15  | Discussion and group work on interactions of LEAN and the [[https://portal.mardi4nfdi.de/wiki/Portal|MaRDI portal]]                                     |                                             ||
+| | //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]])                                        ||
 <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 ==
@@ Line 32: / Line 49: @@
 == 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