Zulip Chat Archive

Stream: Is there code for X?

Topic: Measurable cardinals

Meow (Aug 04 2023 at 09:58):

Gale-Stewart theorem (open determinacy) was already formalized in Lean 3. Did someone formalized measurable cardinals and $\mathbf{\Pi}^1_1$ determinacy in Lean?

Last updated: Dec 20 2023 at 11:08 UTC