Comment by b9r5
1 year 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 year 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.
But HoTT is removed from lean core?
From > /? Hott in lean4 https://www.google.com/search?q=hott+in+lean4- API Reference
- Hacker News RSS
- Source on GitHub
- Support Ukraine
- Equal Justice Initiative
- GiveWell Charities
Slacker News
Product
Community