Lean 4 without any axioms

This repository is an experiment to see how much you can do without any of Lean's standard axioms, that is:

• without propositional extensionality (propext)
• without useful quotients (Quot.sound)
• without functional extensionality (funext, consequence of Quot.sound)
• without choice (Classical.choice)
• without law of excluded middle (consequence of all three axioms)

With these rules, Z (ZF without choice or replacement) has been formalized and formalization of real numbers is partway done.