11 ms·
amazing, it's a huge achievement. can someone clarify, where the writeup says "The finished proof was checked by Lean; it uses just Lean’s three standard axiom
by logicallee 12d ago
amazing, it's a huge achievement. can someone clarify, where the writeup says "The finished proof was checked by Lean; it uses just Lean’s three standard axioms" what does this mean? Aren't there a large set of standard axioms that are also necessary? (i.e. ZFC+)? if not, since it's only three axioms, can someone say what they were?
- sanxiyn 12d agoLean's three standard axioms are documented in The Lean Language Reference. https://lean-lang.org/doc/reference/latest/Axioms/#standard-axioms https://lean-lang.org/doc/reference/latest/Axioms/#standard-... The axiom of choice: axiom Classical.choice {α : Sort u} : Nonempty α → α The axiom of propositional extensionality: axiom propext {a b : Prop} : (a ↔ b) → a = b The quotient axiom: axiom Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Eq (Quot.mk r a) (Quot.mk r b)
- auggierose 12d agoI don't really know Lean, but I think this means, three axioms on top of their whole type theory machinery, to make it classical. The type theory machinery is the obfuscated encoding of the large set of standard axioms that they don't tell you about. For example, they can encode natural numbers using that machinery.