A self-study Math genius Vladimir Voevodsky, Fields Medalist, Russian.
Voevodsky borrowed idea from Computer Science (“Interface” =hide implementation details) to Math, and vice-versa, from Math to Computer Science :
Homotopy Type Theory (HoTT)
Result: Computer to prove math theorems.
Computer Science Idea:
- Hiding Implementation Detail
- Black Box “Interface”
- Type (类) : Boolean, Integer, String, … (stronger structure than ＂Set＂ 集合)
Math Idea (Abstract Geometry : Algebraic Geometry) :
- Homotopy (同伦)
- eg. Cup ~ Donut, both are homotopic or same “Type” (in Computer)
- Isomorphism is Equality “=”
- Homotopy Type Theory (HoTT):
- Univalent Theorem: both objects are considered “=” if they are isomorphic (prove if 1-to-1 correspondence 对应)
Mathtuition88 