Zulip Chat Archive
Stream: Is there code for X?
Topic: AD determinacy axiom
Olaf Kołodziejski (Feb 14 2023 at 17:27):
Hey, is there a code for ZF+AD?
Damiano Testa (Feb 14 2023 at 17:39):
I think that there might be nothing.
A lot of mathlib uses the axiom of choice, so that's a problem...
Yaël Dillies (Feb 14 2023 at 20:21):
We have docs#Set if you want to get ideas on how to embed ZF + AD into Lean.
Last updated: May 02 2025 at 03:31 UTC