alt Hacker NewsZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.
Replies
andriy_koval • yesterday at 9:42 PM
do we know if claude's formalization is built on top of zfc and not zfc+extra?
zfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
➕ show 1 reply
Reply to sibling - lean4 doesn't rest on ZF or ZFC. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Co... However I believe an equivalence of power has been shown between the two.