Zulip Chat Archive

Stream: Lean for teaching

Topics:

Teaching with Verbose Lean (44 messages, latest: Dec 19 2025 at 22:59)
adding type annotation to choose (9 messages, latest: Dec 19 2025 at 05:16)
building your own Lean game (209 messages, latest: Dec 14 2025 at 08:45)
Real analysis (204 messages, latest: Dec 11 2025 at 17:14)
A repo for learning Lean through projects (1 message, latest: Dec 03 2025 at 17:50)
Need help on square roots within The Mechanics of Proof (2 messages, latest: Nov 17 2025 at 19:06)
Lean for Waterproof file format design (21 messages, latest: Oct 27 2025 at 05:14)
Lean courses around the world (50 messages, latest: Sep 29 2025 at 04:18)
Natural numbers game Lean4 (77 messages, latest: Sep 06 2025 at 10:16)
Program Specification Based Programming Course (2 messages, latest: Sep 06 2025 at 10:16)
Autograder for logic intro with lean (4 messages, latest: Aug 29 2025 at 19:52)
A high-school exam question solved in Lean (13 messages, latest: Aug 28 2025 at 14:43)
incrementally publishing a Lean game (9 messages, latest: Aug 22 2025 at 15:03)
would mathlib users need to learn type theory at some point? (20 messages, latest: Aug 21 2025 at 15:58)
✔ CS 99 at Stanford University (7 messages, latest: Aug 19 2025 at 02:56)
Real Numbers game (20 messages, latest: Aug 05 2025 at 14:40)
Minimathlib: an experimental mathlib (7 messages, latest: Jul 30 2025 at 04:23)
#eval (Real.sin 3)^2 + (Real.cos 3)^2 failed (9 messages, latest: Jul 23 2025 at 20:03)
We made a board game for LEAN (7 messages, latest: Jul 15 2025 at 20:15)
Interactive Lean videos (3 messages, latest: Jul 04 2025 at 07:46)
Offline proof presentation e.g. in PDF (5 messages, latest: May 30 2025 at 19:13)
lean tutorial for motivated 8th graders (7 messages, latest: May 15 2025 at 13:16)
Issue with Duper in The Mechanics of Proof (42 messages, latest: May 04 2025 at 08:51)
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 Environments (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)
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)
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)
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: Dec 20 2025 at 21:32 UTC