Yes, in fact Lean proves the law of the excluded middle using Diaconescu's theorem rather than assuming it as an independent axiom: https://github.com/leanprov

Yes, in fact Lean proves the law of the excluded middle using Diaconescu's theorem rather than assuming it as an independent axiom: https://github.com/leanprover/lean4/blob/ad1a017949674a947f0d6794cbf7130d642c6530/src/Init/Classical.lean#L35-L67 https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...