News for hackers. Stuff that matters.

A comment on Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?.

Re:Should Type Theory (HoTT) Replace (ZFC) Set Theory as the... by b9r5 on Wednesday February 26, 2025 @10:56PM (#43191176)
In a practical sense, hasn't type theory already replaced ZFC in the foundations of math? Lean is what working mathematicians currently use to formally prove theorems, and Lean is based on type theory rather than ZFC.
[ Parent | on HN ]
Re:Should Type Theory (HoTT) Replace (ZFC) Set Theory as the... by westurner on Thursday February 27, 2025 @12:28PM (#43196452)
But HoTT is removed from lean core?

From https://news.ycombinator.com/item?id=42440016#42444882 :

> /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4

https://github.com/forked-from-1kasper/ground_zero :

> Lean 4 HoTT Library

[ Parent | on HN ]