Zulip Chat Archive
Stream: Lean for teaching
Topics:
- Issue with
Duper
inThe Mechanics of Proof
(41 messages, latest: May 01 2025 at 15:28) - Creating aliases for a tactic (19 messages, latest: Apr 18 2025 at 13:51)
- Game about finishing tactics (27 messages, latest: Apr 08 2025 at 18:56)
- Why are filters not used pervasively in undergrad education? (19 messages, latest: Mar 30 2025 at 13:49)
- A 'game'/interactive tutorial for items other than proofs (4 messages, latest: Mar 25 2025 at 09:26)
- For game developers: small script for refactoring levels (1 message, latest: Mar 14 2025 at 20:46)
- Verbose Lean (53 messages, latest: Mar 06 2025 at 22:41)
- Help design this exercise (11 messages, latest: Jan 23 2025 at 09:14)
- Verified Compiler (1 message, latest: Jan 18 2025 at 16:17)
- A study from UZH (1 message, latest: Jan 09 2025 at 21:41)
- Pandoc Lean Reader (1 message, latest: Jan 08 2025 at 15:00)
- beginner (5 messages, latest: Jan 08 2025 at 13:20)
- result of my lean mentorship program: 3 out of 16 (3 messages, latest: Dec 19 2024 at 09:20)
- Introduction to mathematical logic with Lean 4? (4 messages, latest: Nov 28 2024 at 11:20)
- Preparing HTML slides (10 messages, latest: Nov 21 2024 at 17:15)
- usage of the term 'proposition' in KR high school math (31 messages, latest: Nov 12 2024 at 14:44)
- live.lean-lang.org usage (14 messages, latest: Nov 11 2024 at 17:13)
- Automarking exercises with prover (29 messages, latest: Oct 30 2024 at 14:51)
- setting up local lean server for online use by students? (22 messages, latest: Oct 15 2024 at 11:29)
- One day tutorial (17 messages, latest: Sep 24 2024 at 17:31)
- Lean4 cheatsheet (203 messages, latest: Sep 24 2024 at 10:37)
- teaching lean alone in south korea (1 message, latest: Sep 24 2024 at 04:28)
- Informalisation for teaching (7 messages, latest: Sep 16 2024 at 11:36)
- Short introduction video in Lean4 (1 message, latest: Sep 13 2024 at 17:15)
- beta reduction (16 messages, latest: Aug 23 2024 at 21:21)
- Checking equality of types between different
Environment
s (9 messages, latest: Aug 23 2024 at 12:42) - Fall 2024 (1 message, latest: Aug 20 2024 at 16:20)
- Quantum computing (140 messages, latest: Aug 14 2024 at 18:58)
- Error in Set Theory Game (5 messages, latest: Aug 04 2024 at 01:41)
- proof irrelevant (11 messages, latest: Jul 26 2024 at 19:52)
- Workshop: interactive thm proving in education + research (3 messages, latest: Jul 24 2024 at 10:01)
- Project: Dutch version of verbose-lean4 (9 messages, latest: Jul 22 2024 at 13:24)
- Analysis Lean Game (9 messages, latest: Jul 15 2024 at 23:37)
- New animated video on the Lambda Calculus and Lean :D (2 messages, latest: Jun 15 2024 at 11:31)
- NSF proposal on Git-maintained math OER content (4 messages, latest: Jun 14 2024 at 03:56)
- ✔ PR adding a Lean course (5 messages, latest: Jun 03 2024 at 00:46)
- teaching resources on website (10 messages, latest: May 10 2024 at 07:05)
- Moving lecture notes to Lean 4 (5 messages, latest: Apr 29 2024 at 18:17)
- ✔ Is there a tactic manual? (2 messages, latest: Apr 04 2024 at 06:41)
- ThEdu'24 (1 message, latest: Mar 27 2024 at 18:11)
- Natural numbers game Lean4 (66 messages, latest: Mar 08 2024 at 17:21)
- Automatic grading of lean4 codes (51 messages, latest: Jan 29 2024 at 17:24)
- ✔ e^{i\pi}+1=0 (3 messages, latest: Jan 29 2024 at 09:56)
- Advertising a course (70 messages, latest: Jan 22 2024 at 13:57)
- Bool vs Prop (69 messages, latest: Jan 13 2024 at 20:25)
- advanced MiL exercises (3 messages, latest: Dec 31 2023 at 05:18)
- Post-quantum crypto (1 message, latest: Dec 18 2023 at 20:52)
- 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)
- ✔
have
tactic 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)
- 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)
- 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)
- 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)
cases
isn'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: May 02 2025 at 03:31 UTC