Zulip Chat Archive
Stream: Lean for teaching
Topics:
- Natural numbers game Lean4 (64 messages, latest: Dec 19 2023 at 13:26)
- Post-quantum crypto (1 message, latest: Dec 18 2023 at 20:52)
- Bool vs Prop (15 messages, latest: Dec 18 2023 at 12:54)
- A useful example of "induction … using …" (?) (18 messages, latest: Dec 13 2023 at 10:56)
- best option for live collaboration? (4 messages, latest: Dec 12 2023 at 20:48)
- Lean4 cheatsheet (194 messages, latest: Dec 12 2023 at 17:37)
- Verbose Lean (33 messages, latest: Nov 29 2023 at 13:02)
- ✔
havetactic in lean4game (3 messages, latest: Nov 27 2023 at 22:15) - Lean 4 version for teaching (29 messages, latest: Nov 02 2023 at 14:21)
- teaching resources on website (9 messages, latest: Oct 24 2023 at 14:50)
- Lean courses around the world (44 messages, latest: Oct 08 2023 at 16:35)
- cache on project with gitpod (10 messages, latest: Oct 03 2023 at 08:49)
- Simplest possible example? (19 messages, latest: Sep 30 2023 at 19:15)
- Lean at Duke (15 messages, latest: Sep 12 2023 at 00:20)
- Automatic grading of lean4 codes (44 messages, latest: Sep 11 2023 at 19:36)
- APPAM (1 message, latest: Sep 11 2023 at 13:28)
- codespaces (74 messages, latest: Sep 11 2023 at 05:03)
- Gyde (7 messages, latest: Aug 20 2023 at 04:00)
- ProofBuddy: A Proof Assistant for Learning and Monitoring (4 messages, latest: Aug 17 2023 at 08:56)
- easy to read proofs on mathlib4 (9 messages, latest: Jul 14 2023 at 15:01)
- Waterproof: educational software for learning how to writ… (8 messages, latest: Jul 13 2023 at 16:02)
- Teach Coq first? (45 messages, latest: Jul 13 2023 at 13:34)
- Learning mathematics with Lean (UK conference) (7 messages, latest: Jul 13 2023 at 08:41)
- Lean club student org (8 messages, latest: Jul 12 2023 at 11:08)
- An exercise using induction (32 messages, latest: Jun 29 2023 at 00:38)
- Lean project for high-school students (6 messages, latest: Jun 20 2023 at 20:08)
- Term mode vs tactic mode (22 messages, latest: Jun 07 2023 at 21:08)
- High School Research (20 messages, latest: Jun 07 2023 at 09:22)
- Easy way to install lean4/mathlib4 (3 messages, latest: May 23 2023 at 22:47)
- How to prove it in Lean (9 messages, latest: May 09 2023 at 16:23)
- Lean3 or Lean4? (9 messages, latest: May 05 2023 at 14:09)
- ✔ Jupyterhub (6 messages, latest: Apr 23 2023 at 06:44)
- Two workshops (17 messages, latest: Apr 20 2023 at 16:57)
- Feedback from my seminar (8 messages, latest: Mar 12 2023 at 20:51)
- Running an intro to Lean workshop (11 messages, latest: Feb 25 2023 at 20:12)
- detecting plagiarism (9 messages, latest: Feb 24 2023 at 23:35)
- use of Zulip (9 messages, latest: Jan 16 2023 at 15:09)
- Course in Edinburgh 2023 (4 messages, latest: Jan 10 2023 at 17:21)
- #Lean Independent Study Project? (7 messages, latest: Jan 09 2023 at 09:25)
- overview (6 messages, latest: Jan 05 2023 at 06:48)
- natural number game (54 messages, latest: Jan 02 2023 at 13:19)
- coercion in inequalities (8 messages, latest: Dec 10 2022 at 17:38)
- enforcing structured proofs (37 messages, latest: Dec 07 2022 at 18:37)
- Resources for finite sets/types (6 messages, latest: Dec 06 2022 at 01:24)
- Intro to Proofs in US with Lean (13 messages, latest: Nov 10 2022 at 19:48)
- Installation manual for students (6 messages, latest: Oct 31 2022 at 16:39)
- Literate Lean (20 messages, latest: Oct 14 2022 at 18:52)
- Table of content (2 messages, latest: Oct 14 2022 at 18:16)
- Marmite (33 messages, latest: Oct 12 2022 at 21:33)
- autograding with GH classroom (78 messages, latest: Oct 10 2022 at 17:36)
- Xena summer workshop 2022 (4 messages, latest: Oct 05 2022 at 20:48)
- Automatic marking with moodle (14 messages, latest: Sep 20 2022 at 15:13)
- Intro to Proofs at Johns Hopkins (1 message, latest: Sep 02 2022 at 21:40)
- experience with GH classroom or equivalent (4 messages, latest: Aug 24 2022 at 18:54)
- Sphinx setup for Mathematics in Lean (4 messages, latest: Jul 06 2022 at 20:52)
- ✔ Definition of Nat in Lean4 library (2 messages, latest: Jul 06 2022 at 07:48)
- Definition of Nat in Lean4 library (3 messages, latest: Jul 06 2022 at 06:55)
- Formalising Mathematics 2022 Imperial course (23 messages, latest: Apr 21 2022 at 15:12)
- Fields Institute Mathematics Education Forum March Meeting (25 messages, latest: Apr 05 2022 at 13:46)
- Functional programming (17 messages, latest: Mar 27 2022 at 22:50)
- Making this stream public (4 messages, latest: Mar 25 2022 at 15:15)
- stream events (1 message, latest: Mar 25 2022 at 13:20)
- type of 'list' (2 messages, latest: Feb 01 2022 at 17:17)
- Ideas for half-a-year-long undergrad Lean project (58 messages, latest: Feb 01 2022 at 01:02)
- Two hours of Lean (9 messages, latest: Jan 22 2022 at 14:26)
- format_lean (16 messages, latest: Jan 12 2022 at 17:56)
- using Observable notebooks for teaching (32 messages, latest: Jan 10 2022 at 22:35)
- Teaching Tech Together (1 message, latest: Dec 23 2021 at 13:32)
- Hydras & Co. and snippets for documentation (2 messages, latest: Dec 19 2021 at 17:00)
- submit or share nng solutions (25 messages, latest: Dec 07 2021 at 18:01)
- auto-grading (48 messages, latest: Dec 04 2021 at 23:08)
- teaching algebraic structures (29 messages, latest: Oct 27 2021 at 18:31)
- A zero-config Lean/mathlib development environment (24 messages, latest: Oct 14 2021 at 18:28)
- Thoma-Iannone paper on teaching with Lean (1 message, latest: Jul 16 2021 at 19:37)
- Lean ideas for smart high school students (5 messages, latest: Jun 26 2021 at 03:05)
- Automated Assessment (1 message, latest: Jun 09 2021 at 15:44)
- education (16 messages, latest: Jun 04 2021 at 14:47)
- Patrick's course (15 messages, latest: Mar 16 2021 at 06:40)
- Nipkow on teaching with ITP (1 message, latest: Jan 17 2021 at 19:34)
- Formalize!(?) (5 messages, latest: Jan 16 2021 at 17:15)
- definability in a FOL Structure (5 messages, latest: Sep 17 2020 at 22:52)
- definability in a FOL structure (1 message, latest: Sep 17 2020 at 20:10)
- The lady and the tiger (23 messages, latest: Sep 06 2020 at 22:23)
- linter for helping grading (37 messages, latest: Sep 06 2020 at 22:08)
- tools for teaching with Lean (5 messages, latest: Jul 26 2020 at 03:36)
- by { … } vs. begin … end (15 messages, latest: Jun 20 2020 at 09:14)
- Real analysis (191 messages, latest: Jun 09 2020 at 12:37)
- ex quod libet (6 messages, latest: May 22 2020 at 22:02)
- Quantum computing (139 messages, latest: May 18 2020 at 14:24)
- discrete math book (1 message, latest: May 02 2020 at 22:16)
- from algorithms to proofs (4 messages, latest: May 02 2020 at 15:58)
- Logipedia Club of Teachers (6 messages, latest: Mar 02 2020 at 13:02)
- Hints? (12 messages, latest: Feb 15 2020 at 08:03)
- a = b \to f a = f b? (7 messages, latest: Jan 31 2020 at 22:25)
- graphs (10 messages, latest: Nov 22 2019 at 12:02)
- Making Lean web games (1 message, latest: Nov 16 2019 at 10:50)
- Kevin 2019 (6 messages, latest: Oct 10 2019 at 07:49)
- Kevin teaching 2019 (1 message, latest: Oct 10 2019 at 07:48)
- Next step after the Logic and Proofs (52 messages, latest: Sep 30 2019 at 19:55)
- real numbers in Lean (1 message, latest: Sep 21 2019 at 16:46)
- Draft book using Lean for CS Discrete Math (5 messages, latest: Sep 01 2019 at 13:48)
- Are freshmen ripe for formal proofs? (8 messages, latest: Jul 28 2019 at 10:54)
- bachelor thesis subjects (3 messages, latest: Jul 20 2019 at 17:23)
casesisn't using my notation (32 messages, latest: May 28 2019 at 14:03)- Papers (3 messages, latest: Mar 06 2019 at 09:57)
- Scott's course (37 messages, latest: Mar 05 2019 at 23:08)
- Discrete Mathematics - Kevin Sullivan (1 message, latest: Mar 01 2019 at 00:16)
- hello (1 message, latest: Feb 28 2019 at 21:02)
Last updated: Dec 20 2023 at 11:08 UTC