| Both sides previous revision Previous revision Next revision | Previous revision |
| workshops:lean_workshop1224 [2024/11/12 08:31] – Add Floris abstract lkastner | workshops:lean_workshop1224 [2024/12/05 17:00] (current) – Add some project proposals lkastner |
|---|
| <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 | | 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 || | | 12:00-14:00 | Lunch and arrival | Lunch and departure || |
| | 14:00-15:00 | Formalizing modern mathematics in Lean | || | | 14:00-15:00 | Formalizing modern mathematics in Lean | || |
| | | //Floris van Doorn// | || | | | //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]] | || | | 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> |
| == LEAN and OSCAR == | == 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. | 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 |
| |
| |