open schedule, dates

oliver-butterley · Aug 2, 2023 · f56af2b · f56af2b
1 parent 0bea45f
commit f56af2b
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 40 deletions.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -1,8 +1,5 @@
 {
-    "cSpell.words": [
-        "Lenci",
-        "MIUR",
-        "Tanimoto",
-        "Vergata"
-    ]
+  "cSpell.words": ["Lenci", "MIUR", "Tanimoto", "Vergata"],
+  "editor.formatOnSaveMode": "file",
+  "editor.formatOnSave": true
 }
diff --git a/site/.vitepress/config.ts b/site/.vitepress/config.ts
@@ -24,12 +24,12 @@ export default defineConfig({
       { icon: 'github', link: 'https://github.com/oliver-butterley/formalisation' }
     ],
 
-    footer: {
-      message: 'Department of Mathematics, University of Rome Tor Vergata.',
+    // footer: {
+      // message: 'Department of Mathematics, University of Rome Tor Vergata.',
       // copyright: 'Copyright © 2019-present Someone'
-    },
+    // },
 
-    externalLinkIcon: true,
+    externalLinkIcon: false,
 
   }
 })
diff --git a/site/index.md b/site/index.md
@@ -4,14 +4,14 @@ layout: home
 
 hero:
   name: "Formalisation in Rome"
-  text: "25-27 January 2024"
-  tagline: Over the last several years computerized tools for verifying and manipulating proofs have become much more mature, and as a result formalized proofs have the potential to play a meaningful role in mathematical innovation and teaching well beyond their traditional role in the foundations of mathematics.    
-#  image:
-#    src: /unsound.png
-#    alt: unsound
+  text: "24-26 January 2024"
+  tagline: Over the last several years computerized tools for verifying and manipulating proofs have become much more mature, and as a result formalized proofs have the potential to play a meaningful role in mathematical innovation and teaching well beyond their traditional role in the foundations of mathematics.
+  #  image:
+  #    src: /unsound.png
+  #    alt: unsound
   actions:
     - theme: brand
-      text: See speakers and schedule
+      text: See speakers, schedule and further information
       link: /info
 
 features:
@@ -22,7 +22,6 @@ features:
     details: A series of hands-on sessions intended to give participants first-hand knowledge using the Lean language and associated tools.
     link: /info#schedule
   - title: Audience
-    details: We hope this will provide an introduction to the area for working mathematicians and advanced students in a variety of fields.
+    details: We aim to provide an introduction to the area for working mathematicians and advanced students in a variety of fields.
     link: /info#summary
 ---
-
diff --git a/site/info.md b/site/info.md
@@ -8,41 +8,45 @@ layout: doc
 
 Over the last several years computerized tools for verifying and manipulating proofs have become much more mature, and as a result formalized proofs have the potential to play a meaningful role in mathematical innovation and teaching well beyond their traditional role in the foundations of mathematics.
 
