Zulip Chat Archive
Stream: Berkeley Lean Seminar
Topics:
- Lean Camp 2025 (general chat) (57 messages, latest: Aug 22 2025 at 22:24)
- Real Analysis exercises (1 message, latest: Jun 20 2025 at 20:21)
- Covering Spaces (31 messages, latest: Apr 18 2023 at 05:57)
- Normal Galois Correspondence (7 messages, latest: Apr 17 2023 at 20:25)
- specifying implicit type (4 messages, latest: Aug 02 2022 at 14:21)
- Congratulations (1 message, latest: May 10 2021 at 11:58)
- Solvable groups (79 messages, latest: May 07 2021 at 06:09)
- trunc_cycle_factors (4 messages, latest: May 06 2021 at 15:14)
- computability using set supports (9 messages, latest: May 05 2021 at 04:24)
- Cycle Types (106 messages, latest: Apr 13 2021 at 22:36)
- Logistics (27 messages, latest: Mar 26 2021 at 02:39)
- PRs (3 messages, latest: Mar 13 2021 at 18:42)
- Project ideas (1707 messages, latest: Mar 10 2021 at 21:31)
- minpoly fallout (4 messages, latest: Jan 27 2021 at 18:52)
- Restrict algebra equivalence (55 messages, latest: Jan 16 2021 at 04:06)
- Berekely undergraduate research question (3 messages, latest: Jan 12 2021 at 07:03)
- Random intermediate_field.adjoin question (19 messages, latest: Jan 12 2021 at 06:56)
- Solvable field extensions (29 messages, latest: Jan 03 2021 at 22:55)
- More Project ideas (1 message, latest: Sep 04 2020 at 08:04)
- Massot Exercise 0080 (12 messages, latest: Jul 08 2020 at 23:01)
- Periods at the end of statements (11 messages, latest: Jul 06 2020 at 10:17)
- extends has_scalar (8 messages, latest: Jun 23 2020 at 20:48)
- Bug in lean?? (30 messages, latest: Jun 21 2020 at 22:52)
- Unfolding Definitions (20 messages, latest: Jun 17 2020 at 06:09)
- Good tips for subalgebras (3 messages, latest: Jun 16 2020 at 21:35)
- set or subtype (9 messages, latest: Jun 15 2020 at 19:46)
- Massot Exercise 0037 (32 messages, latest: Jun 12 2020 at 21:09)
- I can't have Lean infer a type class instance (6 messages, latest: Jun 10 2020 at 03:28)
- fintype (10 messages, latest: Jun 10 2020 at 00:50)
- Two silly questions (34 messages, latest: Jun 09 2020 at 20:58)
- Can I have multiple hypotheses of the same name? (5 messages, latest: Jun 09 2020 at 20:42)
- What's the formal type system of Lean? (4 messages, latest: Jun 04 2020 at 22:30)
- propext {P Q : Prop} : (P ↔ Q) → P = Q (51 messages, latest: Jun 04 2020 at 16:44)
- installing for linux and emacs, single user (4 messages, latest: Jun 02 2020 at 20:32)
- 55 in real numbers game (9 messages, latest: Jun 02 2020 at 19:56)
- windows python / git bash problem (85 messages, latest: May 29 2020 at 22:40)
- natural number game (41 messages, latest: May 27 2020 at 19:10)
- tactic at a target (12 messages, latest: May 27 2020 at 17:20)
- have giving error (12 messages, latest: May 27 2020 at 11:19)
- I may have broken number game (3 messages, latest: May 27 2020 at 11:18)
- Apply implication to hypothesis (6 messages, latest: May 27 2020 at 11:17)
- Induction on new variable (5 messages, latest: May 26 2020 at 20:53)
- seminar information (1 message, latest: May 26 2020 at 19:07)
- stream events (1 message, latest: May 22 2020 at 21:14)
Last updated: Dec 20 2025 at 21:32 UTC