News for hackers. Stuff that matters.

A comment on Formalizing Fermat's Last Theorem. Parent comment

Re:Formalizing Fermat's Last Theorem by lanstin on Friday September 04, 2026 @06:26PM (#49570967)
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.
[ Parent | on HN ]
Re:Formalizing Fermat's Last Theorem by mietek on Friday September 04, 2026 @07:36PM (#49571456)
Roughly, yes. See B. Werner (1997) “Sets in types, types in sets”.
[ Parent | on HN ]