Hacker News new | ask | show | jobs
by b9r5 477 days ago
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.
1 comments