-This short program consists of three colloquium talks on major aspects of formalization, in terms of both underlying ideas and concrete implementations, together with a series of workshop-style sessions intended to give participants first-hand knowledge using the Lean language and associated tools.  We hope this will provide an introduction to the area for working mathematicians and advanced students in a variety of fields.
+This short program consists of three colloquium talks on major aspects of formalization, in terms of both underlying ideas and concrete implementations, together with a series of workshop-style sessions intended to give participants first-hand knowledge using the [Lean](https://leanprover.github.io/) language, its [mathematical library](https://leanprover-community.github.io/index.html) and associated tools.
+We hope this will provide an introduction to the area for working mathematicians and advanced students in a variety of fields.
 
 - Duration: 3 days
 - Day 1: Intro to Lean; Day 2: Numbers, sets and functions; Day 3: Algebra, topology and analysis.
-- 1 colloquium talk every day
+- 3 colloquium talks, one each day
 - Workshop during the remaining time
 
+Copious quantities of coffee ☕ and space to code 💻 will be available.
+The short workshop is designed to give participants sufficient knowledge and support so that after the event they can then continue making progress with it in their own time.
+
 ::: warning
-  Everything is very preliminary
+Everything is very preliminary
 :::
 
 # Schedule {#schedule}
 
-|             | Wed 25/01/2024            | Thu 26/01/2024             | Fri 27/01/2024        |
-| :---------: | :------------------------ | :------------------------- | :-------------------- |
-| 9:30-11:00  |                           | session 2: logic           | session 5: algebra    |
-| 10:30-12:30 | _session 0: introduction_ | session 3: sets, functions | session 6: topology   |
-| 12:30-14:30 | _lunch_                   | lunch                      | lunch                 |
-| 14:30-15:30 | **colloquium talk 1**     | **colloquium talk 2**      | **colloquium talk 3** |
-| 15:30-16:30 | coffee                    | coffee                     | coffee                |
-| 16:30-18:00 | session 1: basics         | session 4: numbers         | session 7: analysis   |
+|             | Wed 24/01/2024   | Thu 25/01/2024   | Fri 26/01/2024    |
+| :---------: | :--------------- | :--------------- | :---------------- |
+| 10:00-11:30 |                  | workshop         | workshop          |
+| 11:30-13:00 | _(pre-workshop)_ | workshop         | workshop          |
+| 13:00-14:30 | 🍽️               | 🍽️               | 🍽️                |
+| 14:30-15:30 | **Colloquium 1** | **Colloquium 2** | **Colloquium 3**  |
+| 15:30-16:00 | ☕               | ☕               | ☕                |
+| 16:00-17:30 | workshop         | workshop         | _(post-workshop)_ |
 
 ::: details Session topics (tap to view)
 
-  |     | session             | topics                                                                       |
-  | --- | ------------------- | ---------------------------------------------------------------------------- |
-  | 0   | **introduction**    | tutorial on Lean, installation of Lean (if needed), topics in mathlib        |
-  | 2   | **logic**           | how to deal with all logical connectives and quantifiers                     |
-  | 3   | **sets, functions** | intersections, (pre)images, extensionality                                   |
-  | 4   | **numbers**         | how to work with the numbers in `ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ` and relevant tactics |
-  | 5   | **algebra**         | groups, rings, fields, linear algebra                                        |
-  | 6   | **topology**        | topological spaces, filters                                                  |
-  | 7   | **analysis**        | differentiation, integration, (manifolds?)                                   |
+|     | session             | topics                                                                       |
+| --- | ------------------- | ---------------------------------------------------------------------------- |
+| 0   | **introduction**    | tutorial on Lean, installation of Lean (if needed), topics in mathlib        |
+| 2   | **logic**           | how to deal with all logical connectives and quantifiers                     |
+| 3   | **sets, functions** | intersections, (pre)images, extensionality                                   |
+| 4   | **numbers**         | how to work with the numbers in `ℕ`, `ℤ`, `ℚ`, `ℝ`, `ℂ` and relevant tactics |
+| 5   | **algebra**         | groups, rings, fields, linear algebra                                        |
+| 6   | **topology**        | topological spaces, filters                                                  |
+| 7   | **analysis**        | differentiation, integration, (manifolds?)                                   |
 
-::: 
+:::
 
 ## Speakers / Scientific organizers {#speakers}
 
@@ -65,12 +69,18 @@ These are the ones to contact for anything practical.
 
 In case you are interested, please register, it helps us a lot with the organization!
 
-<!-- ## Other events of interest -->
+## Other events of interest
+
+For those who want to go deeper into Lean and mathlib, check out some [other Lean events](https://leanprover-community.github.io/events.html).
 
 ## Location
 
 All activities will be held in the Mathematics department, University of Rome Tor Vergata.
 
+## Getting started with Lean
+
+If you haven't already, [get started](https://leanprover-community.github.io/get_started) by installing Lean or using it online.
+
 ### Support
 
 This program is funded as part of the MIUR Excellence Department Project MatMod@TOV awarded to the Department of Mathematics, University of Rome Tor Vergata.